open import Cat.Functor.FullSubcategory open import Cat.Instances.Functor open import Cat.Instances.Sets open import Cat.Functor.Hom open import Cat.Prelude module Cat.Univalent.Rezk where
The Rezk completionπ
In the same way that we can freely complete a proset into a poset, it is possible to, in a universal way, replace any precategory by a category , such that there is a weak equivalence (a fully faithful, essentially surjective functor) , such that any map from to a univalent category factors uniquely through .
The construction is essentially piecing together a handful of pre-existing results: The univalence principle for -types implies that Sets is a univalent category, and functor categories with univalent codomain are univalent; The Yoneda lemma implies that any precategory admits a full inclusion into , and full subcategories of univalent categories are univalent β so, like Grothendieck cracking the nut, the sea of theory has risen to the point where our result is trivial:
Rezk-completion : Precategory o h β Precategory (o β lsuc h) (o β h) Rezk-completion A = Full-inclusionβFull-subcat {F = γ A} (γ-is-fully-faithful A) Rezk-completion-is-category : β {A : Precategory o h} β is-category (Rezk-completion A) Rezk-completion-is-category {o} {h} {A} = Restrict-is-category _ (Ξ» _ β squash) (Functor-is-category Sets-is-category)