homotopy type theory - Practical advantages of univalent foundations

I'm interested in the machine translation of mathematics from informal to formal (a la Ganesalingam in The Language of Mathematics). As a first step, I am designing a computer language for expressing mathematical definitions, theorems, and arguments that would at some later point be amenable to a small formalization kernel. (At this point, the language looks like a pared-down Isabelle/ZFC with support for functions not defined on full domains, realm-like objects, and a weak sense of parametric types and polymorphic functions).This translation p...Read more

Does the induction principle of the type of booleans imply its recursion principle?

The type of booleans, denoted by ${\mathbf{2}}$, has two terms $0_{\mathbf{2}}:{\mathbf{2}}$ and $1_{\mathbf{2}}:{\mathbf{2}}$. The induction principle of ${\mathbf{2}}$ states that, given a dependent family $C:2\to {\mathcal{U}}$ and terms $c_0:C(0_{\mathbf{2}})$, $c_1:C(1_{\mathbf{2}})$, there exists a dependent function $f:\prod_{(x:{\mathbf{2}})} C(x)$ such that $f(0_{\mathbf{2}})=c_0$ and $f(1_{\mathbf{2}})=c_1$.The recursion principle of ${\mathbf{2}}$ states that to give a function $f:{\mathbf{2}}\to A$ is equivalent to give terms $a_0,a...Read more

Set truncations in homotopy type theory

We can define set truncation as a higher inductive type with the following constructors:$|-|_0 : A \to ||A||_0$trunc : $(a\ a' : ||A||_0)\ (p\ p' : a = a') \to p = p'$If we replace the type of trunc with $(a\ a' : A)\ (p\ p' : a = a') \to \text{pmap}\ (|-|_0)\ p = \text{pmap}\ (|-|_0)\ p'$, then this definition will be too weak.The question is, what if we define trunc as follows:trunc : $(a\ a' : A)\ (p\ p' : |a|_0 = |a'|_0) \to p = p'$?Is this enough to give us the set truncation or is it also too weak?...Read more

Help with simple homotopy type theory proof

I'm having some beginner problems understanding / proving simple facts about higher inductive type paths.If you take this higher inductive type for natural numbers modulo 1:hit N1 := | 0 : N1 | S : N1 -> N1 | mod : 0 = 1..I have the strong feeling that this corresponds exactly to (is equivalent to) the circle $S^1$ (with $b:S^1$ and $l:b=b$). Where the circle has $\pi_1(S¹, b) \cong (\mathbb{Z}, +, 0)$ by the isomorphism $n \mapsto l^n$, I'd think that N1 has $\pi_1($N1$, 0) \cong (\mathbb{Z}, +, 0)$ too, by the isomorphism $n \mapsto \te...Read more

homotopy type theory - A pointless circle in HoTT

In the beginning of chapter two in The HoTT Book there is a discussion about synthetic vs. analytic geometry: An important difference between homotopy type theory and classical homotopy theory is that homotopy type theory provides a synthetic description of spaces, in the following sense. Synthetic geometry is geometry in the style of Euclid [EucBC]: one starts from some basic notions (points and lines), constructions (a line connecting any two points), and axioms (all right angles are equal), and deduces consequences logically. This is in con...Read more

homotopy type theory - Defining equivalence of equivalences without assuming extensionality

In homotopy type theory, we say that a function $f$ is an equivalence between two types $A$ and $B$, if the inverse image of all points is contractible (as per say the n-lab or Paolo's Capriotti's Agda formalization). The "problem" with this definition is that if $A$ is a function type, the resulting definition asks for (propositional) equality of functions.Equivalently, one could proceed as per section 2.4 of the HoTT book and define equivalence via quasi-inverse (which is the route we've chosen).But this makes no actual difference: while one...Read more

homotopy type theory - What constitutes "a path" in HoTT?

($I$ is the interval [0..1], the domain of all paths in HoTT.)($2$ is the type of two elements, named here as $0_2$ and $1_2$.)Define a map $p : I \rightarrow 2$ by $p(0) = 0_2$ and $p(x) = 1_2$ when $x \neq 0$.Is this map a path, in the HoTT sense?If not, then how have I failed to define it properly?If so, then why isn't it a witness for $0_2$ = $1_2$?Edit: What I am asking is when can (classical) functions from the (classic) interval [0..1] into a type $A$ be used to define a path in $A$ (in the HoTT sense). I think by now we all know what th...Read more

homotopy type theory - Univalent Foundations and canonicity property are compatible?

I'm interested in HoTT, especially its application to foundations of mathematics.I believe strongly that Univalent Foundations is the very foundation of mathematics.So,I have a question.(Q) Univalent Foundations(or such variant systems of HoTT that provide a foundation of mathematics) and canonicity property are compatible?Of course, the answer to the question depends on the definition of such systems.Indeed the system in Appendix A.1 in the HoTT book has canonicity property,while the system in Appendix A.3 doesn't.But regardless of the ...Read more

homotopy type theory - The uniqueness principle for products in the HoTT Book

This is about a point I do not understand in Section 1.5 of the HoTT Book. Here is the relevant excerpt:To be able to define dependent functions over the product type, we have to generalize the recursor. Given $C:A\times B\to\mathcal U$, we may define a function $$f:\prod_{(x:A\times B)}C(x)$$by providing a function$$g:\prod_{(x:A)}\prod_{(y:B)}C((x,y))$$with defining equation$$f((x,y)):\equiv g(x)(y).$$For example, in this way we can prove the propositional uniqueness principle, which says that every element of $A\times B$ is equal to a pair. ...Read more

homotopy type theory - Exercise 4.6 (iii) in the HoTT Book

Being unable to solve Exercise 4.6 (iii) in the HoTT Book, I'd be most grateful for any help.Recall the statement of Exercise 4.6:For $A,B:\mathcal U$, define$$\mathsf{idtoqinv}_{A,B}:(A=B)\to\sum_{f:A\to B}\mathsf{qinv}(f)$$by path induction in the obvious way. Let $\mathsf{qinv}$-$\mathsf{univalence}$ denote the modified form of the univalence axiom which asserts that for all $A,B:\mathcal U$ the function $\mathsf{idtoqinv}_{A,B}$ has a quasi-inverse.(i) Show that $\mathsf{qinv}$-$\mathsf{univalence}$ can be used instead of univalence in the ...Read more

Ladyman's alternative justification for path induction in Homotopy Type Theory

I'm confused by the main point of this paper: http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdfThe authors ask whether HoTT is a valid foundation for all of mathematics in a certain strong sense. They identify the justification of path induction as crucial point. Then, it is shown that path induction follows from the uniqueness principle for identity types (UIP) and substitution of equal expressions ("transport" in HoTT).Two Questions:1) Why does the question arise at all? Why is it path induction and not induction on any other...Read more

homotopy type theory - From projection function to recursor and viceversa

In the HoTT book, page 37, the authors are defining a way to work with product types. They first define$$pr_1 : A \times B \to A, \quad pr_1 ((a,b)):\equiv a $$$$pr_2 : A \times B \to B, \quad pr_2 ((a,b)):\equiv b $$Then they try an alternative way to obtain this result. They consider the functions$$f:A\times B \to C \qquad g : A \to B \to C$$Then they define a recursor$$rec_{A\times B} : \Pi_{(C : \mathcal{U})} (A \to B \to C) \to (A \times B) \to C$$$$rec_{A\times B} (C, g, (a,b)) :\equiv g(a)(b)$$In this way, they can define$$pr_1 :\equiv r...Read more

Induction principle for higher induction types

I am reading the HoTT book and cannot figure out how the induction principe works for the suspension.Let $A$ be a type.Then as I understand it from chapter 6.5 of the book, the induction principle for $\Sigma A$ is as follows. Let $P: \Sigma A \rightarrow \mathcal{U}$.If you have two inhabitants $n:P(N),s:P(S)$and a function $f: \Pi_{x:\Sigma A} (n =^{P(S)}_{medi(x)} s)$.You get a section $g:\Pi_{x:A} P(x)$ with $g(N)=n$ and $g(S)=s$.But if I look in the solutions of the exercises at line 1679 of github,it states that a function $$f:\Pi_{x:\Sig...Read more

homotopy type theory - Can someone elaborate on a categorical/homotopical point made in the proof that $\Sigma 2 = S^1$, given in the HoTT book?

In chapter 6, specifically in the section about suspensions a proof is given that $∑2 = S^1$.The book says that $\mathrm{transport}^{x \mapsto g(f(x)) = x}(\mathrm{refl}_N, \mathrm{merid}(y)) = g(f(\mathrm{merid}(y))^{-1} \cdot \mathrm{refl}_N \cdot \mathrm{merid}(y)$ by "transport in path spaces and pulled back fibrations." Of course this is referring to Theorem 2.11.3 (in my copy), i.e. the fact that:$$\mathrm{transport}^{x \mapsto f(x) = g(x)}(p, q) = \mathrm{ap}_f(p)^{-1} \cdot \mathrm{refl}_N \cdot \mathrm{ap}_g(q)$$$What does this have to...Read more