March 21st
Today I learned about univalence validating synthetic type construction. Roughly speaking, we expect/would like all instances of synthetic constructions of types to be equal, which under univalence means that we merely have to show they are homotopically equivalent.
As a motivating example, we do this for products. We take the following synthetic construction of products.
Definition. Products are defined by a type family $P:\UU\to\UU\to\UU$ for which the following hold.
-
Constructor: for fixed $A,B:\UU,$ there is a function $\op{pair}(A,B):A\to B\to P(A,B).$ We will often suppress the types $A$ and $B$ in $\op{pair}$ if the fixed types are clear.
-
Induction: for fixed $A,B:\UU,$ there is an inductor \[\op{ind}_{A,B}:\prod_{(C:P(A,B)\to\UU)}\left(\prod_{(a:A)}\prod_{(b:B)}C(\op{pair}(a,b))\right)\to\prod_{(p:P(A,B))}C(p)\] for which \[\op{ind}_{A,B}(C)(f)(\op{pair}(a,b))=f(a,b),\] for any $a:A$ and $b:B.$ Again, we will often suppress the types $A$ and $B$ in $\op{ind}$ if the fixed types are clear.
Note that we have demoted the usually judgemental equality in the inductor to a mere propositional equality; frankly, we will not need the strength of a judgemental equality. Additionally, we remark that types are frequently constructed with perhaps a recursion and maybe a uniqueness principle, but we do not do this for simplicity.
The following is the claim here.
Proposition. Suppose $(P_1,\op{pair}_1,\op{ind}_1)$ and $(P_2,\op{pair}_2,\op{ind}_2)$ make product types. Then, for fixed $A,B:\UU,$ we have $P_1(A,B)\simeq P_2(A,B).$
We would like to exhibit quasi-inverses forwards and backwards, but for this, we need maps forwards and backwards. In one direction, we would like to exhibit $P_1(A,B)\to P_2(A,B),$ but we only have one way to construct such functions: induction. So we make $P_2(A,B)$ a constant type family by abuse of notation so that induction means we need to exhibit\[A\to B\to P_2(A,B).\]But $\op{pair}_2$ exhibits this! So we see\[\alpha_1\equiv\op{ind}_1(\op{pair}_2):P_1(A,B)\to P_2(A,B),\]which satisfies $\alpha_1(\op{pair}_1(a,b))=\op{pair}_2(a,b).$ Switching $1$s and $2$s gives a corresponding function\[\alpha_2\equiv\op{ind}_2(\op{pair}_1):P_2(A,B)\to P_1(A,B),\]which satisfies $\alpha_2(\op{pair}_2(a,b))=\op{pair}_1(a,b).$
To finish, we claim that $\alpha_1$ and $\alpha_2$ are in fact quasi-inverses. In one direction, we need to witness $\alpha_2\circ\alpha_1\sim\op{id}_{P_1(A,B)},$ which is the same as\[\prod_{p_1:P_1(A,B)}\alpha_2(\alpha_1(p_1))=p_1.\]Again by induction, we make $p_1\mapsto\alpha_2(\alpha_1(p_1))=p_1$ a type family so that induction makes it suffice for\[\prod_{(a:A)}\prod_{(b:B)}\alpha_2\big(\alpha_1(\op{pair}_1(a,b))\big)=\op{pair}_1(a,b).\]Well, we know that $\alpha_1(\op{pair}_1(a,b))=\op{pair}_2(a,b)$ by definition of $\alpha_1,$ and $\alpha_2(\op{pair}_2(a,b))=\op{pair}_1(a,b),$ so applying $\alpha_2$ to the first equality gives\[\alpha_2\big(\alpha_1(\op{pair}_1(a,b))\big)=\op{pair}_1(a,b).\]This is what we wanted. Switching $1$s and $2$s shows $\alpha_1\circ\alpha_2\sim\op{id}_{P_2(A,B)},$ so we are done here. $\blacksquare$
At this point, we are obligated to say that, for fixed $A$ and $B,$ $P_1(A,B)\simeq P_2(A,B)$ gives $P_1(A,B)=P_2(A,B)$ by univalence, so $P_1=P_2$ by function extensionality. So indeed, our synthetic construction of products guarantees "unique'' products like we wanted.
We remark that the proof actually gives stronger than just $P_1(A,B)\simeq P_2(A,B)$ because the proof talks about the relationship between the underlying constructors and inductors. In particular, we know that the homotopic equivalence takes $\op{pair}_1$ to and from $\op{pair}_2$ "naturally'': $\op{pair}_1(0,0):P_1(2,2)$ will not be taken to $\op{pair}_2(1,1):P_2(2,2).$
I also want to say that this feels like universal properties in category theory. That is, we can uniquely determine certain constructed objects merely by looking at their maps and functions in and out, which is a central philosophy in category theory. Explicitly, the following is the universal property for products.
Definition. Given objects $A,B$ in a category $\mathcal C,$ the product $A\times B$ is defined to be an object with projection maps $\pi_1:A\times B\to A$ and $\pi_2:A\times B\to B$ such that any maps $C\to A$ and $C\to B$ induce a map $C\to A\times B$ commuting with $\pi_1$ and $\pi_2.$
Now, type-theoretic products do not mention projection mappings, but one can show that we can construct induction given projections and vice versa, so induction and projections are more or less the same concept. We do note that there is a difference because type theory does care about the inhabitants of a type; category theory tries not to.
I guess I should provide the example that started this line of thinking. It is exercise 3.15 from the Homotopy Type Theory book . We recall the synthetic definition of truncated types.
Definition. Truncated types are defined by a type family $T:\UU\to\UU$ satisfying the following.
-
Construction: for fixed type $A,$ there is a function $\op{trunc}_A:A\to T(A).$ We will omit the subscript when possible.
-
Mere proposition: for fixed type $A,$ we have $p=q$ for any $p,q:T(A).$ Formally, $\op{isProp}(T(A))$ is inhabited.
-
Recursion: for fixed type $A$ and mere proposition $P,$ and function $f:A\to P,$ there is an induced function $\op{rec}_A(P)(f):T(A)\to P.$ Formally, \[\op{rec}:\prod_{(P:\op{Prop})}\prod_{(f:A\to P)}T(A)\to P.\] As usual, we will omit the subscript when possible.
Note we have omitted requirement that $\op{rec}_A(P)(f)(\op{trunc}(a))=f(a)$ because these are inhabitants of a mere proposition $P,$ so the (propositional) equality is free.
Now, we claim the following.
Proposition. Suppose $(T_1,\op{trunc}_1,\op{rec}_1)$ and $(T_2,\op{trunc}_2,\op{rec}_2)$ make truncated types. Then, for fixed type $A:\UU,$ we have $T_1(A)\simeq T_2(A).$
We follow the outline suggested by products. We want to exhibit quasi-inverses, and it will turn out that any natural map back and forth will do the trick. To exhibit $T_1(A)\to T_2(A),$ recursion on $T_1$ means that it suffices to exhibit $A\to T_2(A)$ because $T_2(A)$ is a mere proposition. But we already have $\op{trunc}_2:A\to T_2(A),$ so we see\[\alpha_1:\equiv\op{rec}_1(T_2(A))(\op{trunc}_2):T_1(A)\to T_2(A).\]Switching the roles of $1$ and $2$ gives us the reverse mapping\[\alpha_2:\equiv\op{rec}_2(T_1(A))(\op{trunc}_1):T_2(A)\to T_1(A).\]We could go through the entire proof that $\alpha_1$ and $\alpha_2$ are actually quasi-inverses, but $T_1(A)$ and $T_2(A)$ are mere propositions, so we just cite the fact that mere propositions $P$ and $Q$ are homotopically equivalent if we can exhibit $P\to Q$ and $Q\to P.$ This finishes. $\blacksquare$
Thus, any two examples of how to truncate types are equal as types by univalence. In particular, our example $A\mapsto\lnot\lnot A$ has\[\lnot\lnot A\simeq\lVert A\rVert\]for any $A:\UU,$ assuming the law of the excluded middle. So we can be satisfied that our example of proposition truncation is "good enough'' even if we only got propositional equality in our recursion.