Showing changes from revision #8 to #9:
Added | Removed | Changed
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 precategory), 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 equivalence.
This has the unfortunate side affect of raising the universe level. If is a category in a universe , then in this proof must at least be as large as . Hence the category is in a higher universe than hence must also be in a higher universe and finally is also in a higher universe than .
Now this can all be avoided by constructing a higher inductive type with constructors:
If we ignore the last constructor we could also write the above as .
We now go on to build a category with a weak equivalence by taking the type of objects as 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.
Category theory Yoneda lemma weak equivalence of precategories