January 5th
Today I learned about equivalence of types. Fix $A$ and $B$ types. For $f:A\to B,$ we say that $f$ has a "quasi-inverse'' $g:B\to A$ if\[(f\circ g\sim\op{id}_A)\times(g\circ f\sim\op{id}_B).\]That is,\[\op{qinv}(f):\equiv\sum_{(g:B\to A)}(f\circ g\sim\op{id}_B)\times(g\circ f\sim\op{id}_A).\]In words, $f\circ g$ and $g\circ f$ are homotopically the identity, suggesting we have a homeomorphism from $A$ to $B,$ giving us an "equivalence.''
In reality, $\op{qinv}$ isn't well-behaved, so there's a different type $\op{isequiv}(f)$ which just witnesses $f$ being an equivalence of $A$ and $B.$ What's important is that $\op{isequiv}(f)$ is a bit better-behaved (all its elements are propositionally equal), but $\op{isequiv}(f)$ is inhabited if and only if $\op{qinv}(f)$ is inhabited. Then we define\[A\simeq B:\equiv\sum_{f:A\to B}\op{isequiv}(f).\]In accordance to constructive mathematics, we have $A$ is equivalent to $B$ if and only if we can construct the equivalence $f$ and the witness of its equivalence $\op{isequiv}(f).$
Equivalence behaves how we'd like; e.g., it's an equivalence relation over types. Reflexivity $A\simeq A$ is witnessed by $\op{id}_A,$ which has quasi-inverse $\op{id}_A.$ Indeed,\[\op{id}_A\circ\op{id}_A\sim\op{id}_A\equiv\op{id}_A\sim\op{id}_A\equiv\prod_{x:A}(\op{id}_A(x)=\op{id}_A(x))\]is witnessed by $\lambda x.\op{refl}_x.$ So $(\op{id}_A,\lambda x.\refl_x,\lambda x.\refl_x):\op{qinv}(\op{id}_A),$ which implies $\op{isequiv}(\op{id}_A)$ is inhabited, so $A\simeq B$ is inhabited.
Symmetry that $(A\simeq B)\to(B\simeq A)$ holds because a function is the quasi-inverse of any of its quasi inverses. Namely, $A\simeq B$ inhabited gives us $f:A\to B$ and $(f^{-1},\alpha,\beta):\op{qinv}(f).$ Well, by construction\[\begin{cases} \beta:f^{-1}\circ f\sim\op{id}_A, \\ \alpha:f\circ f^{-1}\sim\op{id}_B.\end{cases}\]This means $(f,\beta,\alpha):\op{qinv}(f^{-1}).$ Thus, with $f^{-1}:B\to A$ having $\op{qinv}(f^{-1})$ inhabited means $\op{isequiv}(f^{-1})$ is inhabited, so $B\simeq A$ is inhabited, as desired.
Transitivity that $(A\simeq B)\to(B\simeq C)\to(A\simeq C)$ holds because the composition of two functions with a quasi-inverse also has a quasi-inverse. Again, if we are told $A\simeq B$ and $B\simeq C$ are inhabited, then we can build $f:A\to B$ and $g:B\to C$ with $(f^{-1},\alpha_f,\beta_f):\op{qinv}(f)$ and $(g^{-1},\alpha_g,\beta_g):\op{qinv}(g).$ We want to show that $g\circ f:A\to C$ has a quasi-inverse, and we claim that $f^{-1}\circ g^{-1}:C\to A$ is our inverse function. To start, note for $c:C,$\begin{align*} (g\circ f)\circ(f^{-1}\circ g^{-1})(c) &\equiv g\big((f\circ f^{-1})(g^{-1}(c))\big) \\ &= g\big(\op{id}_B\left(g^{-1}(c)\right)\big) \tag{by $\alpha_f\left(g^{-1}(c)\right)$} \\ &\equiv g(g^{-1}(c)) \\ &= \op{id}_C(c). \tag{by $\alpha_g(c)$}\end{align*}It follows $\alpha_{gf}\equiv\lambda c.\alpha_f\left(g^{-1}(c)\right)\cdot\alpha_g(c):(g\circ f)\circ(f^{-1}\circ g^{-1})\sim\op{id}_C.$ Similarly, for $a:A,$ we have\begin{align*} (f^{-1}\circ g^{-1})\circ(g\circ f)(a) &\equiv f^{-1}\big((g^{-1}\circ g)(f(a))\big) \\ &= f^{-1}\big(\op{id}_B(f(a))\big) \tag{by $\beta_g(f(a))$} \\ &\equiv f^{-1}(f(a)) \\ &= \op{id}_A(a). \tag{by $\beta_f(a)$}\end{align*}It follows $\beta_{gf}\equiv\lambda a.\beta_g(f(a))\cdot\beta_f(a):(f^{-1}\circ g^{-1})\circ(g\circ f)\sim\op{id}_A.$ Bringing our witnesses together, we see\[\left(f^{-1}\circ g^{-1},\alpha_{fg},\beta_{fg}\right):\op{qinv}(g\circ f).\]With $\op{qinv}(g\circ f)$ inhabited, we see $\op{isequiv}(g\circ f)$ is inhabited, so $A\simeq C$ is inhabited, as desired.