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) AA^\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)

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)