January 12th
Today I learned about the univalence axiom. The core here is to establish what it means for two types $A$ and $B$ to be equal, with respect to a universe $\UU,$ but we don't really have an easy way to introduce such equalities. To be clear, we can exhibit a function\[\op{idtoeqv}:(A=_\UU B)\to(A\simeq B).\]Indeed, the main idea is to view $\op{id}_\UU:\UU\to\UU$ as a family of types indexed by $\UU$; what this gives us is the ability to think about\[\op{transport}^{\op{id}_\UU}(p):A\to B\]given our $p.$ We claim that this is an equivalence.
The easy way to see this as trying to exhibit a function\[\prod_{(A,B:\UU)}(A=_\UU B)\to(A\simeq B),\]for which path induction says that it suffices to take $A\equiv B$ and $p\equiv\refl_A$ so that our $\op{transport}^\bullet(p)\equiv\op{id}_\UU.$ But we know that $\op{id}_\UU$ is an equivalence with itself as a quasi-inverse, so we're done.
That is a bit cheap, however. More generally, for a type family $P:X\to\UU,$ we have that $p:x=y$ witnesses\[\op{transport}^P(p):P(x)\to P(y),\]which we claim is an equivalence $P(x)\to P(y).$ Taking $P\equiv\op{id}_\UU$ recovers the case that we're interested in. To show that this is an equivalence, it suffices to note that\[\op{transport}^P(p^{-1}):P(y)\to P(x)\]is its quasi-inverse. Indeed, because $\op{transport}$ commutes with path concatenation (proven with path induction), we can say that\[\op{transport}^P(p^{-1})\circ\op{transport}^P(p)=\op{transport}^P(p\cdot p^{-1})\stackrel*=\op{transport}^P(\refl_x)=\op{id}_{P(x)}.\]I guess some care must taken on $\stackrel*=$ because $\op{transport}^P$ is a dependent function, but $p\cdot p^{-1}$ and $\op{refl}_x$ are both of type $x=x,$ so we may restrict $\op{transport}^P$ to a function $(x=x)\to P(x)\to P(x).$ Then $\stackrel*=$ follows by applying $\op{transport}^P$ to both sides of $p^{-1}\cdot p=\refl_x.$ Anyways, similar holds in the opposite direction.
The point here is that\[\op{idtoeqv}(p)\equiv\op{transport}^{\op{id}}(p)\]suffices, where we are abusing $\op{transport}^{\op{id}}(p)$ to witness the entire equivalence in $A\simeq B.$ Now, the univalence axiom for a universe $\UU$ is the assertion that $\op{idtoeqv}$ is an equivalence for the universe $\UU$; in particular, we get a function\[\op{ua}:(A\simeq B)\to(A=_\UU B)\]which is the quasi-inverse of $\op{idtoeqv}.$ More or less, this is how we get to introduce equalities $A=B$—exhibit an equivalence $A\simeq B.$
Quickly, observe that this is the same pattern as with function extensionality. We could build a function\[\op{happly}:(f=g)\to(f\sim g)\]pretty easily by path induction. However, it's not clear how to construct the quasi-inverse of this function, so we have an axiom establishing it. It will turn out that univalence implies function extensionality, but I don't know why.