9.9 The Rezk completion

In this section we will give a universal way to replace a precategory by a category. In fact, we will give two. Both rely on the fact that “categories see weak equivalences as equivalences”.

To prove this, we begin with a couple of lemmas which are completely standard category theory, phrased carefully so as to make sure we are using the eliminator for ${\parallel \text{–}\parallel }_{-1}$ correctly. One would have to be similarly careful in classical category theory if one wanted to avoid the axiom of choice: any time we want to define a function, we need to characterize its values uniquely somehow.

Lemma 9.9.1.

If $A\mathrm{,}B\mathrm{,}C$ are precategories and $H\mathrm{:}A\mathrm{\to }B$ is an essentially surjective functor, then $\mathrm{(}\mathit{\text{–}}\mathrm{\circ }H\mathrm{)}\mathrm{:}{C}^B\mathrm{\to }{C}^A$ is faithful.

Proof.

Let $F,G:B\to C$, and $\gamma ,\delta :F\to G$ be such that $\gamma H=\delta H$; we must show $\gamma =\delta$. Thus let $b:B$; we want to show ${\gamma }_b={\delta }_b$. This is a mere proposition, so since $H$ is essentially surjective, we may assume given an $a:A$ and an isomorphism $f:Ha\cong b$. But now we have

$${\gamma }_b=G(f)\circ {\gamma }_{Ha}\circ F(f^{-1})=G(f)\circ {\delta }_{Ha}\circ F(f^{-1})={\delta }_b.\mathit{∎}$$

Lemma 9.9.2.

If $A\mathrm{,}B\mathrm{,}C$ are precategories and $H\mathrm{:}A\mathrm{\to }B$ is essentially surjective and full, then $\mathrm{(}\mathit{\text{–}}\mathrm{\circ }H\mathrm{)}\mathrm{:}{C}^B\mathrm{\to }{C}^A$ is fully faithful.

Proof.

It remains to show fullness. Thus, let $F,G:B\to C$ and $\gamma :FH\to GH$. We claim that for any $b:B$, the type

$$\sum _{(g:{\mathrm{hom}}_C(Fb,Gb))}\prod _{(a:A)}\prod _{(f:Ha\cong b)}({\gamma }_a=G{f}^{-1}\circ g\circ Ff)$$ (9.9.3)

is contractible. Since contractibility is a mere property, and $H$ is essentially surjective, we may assume given $a_0:A$ and $h:H{a}_0\cong b$.

Now take $g:\equiv Gh\circ {\gamma }_{a_0}\circ F{h}^{-1}$. Then given any other $a:A$ and $f:Ha\cong b$, we must show ${\gamma }_a=G{f}^{-1}\circ g\circ Ff$. Since $H$ is full, there merely exists a morphism $k:{\mathrm{hom}}_A(a,a_0)$ such that $Hk=h^{-1}\circ f$. And since our goal is a mere proposition, we may assume given some such $k$. Then we have

${\gamma }_a$ $=GH{k}^{-1}\circ {\gamma }_{a_0}\circ FHk$

$=G{f}^{-1}\circ Gh\circ {\gamma }_{a_0}\circ F{h}^{-1}\circ Ff$

$=G{f}^{-1}\circ g\circ Ff.$

Thus, (9.9.3) is inhabited. It remains to show it is a mere proposition. Let $g,g^{\prime }:{\mathrm{hom}}_C(Fb,Gb)$ be such that for all $a:A$ and $f:Ha\cong b$, we have both $({\gamma }_a=G{f}^{-1}\circ g\circ Ff)$ and $({\gamma }_a=G{f}^{-1}\circ g^{\prime }\circ Ff)$. The dependent product types are mere propositions, so all we have to prove is $g=g^{\prime }$. But this is a mere proposition, so we may assume $a_0:A$ and $h:H{a}_0\cong b$, in which case we have

$$g=Gh\circ {\gamma }_{a_0}\circ F{h}^{-1}=g^{\prime }.$$

This proves that (9.9.3) is contractible for all $b:B$. Now we define $\delta :F\to G$ by taking ${\delta }_b$ to be the unique $g$ in (9.9.3) for that $b$. To see that this is natural, suppose given $f:{\mathrm{hom}}_B(b,b^{\prime })$; we must show $Gf\circ {\delta }_b={\delta }_{b^{\prime }}\circ Ff$. As before, we may assume $a:A$ and $h:Ha\cong b$, and likewise $a^{\prime }:A$ and $h^{\prime }:H{a}^{\prime }\cong b^{\prime }$. Since $H$ is full as well as essentially surjective, we may also assume $k:{\mathrm{hom}}_A(a,a^{\prime })$ with $Hk=h^{\prime }{}^{-1}\circ f\circ h$.

Since $\gamma$ is natural, $GHk\circ {\gamma }_a={\gamma }_{a^{\prime }}\circ FHk$. Using the definition of $\delta$, we have

$Gf\circ {\delta }_b$ $=Gf\circ Gh\circ {\gamma }_a\circ F{h}^{-1}$

$=G{h}^{\prime }\circ GHk\circ {\gamma }_a\circ F{h}^{-1}$

$=G{h}^{\prime }\circ {\gamma }_{a^{\prime }}\circ FHk\circ F{h}^{-1}$

$=G{h}^{\prime }\circ {\gamma }_{a^{\prime }}\circ Fh^{\prime }{}^{-1}\circ Ff$

$={\delta }_{b^{\prime }}\circ Ff.$

Thus, $\delta$ is natural. Finally, for any $a:A$, applying the definition of ${\delta }_{Ha}$ to $a$ and $1_a$, we obtain ${\gamma }_a={\delta }_{Ha}$. Hence, $\delta \circ H=\gamma$. ∎

The rest of the theorem follows almost exactly the same lines, with the category-ness of $C$ inserted in one crucial step, which we have italicized below for emphasis. This is the point at which we are trying to define a function into objects without using choice, and so we must be careful about what it means for an object to be “uniquely specified”. In classical category theory, all one can say is that this object is specified up to unique isomorphism, but in set-theoretic foundations this is not a sufficient amount of uniqueness to give us a function without invoking $\mathrm{𝖠𝖢}$. In univalent foundations, however, if $C$ is a category, then isomorphism is equality, and we have the appropriate sort of uniqueness (namely, living in a contractible space).

Theorem 9.9.4.

If $A\mathrm{,}B$ are precategories, $C$ is a category, and $H\mathrm{:}A\mathrm{\to }B$ is a weak equivalence, then $\mathrm{(}\mathit{\text{–}}\mathrm{\circ }H\mathrm{)}\mathrm{:}{C}^B\mathrm{\to }{C}^A$ is an isomorphism.

Proof.

By ct:functor-cat, $C^B$ and $C^A$ are categories. Thus, by ct:eqv-levelwise it will suffice to show that $(\text{–}\circ H)$ is an equivalence. But since we know from the preceding two lemmas that it is fully faithful, by ct:catweq it will suffice to show that it is essentially surjective. Thus, suppose $F:A\to C$; we want there to merely exist a $G:B\to C$ such that $GH\cong F$.

For each $b:B$, let $X_b$ be the type whose elements consist of:

1. An element $c:C$; and

2. For each $a:A$ and $h:Ha\cong b$, an isomorphism $k_{a,h}:Fa\cong c$; such that

3. For each $(a,h)$ and $(a^{\prime },h^{\prime })$ as in 2 and each $f:{\mathrm{hom}}_A(a,a^{\prime })$ such that $h^{\prime }\circ Hf=h$, we have $k_{a^{\prime },h^{\prime }}\circ Ff=k_{a,h}$.

We claim that for any $b:B$, the type $X_b$ is contractible. As this is a mere proposition, we may assume given $a_0:A$ and $h_0:H{a}_0\cong b$. Let $c^0:\equiv F{a}_0$. Next, given $a:A$ and $h:Ha\cong b$, since $H$ is fully faithful there is a unique isomorphism $g_{a,h}:a\to a_0$ with $H{g}_{a,h}=h_0{}^{-1}\circ h$; define $k_{a,h}^0:\equiv F{g}_{a,h}$. Finally, if $h^{\prime }\circ Hf=h$, then $h_0{}^{-1}\circ h^{\prime }\circ Hf=h_0{}^{-1}\circ h$, hence $g_{a^{\prime },h^{\prime }}\circ f=g_{a,h}$ and thus $k_{a^{\prime },h^{\prime }}^0\circ Ff=k_{a,h}^0$. Therefore, $X_b$ is inhabited.

Now suppose given another $(c^1,k^1):X_b$. Then $k_{a_0,h_0}^1:c^0\equiv F{a}_0\cong c^1$. Since $C$ is a category, we have $p\mathrm{:}{c}^{\mathrm{0}}\mathrm{=}{c}^{\mathrm{1}}$ with $\mathrm{idtoiso}\mathit{}\mathrm{(}p\mathrm{)}\mathrm{=}{k}_{a_{\mathrm{0}}\mathrm{,}{h}_{\mathrm{0}}}^{\mathrm{1}}$. And for any $a:A$ and $h:Ha\cong b$, by 3 for $(c^1,k^1)$ with $f:\equiv g_{a,h}$, we have

$$k_{a,h}^1=k_{a_0,h_0}^1\circ k_{a,h}^0=p_{*}\left(k_{a,h}^0\right)$$

This gives the requisite data for an equality $(c^0,k^0)=(c^1,k^1)$, completing the proof that $X_b$ is contractible.

Now since $X_b$ is contractible for each $b$, the type ${\prod }_{(b:B)}{X}_b$ is also contractible. In particular, it is inhabited, so we have a function assigning to each $b:B$ a $c$ and a $k$. Define $G_0(b)$ to be this $c$; this gives a function $G_0:B_0\to C_0$.

Next we need to define the action of $G$ on morphisms. For each $b,b^{\prime }:B$ and $f:{\mathrm{hom}}_B(b,b^{\prime })$, let $Y_f$ be the type whose elements consist of:

[resume]

1. A morphism $g:{\mathrm{hom}}_C(Gb,G{b}^{\prime })$, such that

2. For each $a:A$ and $h:Ha\cong b$, and each $a^{\prime }:A$ and $h^{\prime }:H{a}^{\prime }\cong b^{\prime }$, and any $\mathrm{\ell }:{\mathrm{hom}}_A(a,a^{\prime })$, we have

   $$(h^{\prime }\circ H\mathrm{\ell }=f\circ h)\to (k_{a^{\prime },h^{\prime }}\circ F\mathrm{\ell }=g\circ k_{a,h}).$$

We claim that for any $b,b^{\prime }$ and $f$, the type $Y_f$ is contractible. As this is a mere proposition, we may assume given $a_0:A$ and $h_0:H{a}_0\cong b$, and each $a_0^{\prime }:A$ and $h_0^{\prime }:H{a}_0^{\prime }\cong b^{\prime }$. Then since $H$ is fully faithful, there is a unique ${\mathrm{\ell }}_0:{\mathrm{hom}}_A(a_0,a_0^{\prime })$ such that $h_0^{\prime }\circ H{\mathrm{\ell }}_0=f\circ h_0$. Define $g_0:\equiv k_{a_0^{\prime },h_0^{\prime }}\circ F{\mathrm{\ell }}_0\circ {(k_{a_0,h_0})}^{-1}$.

Now for any $a,h,a^{\prime },h^{\prime }$, and $\mathrm{\ell }$ such that $(h^{\prime }\circ H\mathrm{\ell }=f\circ h)$, we have $h^{-1}\circ h_0:H{a}_0\cong Ha$, hence there is a unique $m:a_0\cong a$ with $Hm=h^{-1}\circ h_0$ and hence $h\circ Hm=h_0$. Similarly, we have a unique $m^{\prime }:a_0^{\prime }\cong a^{\prime }$ with $h^{\prime }\circ H{m}^{\prime }=h_0^{\prime }$. Now by 3, we have $k_{a,h}\circ Fm=k_{a_0,h_0}$ and $k_{a^{\prime },h^{\prime }}\circ F{m}^{\prime }=k_{a_0^{\prime },h_0^{\prime }}$. We also have

$H{m}^{\prime }\circ H{\mathrm{\ell }}_0$ $={(h^{\prime })}^{-1}\circ h_0^{\prime }\circ H{\mathrm{\ell }}_0$

$={(h^{\prime })}^{-1}\circ f\circ h_0$

$={(h^{\prime })}^{-1}\circ f\circ h\circ h^{-1}\circ h_0$

$=H\mathrm{\ell }\circ Hm$

and hence $m^{\prime }\circ {\mathrm{\ell }}_0=\mathrm{\ell }\circ m$ since $H$ is fully faithful. Finally, we can compute

$g_0\circ k_{a,h}$ $=k_{a_0^{\prime },h_0^{\prime }}\circ F{\mathrm{\ell }}_0\circ {(k_{a_0,h_0})}^{-1}\circ k_{a,h}$

$=k_{a_0^{\prime },h_0^{\prime }}\circ F{\mathrm{\ell }}_0\circ F{m}^{-1}$

$=k_{a_0^{\prime },h_0^{\prime }}\circ {(F{m}^{\prime })}^{-1}\circ F\mathrm{\ell }$

$=k_{a^{\prime },h^{\prime }}\circ F\mathrm{\ell }.$

This completes the proof that $Y_f$ is inhabited. To show it is contractible, since hom-sets are sets, it suffices to take another $g_1:{\mathrm{hom}}_C(Gb,G{b}^{\prime })$ satisfying 2 and show $g_0=g_1$. However, we still have our specified $a_0,h_0,a_0^{\prime },h_0^{\prime },{\mathrm{\ell }}_0$ around, and 2 implies both $g_0$ and $g_1$ must be equal to $k_{a_0^{\prime },h_0^{\prime }}\circ F{\mathrm{\ell }}_0\circ {(k_{a_0,h_0})}^{-1}$.

This completes the proof that $Y_f$ is contractible for each $b,b^{\prime }:B$ and $f:{\mathrm{hom}}_B(b,b^{\prime })$. Therefore, there is a function assigning to each such $f$ its unique inhabitant; denote this function $G_{b,b^{\prime }}:{\mathrm{hom}}_B(b,b^{\prime })\to {\mathrm{hom}}_C(Gb,G{b}^{\prime })$. The proof that $G$ is a functor is straightforward; in each case we can choose $a,h$ and apply 2.

Finally, for any $a_0:A$, defining $c:\equiv F{a}_0$ and $k_{a,h}:\equiv Fg$, where $g:{\mathrm{hom}}_A(a,a_0)$ is the unique isomorphism with $Hg=h$, gives an element of $X_{H{a}_0}$. Thus, it is equal to the specified one; hence $GHa=Fa$. Similarly, for $f:{\mathrm{hom}}_A(a_0,a_0^{\prime })$ we can define an element of $Y_{Hf}$ by transporting along these equalities, which must therefore be equal to the specified one. Hence, we have $GH=F$, and thus $GH\cong F$ as desired. ∎

Therefore, if a precategory $A$ admits a weak equivalence functor $A\to \widehat{A}$, then that is its “reflection” into categories: any functor from $A$ into a category will factor essentially uniquely through $\widehat{A}$. We now give two constructions of such a weak equivalence.

Theorem 9.9.5.

For any precategory $A$, there is a category $\widehat{A}$ and a weak equivalence $A\mathrm{\to }\widehat{A}$.

First proof.

Let ${\widehat{A}}_0:\equiv F:𝒮e{t}^{A^{\mathrm{op}}}|\exists (a:A).(𝐲a\cong F)$, with hom-sets inherited from $𝒮e{t}^{A^{\mathrm{op}}}$. Then the inclusion $\widehat{A}\to 𝒮e{t}^{A^{\mathrm{op}}}$ is fully faithful and an embedding on objects. Since $𝒮e{t}^{A^{\mathrm{op}}}$ is a category (by ct:functor-cat, since $𝒮et$ is so by univalence), $\widehat{A}$ is also a category.

Let $A\to \widehat{A}$ be the Yoneda embedding. This is fully faithful by ct:yoneda-embedding, and essentially surjective by definition of ${\widehat{A}}_0$. Thus it is a weak equivalence. ∎

This proof is very slick, but it has the drawback that it increases universe level. If $A$ is a category in a universe $𝒰$, then in this proof $𝒮et$ must be at least as large as $𝒮e{t}_{𝒰}$. Then $𝒮e{t}_{𝒰}$ and ${(𝒮e{t}_{𝒰})}^{A^{\mathrm{op}}}$ are not themselves categories in $𝒰$, but only in a higher universe, and a priori the same is true of $\widehat{A}$. One could imagine a resizing axiom that could deal with this, but it is also possible to give a direct construction using higher inductive types.

Second proof.

We define a higher inductive type ${\widehat{A}}_0$ with the following constructors:

• A function $i:A_0\to {\widehat{A}}_0$.

• For each $a,b:A$ and $e:a\cong b$, an equality $je:ia=ib$.

• For each $a:A$, an equality $j(1_a)={\mathrm{𝗋𝖾𝖿𝗅}}_{ia}$.

• For each $(a,b,c:A)$, $(f:a\cong b)$, and $(g:b\cong c)$, an equality $j(g\circ f)=j(f)j(g)$.

• 1-truncation: for all $x,y:{\widehat{A}}_0$ and $p,q:x=y$ and $r,s:p=q$, an equality $r=s$.

Note that for any $a,b:A$ and $p:a=b$, we have $j(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p))=i\left(p\right)$. This follows by path induction on $p$ and the third constructor.

The type ${\widehat{A}}_0$ will be the type of objects of $\widehat{A}$; we now build all the rest of the structure. (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant: it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked.)

Step 1: We define a family ${\mathrm{hom}}_{\widehat{A}}:{\widehat{A}}_0\to {\widehat{A}}_0\to$ by double induction on ${\widehat{A}}_0$. Since is a 1-type, we can ignore the 1-truncation constructor. When $x$ and $y$ are of the form $ia$ and $ib$, we take ${\mathrm{hom}}_{\widehat{A}}(ia,ib):\equiv {\mathrm{hom}}_A(a,b)$. It remains to consider all the other possible pairs of constructors.

Let us keep $x=ia$ fixed at first. If $y$ varies along the identity $je:ib=i{b}^{\prime }$, for some $e:b\cong b^{\prime }$, we require an identity ${\mathrm{hom}}_A(a,b)={\mathrm{hom}}_A(a,b^{\prime })$. By univalence, it suffices to give an equivalence ${\mathrm{hom}}_A(a,b)\simeq {\mathrm{hom}}_A(a,b^{\prime })$. We take this to be the function $(e\circ \text{–}):{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_A(a,b^{\prime })$. To see that this is an equivalence, we give its inverse as $(e^{-1}\circ \text{–})$, with witnesses to inversion coming from the fact that $e^{-1}$ is the inverse of $e$ in $A$.

As $y$ varies along the identity $j(1_b)={\mathrm{𝗋𝖾𝖿𝗅}}_{ib}$, we require an identity $(1_b\circ \text{–})={\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{hom}}_A(a,b)}$; this follows from the identity axiom $1_b\circ g=g$ of a precategory. Similarly, as $y$ varies along the identity $j(g\circ f)=j(f)j(g)$, we require an identity $((g\circ f)\circ \text{–})=(g\circ (f\circ \text{–}))$, which follows from associativity.

Now we consider the other constructors for $x$. Say that $x$ varies along the identity $j(e):ia=i{a}^{\prime }$, for some $e:a\cong a^{\prime }$; we again must deal with all the constructors for $y$. If $y$ is $ib$, then we require an identity ${\mathrm{hom}}_A(a,b)={\mathrm{hom}}_A(a^{\prime },b)$. By univalence, this may come from an equivalence, and for this we can use $(\text{–}\circ e^{-1})$, with inverse $(\text{–}\circ e)$.

Still with $x$ varying along $j(e)$, suppose now that $y$ also varies along $j(f)$ for some $f:b\cong b^{\prime }$. Then we need to know that the two concatenated identities

$${\mathrm{hom}}_A(a,b)={\mathrm{hom}}_A(a^{\prime },b)={\mathrm{hom}}_A(a^{\prime },b^{\prime })\mathit{\hspace{1em}\hspace{1em}}\text{and}$$

$${\mathrm{hom}}_A(a,b)={\mathrm{hom}}_A(a,b^{\prime })={\mathrm{hom}}_A(a^{\prime },b^{\prime })$$

are identical. This follows from associativity: $(f\circ \text{–})\circ e^{-1}=f\circ (\text{–}\circ e^{-1})$. The other two constructors for $y$ are trivial, since they are 2-fold equalities in sets.

For the next two constructors of $x$, all but the first constructor for $y$ is likewise trivial. When $x$ varies along $j(1_a)={\mathrm{𝗋𝖾𝖿𝗅}}_{ia}$ and $y$ is $ib$, we use the identity axiom again. Similarly, when $x$ varies along $j(g\circ f)=j(f)j(g)$, we use associativity again. This completes the construction of ${\mathrm{hom}}_{\widehat{A}}:{\widehat{A}}_0\to {\widehat{A}}_0\to$.

Step 2: We give the precategory structure on $\widehat{A}$, always by induction on ${\widehat{A}}_0$. We are now eliminating into sets (the hom-sets of $\widehat{A}$), so all but the first two constructors are trivial to deal with.

For identities, if $x$ is $ia$ then we have ${\mathrm{hom}}_{\widehat{A}}(x,x)\equiv {\mathrm{hom}}_A(a,a)$ and we define $1_x:\equiv 1_{ia}$. If $x$ varies along $je$ for $e:a\cong a^{\prime }$, we must show that ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto {\mathrm{hom}}_{\widehat{A}}(x,x)}(je,1_{ia})=1_{i{a}^{\prime }}$. But by definition of ${\mathrm{hom}}_{\widehat{A}}$, transporting along $je$ is given by composing with $e$ and $e^{-1}$, and we have $e\circ 1_{ia}\circ e^{-1}=1_{i{a}^{\prime }}$.

For composition, if $x,y,z$ are $ia,ib,ic$ respectively, then ${\mathrm{hom}}_{\widehat{A}}$ reduces to ${\mathrm{hom}}_A$ and we can define composition in $\widehat{A}$ to be composition in $A$. And when $x$, $y$, or $z$ varies along $je$, then we verify the following equalities:

$e\circ (g\circ f)$ $=(e\circ g)\circ f,$

$g\circ f$ $=(g\circ e^{-1})\circ (e\circ f),$

$(g\circ f)\circ e^{-1}$ $=g\circ (f\circ e^{-1}).$

Finally, the associativity and unitality axioms are mere propositions, so all constructors except the first are trivial. But in that case, we have the corresponding axioms in $A$.

Step 3: We show that $\widehat{A}$ is a category. That is, we must show that for all $x,y:\widehat{A}$, the function $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}:(x=y)\to (x\cong y)$ is an equivalence. First we define, for all $x,y:\widehat{A}$, a function $k_{x,y}:(x\cong y)\to (x=y)$ by induction. As before, since our goal is a set, it suffices to deal with the first two constructors.

When $x$ and $y$ are $ia$ and $ib$ respectively, we have ${\mathrm{hom}}_{\widehat{A}}(ia,ib)\equiv {\mathrm{hom}}_A(a,b)$, with composition and identities inherited as well, so that $(ia\cong ib)$ is equivalent to $(a\cong b)$. But now we have the constructor $j:(a\cong b)\to (ia=ib)$.

Next, if $y$ varies along $j(e)$ for some $e:b\cong b^{\prime }$, we must show that for $f:a\cong b$ we have $j(j{(e)}_{*}\left(f\right))=j(f)j(e)$. But by definition of ${\mathrm{hom}}_{\widehat{A}}$ on equalities, transporting along $j(e)$ is equivalent to post-composing with $e$, so this equality follows from the last constructor of ${\widehat{A}}_0$. The remaining case when $x$ varies along $j(e)$ for $e:a\cong a^{\prime }$ is similar. This completes the definition of $k:{\prod }_{(x,y:{\widehat{A}}_0)}(x\cong y)\to (x=y)$.

Now one thing we must show is that if $p:x=y$, then $k(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p))=p$. By induction on $p$, we may assume it is ${\mathrm{𝗋𝖾𝖿𝗅}}_x$, and hence $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p)\equiv 1_x$. Now we argue by induction on $x:{\widehat{A}}_0$, and since our goal is a mere proposition (since ${\widehat{A}}_0$ is a 1-type), all constructors except the first are trivial. But if $x$ is $ia$, then $k(1_{ia})\equiv j(1_a)$, which is equal to ${\mathrm{𝗋𝖾𝖿𝗅}}_{ia}$ by the third constructor of ${\widehat{A}}_0$.

To complete the proof that $\widehat{A}$ is a category, we must show that if $f:x\cong y$, then $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(k(f))=f$. By induction we may assume that $x$ and $y$ are $ia$ and $ib$ respectively, in which case $f$ must arise from an isomorphism $g:a\cong b$ and we have $k(f)\equiv j(g)$. However, for any $p$ we have $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p)=p_{*}\left(1\right)$, so in particular $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(j(g))=j{(g)}_{*}\left(1_{ia}\right)$. And by definition of ${\mathrm{hom}}_{\widehat{A}}$ on equalities, this is given by composing $1_{ia}$ with the equivalence $g$, hence is equal to $g$.

Note the similarity of this step to the encode-decode method used in sec:compute-coprod,sec:compute-nat,cha:homotopy. Once again we are characterizing the identity types of a higher inductive type (here, ${\widehat{A}}_0$) by defining recursively a family of codes (here, $(x,y)\mapsto (x\cong y)$) and encoding and decoding functions by induction on ${\widehat{A}}_0$ and on paths.

Step 4: We define a weak equivalence $I:A\to \widehat{A}$. We take $I_0:\equiv i:A_0\to {\widehat{A}}_0$, and by construction of ${\mathrm{hom}}_{\widehat{A}}$ we have functions $I_{a,b}:{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_{\widehat{A}}(Ia,Ib)$ forming a functor $I:A\to \widehat{A}$. This functor is fully faithful by construction, so it remains to show it is essentially surjective. That is, for all $x:\widehat{A}$ we want there to merely exist an $a:A$ such that $Ia\cong x$. As always, we argue by induction on $x$, and since the goal is a mere proposition, all but the first constructor are trivial. But if $x$ is $ia$, then of course we have $a:A$ and $Ia\equiv ia$, hence $Ia\cong ia$. (Note that if we were trying to prove $I$ to be split essentially surjective, we would be stuck, because we know nothing about equalities in $A_0$ and thus have no way to deal with any further constructors.) ∎

We call the construction $A\mapsto \widehat{A}$ the Rezk completion, although there is also an argument (coming from higher topos semantics) for calling it the stack completion.

We have seen that most precategories arising in practice are categories, since they are constructed from $𝒮et$, which is a category by the univalence axiom. However, there are a few cases in which the Rezk completion is necessary to obtain a category.

Example 9.9.6.

Recall from ct:fundgpd that for any type $X$ there is a pregroupoid with $X$ as its type of objects and $\mathrm{hom}\mathrm{(}x\mathrm{,}y\mathrm{)}\mathrm{:}\mathrm{\equiv }\mathrm{\parallel }x\mathrm{=}y{\mathrm{\parallel }}_{\mathrm{0}}$. Its Rezk completion is the fundamental groupoid of $X$. Recalling that groupoids are equivalent to 1-types, it is not hard to identify this groupoid with ${\mathrm{\parallel }X\mathrm{\parallel }}_{\mathrm{1}}$.

Example 9.9.7.

Recall from ct:hoprecat that there is a precategory whose type of objects is $\mathrm{U}$ and with $\mathrm{hom}\mathrm{(}X\mathrm{,}Y\mathrm{)}\mathrm{:}\mathrm{\equiv }\mathrm{\parallel }X\mathrm{\to }Y{\mathrm{\parallel }}_{\mathrm{0}}$. Its Rezk completion may be called the homotopy category of types. Its type of objects can be identified with ${\mathrm{\parallel }\mathrm{U}\mathrm{\parallel }}_{\mathrm{1}}$ (see ct:ex:hocat).

The Rezk completion also allows us to show that the notion of “category” is determined by the notion of “weak equivalence of precategories”. Thus, insofar as the latter is inevitable, so is the former.

Theorem 9.9.8.

A precategory $C$ is a category if and only if for every weak equivalence of precategories $H\mathrm{:}A\mathrm{\to }B$, the induced functor $\mathrm{(}\mathit{\text{–}}\mathrm{\circ }H\mathrm{)}\mathrm{:}{C}^B\mathrm{\to }{C}^A$ is an isomorphism of precategories.

Proof.

“Only if” is ct:cat-weq-eq. In the other direction, let $H$ be $I:A\to \widehat{A}$. Then since ${(\text{–}\circ I)}_0$ is an equivalence, there exists $R:\widehat{A}\to A$ such that $RI=1_A$. Hence $IRI=I$, but again since ${(\text{–}\circ I)}_0$ is an equivalence, this implies $IR=1_{\widehat{A}}$. By ct:isoprecatLABEL:item:ct:ipc3, $I$ is an isomorphism of precategories. But then since $\widehat{A}$ is a category, so is $A$. ∎

Title	9.9 The Rezk completion