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)