Univalent Categories and Rezk Completion

Proof. Let $(g,\eta ,ϵ)$ and $(g^{\prime },{\eta }^{\prime },{ϵ}^{\prime })$ witness invertibility of $f$, with $\eta :g\circ f=1_a$, $ϵ:f\circ g=1_b$, and likewise for the primed data. The equations inhabit identity types of sets, hence are mere propositions; by theorem 62.30 it suffices to identify $g$ with $g^{\prime }$. Using $ϵ$ and ${\eta }^{\prime }$, $$g^{\prime }\stackrel{rightunit}{=}{g}^{\prime }\circ 1_b\stackrel{ϵ}{=}{g}^{\prime }\circ (f\circ g)\stackrel{associativity}{=}(g^{\prime }\circ f)\circ g\stackrel{{\eta }^{\prime }}{=}{1}_a\circ g\stackrel{leftunit}{=}g.$$ Thus $a\cong b$ is a subtype of the set ${\mathrm{hom}}_A(a,b)$, hence a set. ◻

Proof. Each $a=b$ is equivalent to the set $a\cong b$ (lemma 74.4); a type whose identity types are sets is a $1$-type (definition 66.2). ◻

Proof. By path induction assume $p\equiv {\mathsf{refl}}_a$, $q\equiv {\mathsf{refl}}_b$; then the left side is $f$ and the right side is $1_b\circ f\circ 1_a$, identified with $f$ by the unit laws. ◻

Proof. Suppose first that $A_0$ is a set. Then each loop type $a=a$ is a mere proposition. Univalence makes $\mathsf{idtoiso}:(a=a)\to (a\cong a)$ an equivalence, so $a\cong a$ is a proposition as well. Its two elements $f$ and $1_a=\mathsf{idtoiso}({\mathsf{refl}}_a)$ are therefore equal.

Conversely, suppose every automorphism is the identity. For $p,q:a=b$, the composite $$\mathsf{idtoiso}(q{)}^{-1}\circ \mathsf{idtoiso}(p):a\cong a$$ equals $1_a$ by hypothesis. Cancelling $\mathsf{idtoiso}(q{)}^{-1}$ gives $\mathsf{idtoiso}(p)=\mathsf{idtoiso}(q)$; injectivity of this equivalence then gives $p=q$. Thus every identity type $a=b$ is a proposition, which is exactly that $A_0$ is a set. ◻

Proof. Truncation eliminates concatenation into the set-valued hom type. Double truncation induction reduces associativity and both unit laws to the corresponding path-groupoid laws of theorem 30.20; hence the precategory equations hold. Its map from object identity to isomorphism has underlying arrow $|p{|}_0$. Inverses are represented by $p^{-1}$, and the inverse equations again follow by truncation induction.

This map is an equivalence for every $x,y$ precisely when $x{=}_{X}y\to \Vert x{=}_{X}y{\Vert }_0$ is an equivalence. By lemma 66.55, that holds precisely when each path type is a set, which is the definition that $X$ is a $1$-type. ◻

Proof. Naturality is a product of identifications in sets, a mere proposition by the closure theorems; so the type of natural transformations is a subtype of the set $\prod _{a:A_0}{\mathrm{hom}}_B(Fa,Ga)$ (a product of sets, using theorem 65.18). ◻

Proof. If $\delta$ inverts $\gamma$, then ${\delta }_a\circ {\gamma }_a=1_{Fa}$ and ${\gamma }_a\circ {\delta }_a=1_{Ga}$. Conversely let each ${\gamma }_a$ have inverse ${\delta }_a$; the family $\delta$ is natural since for $f:{\mathrm{hom}}_A(a,b)$, and $(\delta \circ \gamma {)}_a=1_{Fa}$ and $(\gamma \circ \delta {)}_a=1_{Ga}$; lemma 74.14 promotes these component equations to the two inverse identities. ◻

Proof. Fix $F,G:A\to B$; we invert $\mathsf{idtoiso}:(F=G)\to (F\cong G)$. Given a natural isomorphism $\gamma$, each component is an isomorphism (lemma 74.16), so univalence of $B$ yields $\mathsf{isotoid}({\gamma }_a):Fa=Ga$, and function extensionality (theorem 65.18) an identification $\overline{\gamma }:F_0=G_0$ with $\mathsf{happly}(\overline{\gamma })(a)=\mathsf{isotoid}({\gamma }_a)$. Among the data of a functor, the two equation families are mere propositions. By theorem 62.30, the second component is an identification between the transport of the hom-action of $F$ along $\overline{\gamma }$ and the hom-action of $G$. The first component of the required $\mathrm{\Sigma }$-path is $\overline{\gamma }$; the functor-law components need no further choice because they are mere propositions. For the hom-action component, the computation rule for $\mathsf{funext}$ evaluates $\mathsf{happly}(\overline{\gamma })$ at $a$ and $b$, so lemma 74.10 carries $Ff$ (for $f:{\mathrm{hom}}_A(a,b)$) to This defines $\mathsf{isotoid}:(F\cong G)\to (F=G)$.

For the round trips: an identification $F=G$ is determined by its image in $F_0=G_0$, because the remaining components of the characterization above are mere propositions; and if $\gamma =\mathsf{idtoiso}(p)$ then ${\gamma }_a=\mathsf{idtoiso}(\mathsf{happly}(p_0)(a))$ by path induction, whence $\overline{\gamma }=p_0$ by $\mathsf{funext}$. Conversely $\mathsf{idtoiso}(\overline{\gamma }{)}_a=\mathsf{idtoiso}(\mathsf{isotoid}({\gamma }_a))={\gamma }_a$, and natural transformations are determined by their components (lemma 74.14). ◻

Proof. Given $(G,\eta ,ϵ)$: the assignment $g\mapsto {\eta }_b^{-1}\circ G(g)\circ {\eta }_a$ is a two-sided inverse of $F_{a,b}$ (a chase using naturality and functoriality), so $F$ is fully faithful, and ${ϵ}_b:FGb\cong b$ splits essential surjectivity. Conversely, given fully faithful $F$ and a splitting $b\mapsto (G_{0}b,{ϵ}_b:F{G}_{0}b\cong b)$, define $G$ on $g:{\mathrm{hom}}_B(b,b^{\prime })$ as the unique morphism with $F(G(g))={ϵ}_{b^{\prime }}^{-1}\circ g\circ {ϵ}_b$, and let ${\eta }_a$ be the unique morphism with $F({\eta }_a)={ϵ}_{Fa}^{-1}$. Functoriality of $G$ and naturality of $\eta ,ϵ$ follow from faithfulness of $F$. Indeed, $$F(G(1_b))={ϵ}_b^{-1}\circ {ϵ}_b=1_{FGb},$$ so $G(1_b)=1_{Gb}$; and for $g:b\to b^{\prime }$, $h:b^{\prime }\to b^{″}$, $$F(G(h\circ g))={ϵ}_{b^{″}}^{-1}\circ h\circ g\circ {ϵ}_b=F(Gh\circ Gg),$$ so $G(h\circ g)=Gh\circ Gg$. The defining equality for $Gg$ rearranges to $g\circ {ϵ}_b={ϵ}_{b^{\prime }}\circ F(Gg)$, which is naturality of $ϵ$. Applying $F$ to the naturality square for $\eta$ gives on both sides ${ϵ}_{F{a}^{\prime }}^{-1}\circ Ff$; faithfulness gives the square in $A$. ◻

Proof. Let $(a,f)$ and $(a^{\prime },f^{\prime })$ be two elements. Then $f^{\prime -1}\circ f:Fa\cong F{a}^{\prime }$, and since $F$ is fully faithful there is $g:a\cong a^{\prime }$ with $Fg=f^{\prime -1}\circ f$. By univalence of $A$ take $p:=\mathsf{isotoid}(g):a=a^{\prime }$. Path induction (as in lemma 74.10) computes the transport of $f$ along $p$ in the family $x\mapsto (Fx\cong b)$ as so $(a,f)=(a^{\prime },f^{\prime })$ by theorem 62.30. ◻

Proof. An equivalence is a weak equivalence by truncating the splitting pointwise. Conversely let $F$ be fully faithful and essentially surjective. For each $b$ the type $\sum _{a:A_0}(Fa\cong b)$ is a mere proposition (lemma 74.21) and merely inhabited, hence inhabited by the elimination rule of truncation (definition 66.33); so $F$ is split essentially surjective. Propositionality: full faithfulness is a family of $\mathsf{isEquiv}$-conditions, and split essential surjectivity is a product of mere propositions by lemma 74.21. ◻

Proof. The type of precategories is an iterated $\mathrm{\Sigma }$-type, so by repeated use of theorem 62.30 an identification $A=B$ amounts to: $P_0:A_0=B_0$; a family of identifications ${\mathrm{hom}}_A(a,b)={\mathrm{hom}}_B({\mathsf{tr}}_{P_0}(a),{\mathsf{tr}}_{P_0}(b))$ (the axiom components being mere propositions over the rest); and identifications matching identities and composition. Applying univalence to $P_0$ and to each hom-identification — and $\mathsf{funext}$ to pass between families of identifications and identifications of families — this data is equivalent to: an equivalence $F_0:A_0\simeq B_0$; equivalences $F_{a,b}:{\mathrm{hom}}_A(a,b)\simeq {\mathrm{hom}}_B(F_{0}a,F_{0}b)$; and the functor equations $F(1_a)=1_{F_{0}a}$, $F(g\circ f)=Fg\circ Ff$ — precisely an isomorphism of precategories. To identify the composite with the canonical map, path-induct on $A=B$. At reflexivity every transport, both applications of univalence, and the resulting functor compute to the identity, so the comparison is reflexivity. ◻

Proof. Both are mere propositions (being fully faithful is a product of $\mathsf{isEquiv}$-conditions, as is $\mathsf{isEquiv}(F_0)$; split essential surjectivity is one by lemma 74.21), so a logical equivalence suffices. If $F$ is an isomorphism, then for $b:B$ we get $a$ with $F_{0}a=b$, hence $Fa\cong b$ by $\mathsf{idtoiso}$: split essential surjectivity. Conversely let $F$ be an equivalence, with $(G,\eta ,ϵ)$ as in proposition 74.20. By theorem 74.17 the precategories $A^A$ and $B^B$ are univalent, so the natural isomorphisms $\eta ,ϵ$ yield identifications $1_A=GF$ and $FG=1_B$; projecting to object parts, $G_0$ is a two-sided inverse of $F_0$ up to identification, so $F_0$ is an equivalence of types. ◻

Proof. Being univalent is a mere proposition (a product of $\mathsf{isEquiv}$-conditions), so identifications of univalent categories coincide with identifications of their underlying precategories (theorem 62.30). Now combine theorem 74.25 with lemma 74.26: the subtype of functors that are isomorphisms agrees with the subtype of equivalences. ◻

Proof. For univalent $A,B$ the type of equivalences $A\to B$ is a subtype of the objects of the univalent category $B^A$ (theorem 74.17), a $1$-type by lemma 74.8; by theorem 74.27 each $A=B$ is thus a $1$-type. ◻

Proof. Inverse: to $x:Fa$ associate the transformation $\alpha$ with ${\alpha }_{a^{\prime }}(f):=F(f)(x)$; its naturality is functoriality of $F$. One composite: ${\alpha }_a(1_a)=F(1_a)(x)=x$. The other: for $\alpha :\mathrm{y}a\to F$ and $f:{\mathrm{hom}}_A(a^{\prime },a)$, naturality gives ${\alpha }_{a^{\prime }}(f)={\alpha }_{a^{\prime }}((\mathrm{y}a)(f)(1_a))=F(f)({\alpha }_a(1_a))$, which is the transformation associated to ${\alpha }_a(1_a)$. For a natural transformation $\theta :F\to G$, both routes send $\alpha$ to ${\theta }_a({\alpha }_a(1_a))$; this is naturality in $F$. For $k:a^{\prime }\to a$, both routes send $\alpha$ to $F(k)({\alpha }_a(1_a))$, by the naturality square of $\alpha$; this is naturality in $a$. ◻

Proof. $\mathrm{hom}(\mathrm{y}a,\mathrm{y}b)\cong (\mathrm{y}b)(a)\equiv {\mathrm{hom}}_A(a,b)$ by theorem 74.31, and the isomorphism is inverse to the action of $\mathrm{y}$ on hom-sets. ◻

Proof. Identifications of objects of $B{|}_P$ agree with identifications of their carriers (theorem 62.30, $P$ being prop-valued), isomorphisms agree by definition, and $\mathsf{idtoiso}$ commutes with both comparisons by path induction. ◻

Proof. Take $\hat{A}:={\mathbf{Set}}_{\mathcal{U}}^{A^{\mathrm{op}}}{|}_P$, the full subcategory of the presheaf category on the mere property $P(F):=\Vert \sum _{a:A_0}(\mathrm{y}a\cong F)\Vert$; it is univalent by lemma 74.33 and definition 74.29. The corestriction $I$ of $\mathrm{y}$ lands in $\hat{A}$ and is fully faithful by corollary 74.32; it is essentially surjective by the definition of $P$. ◻

Proof. This is HoTT Book Theorem 9.9.4 [Uni13]. Its signature is a weak equivalence $H:A\to B$ of precategories and a univalent category $C$, exactly as here; it concludes that precomposition is an isomorphism of precategories, not merely an equivalence on objects. Lemmas 9.9.1–9.9.3 in the same source prove faithfulness from essential surjectivity and fullness from fullness plus essential surjectivity. The object component is constructed by characterizing the image object and its action on morphisms by contractible types; univalence of $C$ converts the unique isomorphism between two choices into the identity needed for truncation elimination. Thus no choice or resizing principle is hidden in the import.

Apply the imported isomorphism to $H:=I$ from theorem 74.34. Its essential surjectivity gives a factor of every $A\to C$ through $\hat{A}$. Explicitly, if $K,L:\hat{A}\to C$ and $p:K\circ I=L\circ I$, faithfulness of precomposition gives the unique $\overline{p}:K=L$ with ${\mathsf{ap}}_{(-\circ I)}(\overline{p})=p$. Thus the factorization is unique. This exact import is used only for the two examples immediately below; no subsequent core theorem depends on it. ◻

Proof. Transport along any identification is an equivalence, since ${\mathsf{tr}}_p^P$ and ${\mathsf{tr}}_{p^{-1}}^P$ have homotopies $${\mathsf{tr}}_{p^{-1}}^P({\mathsf{tr}}_p^P(u))=u,{\mathsf{tr}}_p^P({\mathsf{tr}}_{p^{-1}}^P(v))=v,$$ obtained by functoriality of transport and the paths $p\cdot p^{-1}=\mathsf{refl}$ and $p^{-1}\cdot p=\mathsf{refl}$ (proposition 62.2(ii)). Thus transport along the inverse path is an inverse map. ◻

Calculation. Write $p:=\mathsf{ua}(e)$. Transport in a function family is contravariant in its domain and covariant in its codomain, so two iterations give $${\mathsf{tr}}_p^{X\mapsto X\to X\to X}(m)(b_1,b_2)={\mathsf{tr}}_p^{X\mapsto X}(m({\mathsf{tr}}_{p^{-1}}^{X\mapsto X}(b_1),{\mathsf{tr}}_{p^{-1}}^{X\mapsto X}(b_2))).$$ The $\mathsf{ua}$ transport equations are $${\mathsf{tr}}_{\mathsf{ua}(e)}^{X\mapsto X}(a)=e(a),{\mathsf{tr}}_{\mathsf{ua}(e{)}^{-1}}^{X\mapsto X}(b)=e^{-1}(b).$$ Substitution into the preceding formula gives the displayed $m^{\prime }$. Apply $\mathsf{ap}$ to the associativity path $s(x,y,z)$ and substitute $e^{-1}(b_1),e^{-1}(b_2),e^{-1}(b_3)$; the two sides reduce to the two associativity composites for $m^{\prime }$. This constructs $s^{\prime }$ and proves the claimed pair equation by the path rule for $\mathrm{\Sigma }$. ◻

Proof. Fix $x$ and $\alpha ,\beta :Px$, and put

$$R(\alpha ,\beta ):=(\alpha {\le }_x\beta )\times (\beta {\le }_x\alpha ).$$

This is a proposition because the two $H$-judgments are propositions. Path induction, using reflexivity of ${\le }_x$, defines $u:(\alpha =\beta )\to R(\alpha ,\beta )$; antisymmetry defines $v:R(\alpha ,\beta )\to (\alpha =\beta )$. Hence $v\circ u$ is a weakly constant endomap of every path type: $u(p)=u(q)$ by propositionhood of $R(\alpha ,\beta )$, and applying $v$ gives $(v\circ u)(p)=(v\circ u)(q)$. The collapse lemma lemma 66.27, applied to $Px$, now makes $Px$ a set. ◻

Proof. By theorem 62.30, an identification $(x,\alpha )=(y,\beta )$ consists of $p:x=y$ together with ${\mathsf{tr}}_p(\alpha )=\beta$, and the latter is a mere proposition since $P$ is set-valued by lemma 207.46. An isomorphism $(x,\alpha )\cong (y,\beta )$ consists of an isomorphism $f:x\cong y$ in $X$ such that $H_{\alpha \beta }(f)$ and $H_{\beta \alpha }(f^{-1})$ — again a mere condition on $f$. Since $X$ is univalent, $(x=y)\simeq (x\cong y)$; it therefore suffices to show, for $p:x=y$, $${\mathsf{tr}}_p(\alpha )=\beta ⟺H_{\alpha \beta }(\mathsf{idtoiso}(p))\wedge H_{\beta \alpha }(\mathsf{idtoiso}(p{)}^{-1}).$$ Left to right is the existence of $\mathsf{idtoiso}$ for ${\mathrm{Str}}_{(P,H)}(X)$ itself. For right to left, path induction reduces to $p\equiv {\mathsf{refl}}_x$, where the hypotheses read $\alpha {\le }_x\beta$ and $\beta {\le }_x\alpha$; standardness gives $\alpha =\beta$. The two mere conditions correspond under this equivalence by construction, so $\mathsf{idtoiso}$ for the structure precategory is an equivalence. ◻