Homotopy Type Theory
Rezk completion (Rev #2)


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?.


Theorem 9.9.5

For any precategory AA, there is a category A^\hat{A} and a weak equivalence AA^A\to \hat{A}.

Proof. Let A^ 0\hat{A}_0 be the type of representable? objects of Set A op\mathit{Set}^{A^{\mathrm{op}}}, with hom-sets inherited from Set A op\mathit{Set}^{A^{\mathrm{op}}}. Then the inclusion A^Set A op\hat{A} \to \mathit{Set}^{A^{\mathrm{op}}} is fully faithful and an embedding on objects?. Since Set A op\mathit{Set}^{A^{\mathrm{op}}} is a category by Theorem 9.2.5 (see functor precategory), A^\hat{A} is also a category. Let AA^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 A^ 0\hat{A}_0. Thus it is a weak equivlance?. \square

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


HoTT book

category: category theory

Revision on September 4, 2018 at 15:22:26 by Ali Caglayan. See the history of this page for a list of all contributions to it.