# Homotopy Type Theory Rezk completion (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## 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?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$

## References

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.