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.
For any precategory , there is a category and a weak equivalence .
Proof. Let be the type of representable? objects of , with hom-sets inherited from . Then the inclusion is fully faithful and an embedding on objects?. Since is a category by Theorem 9.2.5 (see functor category?), is also a category. Let be the Yoneda embedding. This is fully faithful by corollary 9.5.6 (See Yoneda embedding), and essentially surjective by definition of . Thus it is a weak equivlance?.
Revision on September 4, 2018 at 17:20:48 by Ali Caglayan. See the history of this page for a list of all contributions to it.