March 15th
Today I learned how to fix the law of the excluded middle in homotopy type theory, from the homotopy type theory book as usual. The main issue with univalence is that it allows distinction between proofs/witnesses for a particular type, so we take the following definition.
Definition. Call a type $A:\UU$ a mere proposition if and only if the type \[\op{isProp}(A):\equiv\prod_{(a,b:P)}(a=b)\] is inhabited. In other words, all witnesses are equal.
So, in essence, types with a witness to $\op{isProp}(A)$ are either true or false, and being true doesn't give us any more information than that $A$ is true, for all proofs are the same here. Of course, requiring $\op{isProp}(A)$ weakens our logic, and I think homotopy type theory likes dealing with types more than mere propositions.
Anyways, we can formalize the idea that mere propositions are either true or false with no extra information. Certainly we hope that if mere proposition captures the idea of purely true or false, then the types $0$ and $1$ should mere propositions, so we start with these.
Example. The type $0$ is a mere proposition because any inhabitants $a,b:0$ let us inhabit any type, of which $a=b$ is an example, using the induction of $0.$
Example. The type $1$ is a mere proposition because we using the induction of $1$ on \[\prod_{(a:1)}\prod_{(b:1)}(a=b)\] means that we have to witness $\prod_{(b:1)}(\star=1),$ for which induction on $1$ (again) means we have to witness $\star=\star.$ Now, $\op{refl}_\star$ works here, so we're safe.
Thus, true and false are mere propositions, so we formalize the idea that mere propositions are either true or false with equivalences.
Proposition. Suppose $A$ is a mere proposition. If $A,$ then $A=1.$ If $\lnot A,$ then $A=0.$
The easiest way to show this is to take the following lemma.
Lemma. If $A$ and $B$ are mere propositions for which $A\to B$ and $B\to A$ are inhabited, then $A=B.$
We note that univalence means that we merely have to witness the equivalence $A\simeq B.$ Well, pick up any $f:A\to B$ and $g:B\to A,$ and we claim that $f$ and $g$ are quasi-inverses, which will be enough. Indeed, for any $a:A,$ we have that $(g\circ f)(a):A,$ but $A$ is a mere proposition, so\[(g\circ f)(a)=a,\]so $g\circ f\sim\op{id}.$ Similarly, any $b:B$ gives $(f\circ g)(b):B,$ which implies $(g\circ f)(b)=b$ because $B$ is a mere proposition, so $f\circ g\sim\op{id}$ as well. This is what we wanted. $\blacksquare$
In lieu of the above lemma, we merely have to exhibit maps to show the desired equalities. From here, we split this into cases.
-
We note that we always have $\lambda(a:A).\star:A\to1,$ so it remains to exhibit $1\to A.$ Well, given $A,$ we can fix $a:A$ and then use induction to give a map $1\to A$ sending $\star\mapsto a.$ So given $A,$ we do have $A=1$ by lemma.
-
We note that we always have $0\to A$ by inducting on $0,$ so it remains to exhibit $A\to 0:\equiv\lnot A.$ So given $\lnot A,$ we do have $A=0$ by lemma.
Having proved both parts of the proposition, we are done here. $\blacksquare$
Having established that mere propositions are well-behaved in terms of their truthiness, we introduce the law of the excluded middle in homotopy type theory. Having eliminated all possibly problematic $\infty$-groupoid structure for mere propositions, our law of the excluded middle is\[\op{LEM}:\prod_{(A:\UU)}\big(\op{isProp}(A)\to(A+\lnot A)\big).\]That is, all mere propositions are (constructively) either true or false. Note that this has not been stated as a theorem because it is an axiom. I am told that one can construct of models of homotopy type theory where even this law of the excluded middle breaks, which means it cannot be proven. But at least nothing breaks (immediately).
It will turn out that being a mere proposition is not a "serious'' block to proving types are inhabited. In particular, there is a way (I have not learned) to take a type $A$ and get a mere proposition $\lVert A\rVert$ that is inhabited if and only if $A$ is.