Homotopy Type Theory Rezk completion > history (Rev #3)

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 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 equivlance?. $\square$

• $\hat{A}_0\equiv \sum_{(F : \mathit{Set}^{A^{\mathrm{op}}})} \sum_{(a:A)} \mathbf{y} a \cong F$

See also

Category theory yoneda lemma

References

HoTT book