Homotopy Type Theory
Rezk completion


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 equivalence. \square

This has the unfortunate side affect of raising the universe level. If AA is a category in a universe 𝒰\mathcal{U}, then in this proof Set\mathit{Set} must at least be as large as Set 𝒰\mathit{Set}_{\mathcal{U}}. Hence the category Set 𝒰\mathit{Set}_{\mathcal{U}} is in a higher universe than 𝒰\mathcal{U} hence Set A op\mathit{Set}^{A^{\mathrm{op}}} must also be in a higher universe and finally A^\hat{A} is also in a higher universe than 𝒰\mathcal{U}.

Now this can all be avoided by constructing a higher inductive type A^\hat{A} with constructors:

If we ignore the last constructor we could also write the above as A^ 0 1\| \hat{A}_0 \|_1.

We now go on to build a category A^\hat{A} with a weak equivalence AA^A \to \hat{A} by taking the type of objects as A^ 0\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


HoTT book

category: category theory