## Idea ## There is a canonical way to turn any [[precategory]] into a [[weak equivalence of precategories|weakly equivalent]] [[category]]. This can be thought of as an analogue of [[univalence]] but for [[isomorphism in a precategory|isomorphisms]] instead of [[equivalence of precategories|equivalences]]. ## Construction ## ### Theorem 9.9.5 ### For any [[precategory]] $A$, there is a [[category]] $\hat{A}$ and a [[weak equivalence]] $A\to \hat{A}$. **Proof.** Let $\hat{A}_0$ be the type of [[representable]] objects of $\mathit{Set}^{A^{\mathrm{op}}}$, with hom-sets inherited from $\mathit{Set}^{A^{\mathrm{op}}}$. Then the inclusion $\hat{A} \to \mathit{Set}^{A^{\mathrm{op}}}$ is [[fully faithful]] and an [[embedding on objects]]. Since $\mathit{Set}^{A^{\mathrm{op}}}$ is a category by Theorem 9.2.5 (see [[functor precategory]]), $\hat{A}$ is also a category. Let $A \to \hat{A}$ be the [[Yoneda embedding]]. This is [[fully faithful]] by corollary 9.5.6 (See [[Yoneda embedding]]), and [[essentially surjective]] by definition of $\hat{A}_0$. Thus it is a [[weak equivalence of precategories|weak equivlance]]. $\square$ * $\hat{A}_0\equiv \sum_{(F : \mathit{Set}^{A^{\mathrm{op}}})} \sum_{(a:A)} \mathbf{y} a \cong F$ This has the unfortunate side affect of raising the [[universe]] level. If $A$ is a [[category]] in a universe $\mathcal{U}$, then in this proof $\mathit{Set}$ must at least be as large as $\mathit{Set}_{\mathcal{U}}$. Hence the category $\mathit{Set}_{\mathcal{U}}$ is in a higher universe than $\mathcal{U}$ hence $\mathit{Set}^{A^{\mathrm{op}}}$ must also be in a higher universe and finally $\hat{A}$ is also in a higher universe than $\mathcal{U}$. Now this can all be avoided by constructing a [[higher inductive type]] $\hat{A}$ with constructors: * A function $i : A_0 \to \hat{A}_0$. * For each $a,b:A$ ad $e: a \iso b$, an equality $j e : i a = i b$ * For each $a : A$, an equality $k(1_a)=refl_{i a}$. * For each $a,b,c:A$, $f : a \cong b$, and $g : b \cong c$, an equality $j(g \circ f)=j(f) \centerdot j(g).$ * 1-truncation: for all $x,y:\hat{A}_0$ and $p,q: x = y$ and $r,s : p = q$, an equality $r=s$. If we ignore the last constructor we could also write the above as $\| \hat{A}_0 \|_1$. We now go on to build a category $\hat{A}$ with a [[weak equivalence of precategories|weak equivalence]] $A \to \hat{A}$ by taking the type of objects as $\hat{A}_0$ and defining hom-sets by double [[induction]]. The advantage of this approach is that it preserves [[universe]] levels, there are a lot of things to check but it is an easy proof. The kind of proof that is well suited to a proof assistant. For the complete proof see Theorem 9.9.5 of the [[HoTT book]]. ## See also ## [[Category theory]] [[Yoneda lemma]] [[weak equivalence of precategories]] ## References ## [[HoTT book]] category: category theory