January 6th
Today I learned that equality types of Cartesian products are well-behaved in type theory. Essentially, we have the equivalences\[\prod_{x,x':A\times B}(x=x')\simeq(\op{pr}_1x=\op{pr}_1x')\times(\op{pr}_2x=\op{pr}_2x').\]Note I may start repressing the parentheses around single-variable functions like $\op{pr}_1$ when little confusion is possible.
In one direction, we can just run $\op{pr}_1$ and $\op{pr}_2$ to $x=y$ to generate functions\[\begin{cases} \op{ap}_{\op{pr}_1}:(x=x')\to(\op{pr}_1x=\op{pr}_1x'), \\ \op{ap}_{\op{pr}_2}:(x=x')\to(\op{pr}_2x=\op{pr}_2x').\end{cases}\]Then induction for products will give \[f(x,x')\equiv\lambda p.\big(\op{ap}_{\op{pr}_1}p,\,\op{ap}_{\op{pr}_2}p\big):(x=x')\to(\op{pr}_1x=\op{pr}_1x')\times(\op{pr}_2x=\op{pr}_2x')\]because ordered pairs are primitive.
In the other direction, we note that we can use some induction to construct our function. We need to exhibit\[g:\prod_{x,x':A\times B}(\op{pr}_1x=\op{pr}_1x')\times(\op{pr}_2x=\op{pr}_2x')\to(x=x').\]By induction on the product, it suffices to exhibit a curried function in\[\prod_{x,x':A\times B}(\op{pr}_1x=\op{pr}_1x')\to(\op{pr}_2x=\op{pr}_2x')\to(x=x').\]Now inducting on the product $A\times B,$ we can let $x\equiv(a,b)$ and $x'\equiv(a',b'),$ meaning we have to exhibit\[\prod_{(a,a':A)}\prod_{(b,b':B)}(a=a')\to(b=b')\to((a,b)=(a',b')).\]Only at this point we can read this as (nested) path induction, after some swapping. Namely, we exhibit\[\prod_{(a,a':A)}\prod_{(p:a=a')}\prod_{(b,b':B)}\prod_{(q:b=b')}(a,b)=(a',b').\]By path induction (family $C(a,a',p)\equiv\prod_{(b,b':B)}\prod_{(q:b=b')}(a,b)=(a',b')$), it suffices to take $a\equiv a'$ and $p\equiv\refl_a.$ So it remains to exhibit\[\prod_{(a:A)}\prod_{(b,b':B)}\prod_{(q:b=b')}(a,b)=(a,b').\]By path induction (family $D(b,b',q)\equiv(a,b)=(a,b')$), it suffices to take $b\equiv b'$ and $q\equiv\refl_b.$ But then we see\[\lambda a.\lambda b.\refl_{(a,b)}:\prod_{(a:A)}\prod_{b:B}(a,b)=(a,b),\]which is what we wanted.
So we have somewhat natural mappings in both directions. I guess it remains to show that $g(x,x'):\op{qinv}(f(x,x')),$ which will imply $\op{isequiv}(f(x,x'))$ is inhabited, verifying that $f(x,x')$ witnesses the equivalences\[(x=x')\simeq(\op{pr}_1x=\op{pr}_1x')\times(\op{pr}_2x=\op{pr}_2x').\]The proof that $g(x,x'):\op{qinv}(f(x,x'))$ is a couple of somewhat involved inductions. I won't do this in formality, for my own sanity.
In one direction, we show $f(x,x')\circ g(x,x')\sim\op{id}_\square,$ which means we have $r:(\op{pr}_1x=\op{pr}_1x')\times(\op{pr}_1x=\op{pr}_1x')$ and need to show\[(f(x,x')\circ g(x,x'))(r)=r.\]By induction on $x,x':A\times B,$ we may assert $x\equiv(a,b)$ and $x'\equiv(a',b')$ so that $r:(a=a')\times(b=b').$ It's not clear to me why we can't start with an induction on $r,$ but an induction on $r$ now lets us assert $r\equiv(p,q)$ with $p:a=a'$ and $q:b=b'.$ Now we induct on $p$ and $q$ to let us say $p\equiv\refl_a$ and $q\equiv\refl_b.$ But then\[(f(x,x)\circ g(x,x))((\refl_a,\refl_b))\equiv f(x,x)(\refl_{(a,b)})\equiv(\refl_a,\refl_b),\]so reflexivity witnesses here.
In the other direction, we show $g(x,x')\circ f(x,x')\sim\op{id}_\square,$ which means we have $r:x=x'$ and need to show\[(g(x,x')\circ f(x,x'))(r)=r.\]By induction on $r,$ we take $x\equiv x'$ and $r\equiv\refl_x.$ Then induction on $x:A\times B$ lets us say $x\equiv(a,b),$ which implies\[(g(x,x)\circ f(x,x))(\refl_x)\equiv g(x,x)((\refl_a,\refl_b))\equiv\refl_{(a,b)},\]so again reflexivity witnesses.