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

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

  : βˆ€ {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)