ch:univalent-categories: ch:univalent-categories

Path induction on $p$ gives $\mathsf{idtoiso}(p^{-1})=\mathsf{idtoiso}(p{)}^{-1}$; both sides are the identity isomorphism in the reflexive case. Double induction on $p,q$ gives $\mathsf{idtoiso}(p\cdot q)=\mathsf{idtoiso}(q)\circ \mathsf{idtoiso}(p)$. In a univalent category apply the inverse map $\mathsf{isotoid}$ and its inverse laws to obtain $\mathsf{isotoid}(i^{-1})=\mathsf{isotoid}(i{)}^{-1}$ and $\mathsf{isotoid}(j\circ i)=\mathsf{isotoid}(i)\cdot \mathsf{isotoid}(j)$ with the same path orientation.

In a preorder, an isomorphism $x\cong y$ is exactly the proposition $(x\le y)\times (y\le x)$. If the category is univalent, its object identity types are propositions because isomorphism types are, so $A_0$ is a set; the inverse of $\mathsf{idtoiso}$ sends mutual inequalities to $x=y$, giving antisymmetry. Conversely, for a set with an antisymmetric preorder, reflexivity maps $x=y$ to mutual inequalities and antisymmetry maps back; propositionality makes the round trips automatic, hence $\mathsf{idtoiso}$ is an equivalence.

Identity is $|\mathsf{refl}{|}_0$, composition is induced by concatenation using set-truncation recursion, and associativity and unit follow by truncation induction from the path groupoid laws. Every morphism is invertible by truncated path inverse. Thus isomorphisms $x\cong y$ are equivalent to $\Vert ({\Vert }_{0}x=y)$. The canonical map is the set-truncation constructor, which is an equivalence exactly when each $x=y$ is already a set. This condition for all endpoints says precisely that $X$ is a $1$-type.

Univalence gives $(a=a)\simeq \mathsf{Aut}(a)$. If $A_0$ is a set, $a=a$ is a proposition and contains reflexivity, hence is contractible; therefore every automorphism equals the identity. Conversely, if every automorphism is the identity, $\mathsf{Aut}(a)$ is contractible. For $a,b$, the type $a\cong b$ is a proposition because any two isomorphisms differ by an automorphism of $a$. Univalence transfers this to $a=b$, so $A_0$ is a set.

Every hom-map $\mathbf{1}\to \mathbf{1}$ is an equivalence, so the unique functor is fully faithful; its sole target object is in the image of any chosen $x:X$, and essential surjectivity is merely inhabited when $X$ is inhabited (the empty case is not a weak equivalence). An inverse functor to an actual precategory isomorphism would give mutually inverse maps between $X$ and $\mathbf{1}$, so $X$ must be contractible; conversely a contraction supplies the inverse. Taking an inhabited noncontractible $X$ shows the chaotic precategory is weakly equivalent to the univalent terminal category but is not itself univalent. More exactly, $\mathsf{idtoiso}:(x=y)\to \mathbf{1}$ is an equivalence for every $x,y:X$ if and only if every identity type $x=y$ is contractible. Thus $X_{\mathrm{ch}}$ is univalent exactly when $X$ is a mere proposition; under the exercise’s inhabitedness hypothesis, this is equivalent to $X$ being contractible.

From fully faithful and essentially surjective $F$, choose preimages using the stated untruncated hypothesis and define $G$ on objects. Full faithfulness uniquely lifts each arrow to define $G$ on homs; uniqueness also proves preservation of identities and composition. The chosen target isomorphisms form $ϵ:FG\cong 1$ by the same uniqueness calculation, and lifting their composites gives $\eta :1\cong GF$; naturality is obtained by applying the faithful hom-map. Conversely an adjoint equivalence plainly gives these data. When $A$ is univalent, equality of object choices follows from their isomorphisms, and hom-setness makes all remaining structure equal, so the constructions are mutually inverse.

Induct on the path $p:A=B$ of precategories. At reflexivity, transport of objects and morphisms is judgmentally identity, and the constructed functor and its inverse reduce to the identity functor. The canonical map $\mathsf{idtoiso}(\mathsf{refl})$ is also identity. Hence the comparison is reflexivity in the base case, and path induction proves the construction equals the canonical map for every $p$.

The forward Yoneda map sends a natural transformation $\alpha :ya\to F$ to ${\alpha }_a({\mathrm{id}}_a)$. Postcomposing with $\theta :F\to G$ yields ${\theta }_a({\alpha }_a\mathrm{id})$, which is the image under the Yoneda map; this proves naturality in $F$. For $f:a^{\prime }\to a$, precomposition with $y(f)$ sends the distinguished identity to $f$; naturality of $\alpha$ gives $F(f)({\alpha }_a\mathrm{id})={\alpha }_{a^{\prime }}(f)$. This is exactly naturality in $a$ along Yoneda.

Suppose $(a,i)$ and $(b,j)$ represent $F$. Then $j^{-1}i:ya\cong yb$; full faithfulness of Yoneda gives an isomorphism $a\cong b$, and univalence turns it into a path $a=b$. Transporting along that path identifies $i$ with $j$ because natural-isomorphism types between set-valued functors are sets and the Yoneda correspondence fixes the component. Hence any two representations are equal, so representability is a proposition.

The completion unit $I:A\to \hat{A}$ is fully faithful and essentially surjective by its universal property. If $A$ is already univalent, so is $\hat{A}$, and the weak-equivalence–equivalence theorem upgrades $I$ to an equivalence of categories. Thus completing a univalent category changes it only up to categorical equivalence.

A monoid structure is $(m,e)$ with associativity and unit laws; set $H(f)$ to $f(m(x,y))=m^{\prime }(fx,fy)$ and $f(e)=e^{\prime }$. The laws are propositions, so transport of structure along equivalences is unique and $H$ is standard. For rings include addition, multiplication, $0$, $1$, and additive inverse, and require preservation of both binary operations; preservation of $0$ and inverse follows from the group calculation, while preservation of $1$ must be included unless rings are allowed nonunital maps. The structure identity principle then identifies equality of structured objects with the appropriate structure-preserving equivalences.

If $f(xy)=f(x)f(y)$, then $f(e)=f(e)f(e)$; cancel $f(e)$ to obtain $f(e)=e$. Next $e=f(e)=f(x{x}^{-1})=f(x)f(x^{-1})$, so uniqueness of inverses gives $f(x^{-1})=f(x{)}^{-1}$. Hence preservation of multiplication entails preservation of unit and inverse, and the stronger and weaker formulations of $H$ are logically equivalent propositions.

Transporting a point $x_0:X$ along an equivalence $f:X\simeq Y$ gives $f(x_0):Y$, and the preservation witness is the equality $f(x_0)=y_0$. Identity and composition follow from function computation; the witness type is a proposition because $Y$ is a set. Thus this is a standard structure. Its objects are pairs $(X,x_0)$ with $X$ a set, and morphisms are functions carrying the distinguished point to the distinguished point; univalence identifies paths of pointed sets with pointed equivalences.

For the one-object precategory $BM$ of a monoid $M$, the Rezk completion has objects the representable presheaves merely isomorphic to the unique representable $y(\ast )$; its morphisms are natural transformations. Yoneda identifies $\mathrm{hom}(y(\ast ),y(\ast ))\cong M$, so the unit $I:BM\to \widehat{BM}$ is fully faithful. By the defining predicate of the full subcategory, every object $F$ of the completion carries $\Vert \sum _{x:\mathbf{1}}y(\ast )\cong F\Vert$; this truncated represented isomorphism is exactly the essential-surjectivity witness.