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 $\ca{A}$ by a category $\widehat{\ca{A}}$, such that there is a weak equivalence (a fully faithful, essentially surjective functor) $\ca{A} \to \widehat{\ca{A}}$, such that any map from $\ca{A}$ to a univalent category $\ca{C}$ factors uniquely through $\widehat{\ca{A}}$.

The construction is essentially piecing together a handful of pre-existing results: The univalence principle for $n$-types implies that Sets is a univalent category, and functor categories with univalent codomain are univalent; The Yoneda lemma implies that any precategory $\ca{A}$ admits a full inclusion into $[\ca{A}\op, \sets]$, 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)