## Idea ## There is a canonical way to turn any [[precategory]] into a [[weakly equivalent]] [[category]]. This can be thought of as an analogue of [[univalence]] but for [[isomorphisms]] instead of [[equivalences]]. ## Defintion ## ### 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 category]]), $\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 equivlance]]. $\square$ * $\hat{A}_0\equiv \sum_{(F : \mathit{Set}^{A^{\mathrm{op}}})} \sum_{(a:A)} \mathbf{y} a \cong F$ ## References ## [[HoTT book]] category: category theory