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{\u2013}\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{\u2013}}\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{\u220e}$$ 
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{\u2013}}\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 categoryness 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 settheoretic foundations this is not a sufficient amount of uniqueness to give us a function without invoking $\mathrm{\U0001d5a0\U0001d5a2}$. 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{\u2013}}\mathrm{\circ}H\mathrm{)}\mathrm{:}{C}^{B}\mathrm{\to}{C}^{A}$ is an isomorphism.
Proof.
By \autorefct:functorcat, ${C}^{B}$ and ${C}^{A}$ are categories. Thus, by \autorefct:eqvlevelwise it will suffice to show that $(\text{\u2013}\circ H)$ is an equivalence. But since we know from the preceding two lemmas that it is fully faithful, by \autorefct: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 homsets 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 \text{setof}F:\mathcal{S}e{t}^{{A}^{\mathrm{op}}}\exists (a:A).(\mathbf{y}a\cong F)$, with homsets inherited from $\mathcal{S}e{t}^{{A}^{\mathrm{op}}}$. Then the inclusion $\widehat{A}\to \mathcal{S}e{t}^{{A}^{\mathrm{op}}}$ is fully faithful and an embedding on objects. Since $\mathcal{S}e{t}^{{A}^{\mathrm{op}}}$ is a category (by \autorefct:functorcat, since $\mathcal{S}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 \autorefct:yonedaembedding, 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 $\mathcal{U}$, then in this proof $\mathcal{S}et$ must be at least as large as $\mathcal{S}e{t}_{\mathcal{U}}$. Then $\mathcal{S}e{t}_{\mathcal{U}}$ and ${(\mathcal{S}e{t}_{\mathcal{U}})}^{{A}^{\mathrm{op}}}$ are not themselves categories in $\mathcal{U}$, 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{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{ia}$.

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

•
1truncation: 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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(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 \text{set}$ by double induction on ${\widehat{A}}_{0}$. Since \setis a 1type, we can ignore the 1truncation 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{\u2013}):{\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{\u2013})$, 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{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{ib}$, we require an identity $({1}_{b}\circ \text{\u2013})={\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{{\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)\text{centerdot}j(g)$, we require an identity $((g\circ f)\circ \text{\u2013})=(g\circ (f\circ \text{\u2013}))$, 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{\u2013}\circ {e}^{1})$, with inverse $(\text{\u2013}\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})\text{mathrlap}\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{\u2013})\circ {e}^{1}=f\circ (\text{\u2013}\circ {e}^{1})$. The other two constructors for $y$ are trivial, since they are 2fold 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{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{ia}$ and $y$ is $ib$, we use the identity axiom again. Similarly, when $x$ varies along $j(g\circ f)=j(f)\text{centerdot}j(g)$, we use associativity again. This completes the construction of ${\mathrm{hom}}_{\widehat{A}}:{\widehat{A}}_{0}\to {\widehat{A}}_{0}\to \text{set}$.
Step 2: We give the precategory structure on $\widehat{A}$, always by induction on ${\widehat{A}}_{0}$. We are now eliminating into sets (the homsets 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{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}:(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)\text{centerdot}j(e)$. But by definition of ${\mathrm{hom}}_{\widehat{A}}$ on equalities, transporting along $j(e)$ is equivalent to postcomposing 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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(p))=p$. By induction on $p$, we may assume it is ${\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{x}$, and hence $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(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 1type), 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{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(p)={p}_{*}\left(1\right)$, so in particular $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(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 encodedecode method used in \autorefsec:computecoprod,sec:computenat,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 $\mathcal{S}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 \autorefct: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 1types, it is not hard to identify this groupoid with ${\mathrm{\parallel}X\mathrm{\parallel}}_{\mathrm{1}}$.
Example 9.9.7.
Recall from \autorefct: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 \autorefct: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{\u2013}}\mathrm{\circ}H\mathrm{)}\mathrm{:}{C}^{B}\mathrm{\to}{C}^{A}$ is an isomorphism of precategories.
Proof.
“Only if” is \autorefct:catweqeq. In the other direction, let $H$ be $I:A\to \widehat{A}$. Then since ${(\text{\u2013}\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{\u2013}\circ I)}_{0}$ is an equivalence, this implies $IR={1}_{\widehat{A}}$. By \autorefct: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 

\metatable 