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 {D = Sets _} Sets-is-category)