ch:univalence: ch:univalence

Use identity induction with motive $B\mapsto A=B\to A\simeq B$ and reflexive branch the identity map together with its contractible-fiber witness. Call the result $j$. To compare $j(p)$ with $\mathsf{idtoeqv}(p)$, path-induct on $p$. Both underlying functions then compute to ${\mathrm{id}}_A$, and the type $\mathsf{isEquiv}({\mathrm{id}}_A)$ is a proposition, so the witnesses agree. The $\mathrm{\Sigma }$-path theorem gives $j(p)=\mathsf{idtoeqv}(p)$.

For $c:C$, let $E_c={\mathrm{\Sigma }}_{(b,q):{\mathsf{fib}}_g(c)}{\mathsf{fib}}_f(b)$. It is contractible: the base ${\mathsf{fib}}_g(c)$ is contractible and each fiber ${\mathsf{fib}}_f(b)$ is contractible. Map $E_c$ to ${\mathsf{fib}}_{gf}(c)$ by $((b,q),(a,p))\mapsto (a,{\mathsf{ap}}_g(p)\cdot q)$. Choosing the intermediate point $fa$ defines a section, and path induction gives a retraction. A retract of a contractible type is contractible, so every fiber of $gf$ is contractible.

Equivalence induction defines ${\mathsf{ua}}^{\prime }(X,e):A=X$ with ${\mathsf{ua}}^{\prime }(A,\mathrm{id})={\mathsf{refl}}_A$. The equality $\mathsf{idtoeqv}({\mathsf{ua}}^{\prime }(e))=e$ follows by the same induction; the other composite ${\mathsf{ua}}^{\prime }(\mathsf{idtoeqv}(p))=p$ follows by identity induction on $p$. Hence for fixed $A$, the total types ${\mathrm{\Sigma }}_X(A\simeq X)$ and ${\mathrm{\Sigma }}_X(A=X)$ are retracts of one another. The latter is a singleton and therefore contractible, so the former is contractible. The total-space criterion for the fibers of $\mathsf{idtoeqv}$ now proves univalence.

For $p={\mathsf{refl}}_A$, the section law of the univalence inverse gives ${\eta }_{{\mathsf{refl}}_A}:\mathsf{ua}(\mathsf{idtoeqv}({\mathsf{refl}}_A))={\mathsf{refl}}_A$. The underlying map of $\mathsf{idtoeqv}({\mathsf{refl}}_A)$ computes to ${\mathrm{id}}_A$, and its equivalence witness equals the chosen identity witness because $\mathsf{isEquiv}({\mathrm{id}}_A)$ is a proposition. Congruence of $\mathsf{ua}$ along that equality, followed by ${\eta }_{{\mathsf{refl}}_A}^{-1}$, yields ${\mathsf{refl}}_A=\mathsf{ua}({\mathrm{id}}_A)$.

The assumed computation path identifies the underlying function of $\mathsf{idtoeqv}(\mathsf{u}(e))$ with that of $e$. Since $\mathsf{isEquiv}(f)$ is a proposition, it upgrades uniquely to an equality $\mathsf{idtoeqv}(\mathsf{u}(e))=e$. Thus $\mathsf{u}$ is a right inverse of $\mathsf{idtoeqv}$. The induced map on total spaces retracts ${\mathrm{\Sigma }}_X(A\simeq X)$ onto the singleton ${\mathrm{\Sigma }}_X(A=X)$ exactly as in the retract proof of univalence; its fibers are consequently contractible. Therefore $\mathsf{idtoeqv}$ is an equivalence.

Function extensionality states that $\mathsf{happly}:(f=g)\to (f\sim g)$ is an equivalence; define $\mathsf{funext}$ by its inverse. The two displayed laws are the inverse and section homotopies of that equivalence. For the final law, $\mathsf{happly}({\mathsf{refl}}_f)$ computes to $\lambda x.{\mathsf{refl}}_{fx}$, so applying the second inverse law at ${\mathsf{refl}}_f$ gives $\mathsf{funext}(\lambda x.{\mathsf{refl}}_{fx})={\mathsf{refl}}_f$.

For $b:B$, let $(gb,{ϵ}_b)$ be the center of the contractible fiber ${\mathsf{fib}}_e(b)$. Then $ϵ:e(gb)=b$ is the right-inverse homotopy. At $e(a)$, both $(g(ea),{ϵ}_{ea})$ and $(a,\mathsf{refl})$ lie in the same contractible fiber; projecting their unique path gives $g(ea)=a$, the left-inverse homotopy. These homotopies make $g$ an equivalence, so $e^{-1}=(g,\mathsf{isEquiv}(g))$ has the required two laws.

Functoriality gives $\mathsf{ua}(e)\cdot \mathsf{ua}(e^{-1})=\mathsf{ua}(e^{-1}e)=\mathsf{ua}(\mathrm{id})=\mathsf{refl}$. Thus $\mathsf{ua}(e^{-1})$ is a right inverse of $\mathsf{ua}(e)$. Inverses of a path are unique, so $\mathsf{ua}(e^{-1})=\mathsf{ua}(e{)}^{-1}$. Equivalently, applying $\mathsf{idtoeqv}$ identifies both sides with $e^{-1}$; univalence makes $\mathsf{idtoeqv}$ injective.

Double Boolean induction on $b,b^{\prime }$ reduces the code to $\mathbf{1}$ in the equal cases and $\mathbf{0}$ in the mixed cases. In an equal case, $u:\mathbf{1}$ equals $\star$, so encode after decode is reflexivity; a mixed case has no $u$. Together with the previously proved decode-after-encode identity, these homotopies exhibit encode and decode as inverse equivalences $(b=b^{\prime })\simeq \mathsf{code}(b,b^{\prime })$.

Assume $q:\mathsf{ua}(e_{\mathsf{not}})={\mathsf{refl}}_{\mathbf{2}}$. Apply congruence to the function $p\mapsto {\mathsf{tr}}_p^{X\mapsto X}(\mathsf{tt})$. The left side is $e_{\mathsf{not}}(\mathsf{tt})=\mathsf{ff}$ by the univalence transport law; the right side is $\mathsf{tt}$. Boolean encode–decode sends the resulting path $\mathsf{ff}=\mathsf{tt}$ to an element of $\mathbf{0}$.

Evaluate an automorphism at $\mathsf{tt}$. If the value is $\mathsf{tt}$, injectivity forces the other value to be $\mathsf{ff}$, and function extensionality identifies the map with identity. If it is $\mathsf{ff}$, the other value must be $\mathsf{tt}$, and the map is Boolean negation. These cases define an inverse to $e\mapsto e(\mathsf{tt})$, proving $(\mathbf{2}\simeq \mathbf{2})\simeq \mathbf{2}$. Compose this equivalence with univalence $(\mathbf{2}=\mathbf{2})\simeq (\mathbf{2}\simeq \mathbf{2})$.

When $A$ and $B$ are propositions, each function type $A\to B$ and $B\to A$ is a proposition by function extensionality; hence their product $A\leftrightarrow B$ is a proposition. For any pair of implications, the round trips are pointwise equal to the identities because the codomains are propositions. Thus it determines an equivalence. Forgetting the equivalence witness and adding these forced homotopies are inverse maps; $\mathsf{isEquiv}$ is a proposition, so the inverse law on equivalences is automatic.

Let $(A,h_A),(B,h_B):{\mathcal{U}}_i^{\mathrm{prop}}$ and suppose maps both ways. Propositional univalence gives $p:A=B$. By the $\mathrm{\Sigma }$-path theorem it remains to compare the transported witness $h_A$ with $h_B$. The type $\mathsf{isProp}(B)$ is itself a proposition, so those two witnesses are equal. The pair $(p,-)$ is therefore a path in the subuniverse, not merely a path between its first projections.

By definition $\omega ={\mathsf{tr}}_{\mathsf{ua}(e_{\mathsf{not}})}^{X\mapsto X}(\mathsf{tt})$. The section supplied by construction 65.8 identifies $\mathsf{idtoeqv}(\mathsf{ua}(e_{\mathsf{not}}))$ with $e_{\mathsf{not}}$. Theorem 65.9(i) projects that equality to $\omega =e_{\mathsf{not}}(\mathsf{tt})$. Boolean computation reduces the latter to $\mathsf{ff}$, and concatenating the two paths gives the required closed term.

Functoriality sends an $n$-fold concatenation of $\mathsf{ua}(e_{\mathsf{not}})$ to $\mathsf{ua}(e_{\mathsf{not}}^n)$. Transport along it is therefore the underlying function $e_{\mathsf{not}}^n$. Induction on $n$ alternates the two Boolean constructors: the zero iterate is identity and each successor applies negation. Hence the value at $\mathsf{tt}$ is $\mathsf{tt}$ for even $n$ and $\mathsf{ff}$ for odd $n$.

Let $s:\mathbf{2}\simeq \mathbf{2}$ exchange the constructors and put $p:=\mathsf{ua}(s):\mathbf{2}=\mathbf{2}$. The univalence transport law gives ${\mathsf{tr}}_p^{X\mapsto X}(\mathsf{tt})=\mathsf{ff}$ and ${\mathsf{tr}}_p^{X\mapsto X}(\mathsf{ff})=\mathsf{tt}$. If UIP held in the universe, then $p={\mathsf{refl}}_{\mathbf{2}}$. Applying transport to this equality would identify the swap action with identity transport, hence $\mathsf{ff}=\mathsf{tt}$, contradicting Boolean separation.