May 3rd
Today I learned (finally) the proof that all mere propositions are sets. Very quickly, we recall the following definitions.
Definition. We say that a type $A:\UU$ is a mere proposition if and only if \[\op{isProp}(A):\equiv\prod_{(a,b:A)}(a=_Ab)\] is inhabited. In other words, $A$ has one connected component.
We also define a set.
Definition. We say that a type $A:\UU$ is a set if and only if \[\op{isSet}(A):\equiv\prod_{(a,b:A)}\prod_{(p,q:a=_Ab)}(p=_{a=b}q)\] is inhabited. In other words, all paths between points are homotopically equivalent.
The statement we're building towards is the following.
Proposition. If a type $A:\UU$ is a mere proposition, then $A$ is a set. In other words, we can inhabit \[\prod_{(A:\UU)}\op{isProp}(A)\to\op{isSet}(A).\]
This is harder than it appears. Fix our type $A:\UU$ and witness $\op{eq}:\op{isProp}(A)$ so that $f(a,b):a=b$ for any $a,b:A.$ Now it remains to witness\[\op{isSet}(A):\equiv\prod_{(a,b:A)}\prod_{(p,q:a=b)}(p=q).\]As motivation, we describe what we would like to do, but it isn't completely rigorous. We would like to fix a basepoint $a_0:A$ (this is illegal) and then show that each $p$ is equal to a chosen witness $\op{eq}(a_0,a)^{-1}\cdot\op{eq}(a_0,b).$ However, we cannot guarantee that anything other than $a$ and $b$ actually live in $A,$ so we make $a$ (say) act as our basepoint.
With this in mind, we define\[\op{eq}_a(c):\equiv f(a,a'):a=_Ac.\]This function is rigorizing our desire to use $a$ as a basepoint of $a.$ Now, we want to compare $p$ with $\op{eq}(a,a)^{-1}\cdot\op{eq}(a,b)\equiv\op{eq}_a(a)^{-1}\cdot\op{eq}_a(b),$ so we just brute-force apply $\op{eq}_a$ to $p:a=b$ and hope for the best. This tells us\[\op{transport}^{c\mapsto(a=c)}(p)\left(\op{eq}_a(a)\right)=_{a=b}\op{eq}_a(b).\]We say explicitly that this type-checks: $\op{eq}_a(a):a=a$ is transported into $a=b$ by the type family. However, we actually know things about how transport behaves on paths.
Lemma. We have that \[\prod_{(a,b:A)}\prod_{(p:a=b)}\prod_{(q:a=a)}\op{transport}^{c\mapsto(a=c)}(p)(q)=_{a=b}=q\cdot p.\]
This follows from path induction on $p$: taking $p\equiv\op{refl}_a,$ it suffices to show that\[\prod_{(a:A)}\prod_{(q:a=a)}\op{transport}^{c\mapsto(a=c)}(\op{refl}_a)(q)=_{a=b}q\cdot\op{refl}_a.\]But $\op{transport}^\bullet$ on $\op{refl}$ is the identity function, so this is trying to prove $q=q\cdot\op{refl}_a,$ which is a unit law. $\blacksquare$
Using the above lemma, we now know that\[\op{eq}_a(a)\cdot p=_{a=b}\op{eq}_a(b).\]From this it follows $p=\op{eq}_a(a)^{-1}\cdot\op{eq}_a(b),$ which was our dream to begin with. In particular, any two $p,q:a=b$ are both equal to $\op{eq}_a(a)^{-1}\cdot\op{eq}_a(b),$ which is exactly the statement that $A$ is a set. $\blacksquare$
We remark that this fact is somewhat surprising. Translating everything here in topology, we have said that a path-connected space has all paths (between fixed endpoints) homotopically equivalent. However, something as simple as the torus breaks this: low homotopy information does not determine higher homotopy information. Yet it does in type theory.
We can use this fact to get some other annoying lemmas.
Lemma. Given type $A:\UU,$ we have that $\op{isProp}(A)$ is a mere proposition.
Given witnesses $f,g:\op{isProp}(A),$ we need to show that $f=g.$ Well, these are functions, so by function extensionality, it suffices to show that\[\prod_{(a:A)}f(a)=g(a).\]However, $f(a)$ and $g(a)$ are still functions, so we use function extensionality again so that it suffices for\[\prod_{(a,b:A)}f(a,b)=_{a=b}g(a,b).\]But $A$ is a set because it is a mere proposition, so any two paths inhabiting $a=b$ are equal, so we are done. $\blacksquare$