open import Cat.Functor.FullSubcategory open import Cat.Instances.Functor open import Cat.Instances.Sets open import Cat.Functor.Base open import Cat.Functor.Hom open import Cat.Prelude open import Data.Image import Cat.Functor.Reasoning.FullyFaithful as Ffr import Cat.Reasoning as Cr 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 $\mathcal{A}$ by a category $\widehat{\mathcal{A}}$, such that there is a weak equivalence (a fully faithful, essentially surjective functor) $\mathcal{A} \to \widehat{\mathcal{A}}$, such that any map from $\mathcal{A}$ to a univalent category $\mathcal{C}$ factors uniquely through $\widehat{\mathcal{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 $\mathcal{A}$ admits a full inclusion into $[\mathcal{A}{^{{\mathrm{op}}}}, {{\mathbf{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:

module Rezk-large (A : Precategory o h) where Rezk-completion : Precategory (o β lsuc h) (o β h) Rezk-completion = Full-inclusionβFull-subcat {F = γ A} (γ-is-fully-faithful A) Rezk-completion-is-category : is-category Rezk-completion Rezk-completion-is-category = Restrict-is-category _ (Ξ» _ β squash) (Functor-is-category Sets-is-category) Complete : Functor A Rezk-completion Complete = Ff-domainβFull-subcat {F = γ A} (γ-is-fully-faithful A) Complete-is-ff : is-fully-faithful Complete Complete-is-ff = is-fully-faithful-domainβFull-subcat {F = γ _} (γ-is-fully-faithful _) Complete-is-eso : is-eso Complete Complete-is-eso = is-eso-domainβFull-subcat {F = γ _} (γ-is-fully-faithful _)

However, this construction is a bit disappointing, because weβve had
to pass to a *larger* universe than the one we started with. If
originally we had
$\mathcal{A}$
with objects living in a universe
$o$
and homs in
$h$,
we now have
$\widehat{\mathcal{A}}$
with objects living in
$o \sqcup (1 + h)$.

Itβs unavoidable that the objects in $\widehat{\mathcal{A}}$ will live in an universe $\widehat{o}$ satisfying $(o \sqcup h) \le \widehat{o}$, since we want their identity type to be equivalent to something living in $h$, but going up a level is unfortunate. However, itβs also avoidable!

Since ${{\mathrm{PSh}}}(\mathcal{A})$ is a category, isomorphism is an identity system on its objects, which lives at the level of its morphisms β $o \sqcup h$ β rather than of its objects, $o \sqcup (1 + h)$. Therefore, using the construction of small images, we may take $\operatorname*{im}{γ}_{\mathcal{A}}$ to be a $o \sqcup h$-type!

module _ (A : Precategory o h) where private PSh[A] = PSh h A module PSh[A] = Precategory PSh[A] PSh[A]-is-cat : is-category PSh[A] PSh[A]-is-cat = Functor-is-category Sets-is-category module γim = Replacement PSh[A]-is-cat (γβ A) Rezk-completion : Precategory (o β h) (o β h) Rezk-completion .Ob = γim.Image Rezk-completion .Hom x y = γim.embed x => γim.embed y Rezk-completion .Hom-set _ _ = PSh[A].Hom-set _ _ Rezk-completion .id = PSh[A].id Rezk-completion ._β_ = PSh[A]._β_ Rezk-completion .idr = PSh[A].idr Rezk-completion .idl = PSh[A].idl Rezk-completion .assoc = PSh[A].assoc

Our resized Rezk completion $\widehat{\mathcal{A}}$ factors the Yoneda embedding ${γ}_\mathcal{A}$ as a functor

$\mathcal{A} {\xrightarrow{\sim}} \widehat{\mathcal{A}} {\hookrightarrow}{{\mathrm{PSh}}}(\mathcal{A})$

where the first functor is a weak equivalence, and the second functor is fully faithful. Letβs first define the functors:

complete : Functor A Rezk-completion complete .Fβ = γim.inc complete .Fβ = γ A .Fβ complete .F-id = γ A .F-id complete .F-β = γ A .F-β RezkβͺPSh : Functor Rezk-completion (PSh h A) RezkβͺPSh .Fβ = γim.embed RezkβͺPSh .Fβ f = f RezkβͺPSh .F-id = refl RezkβͺPSh .F-β _ _ = refl

From the existence of the second functor, we can piece together pre-existing lemmas about the image and about identity systems in general to show that this resized Rezk completion is also a category: We can pull back the identity system on ${{\mathrm{PSh}}}(\mathcal{A})$ to one on $\widehat{\mathcal{A}}$, since we know of a (type-theoretic) embedding between their types of objects.

That gives us an identity system which is slightly off, that of β${{\mathrm{PSh}}}(\mathcal{A})$-isomorphisms on the image of the functor $\widehat{\mathcal{A}} {\hookrightarrow}{{\mathrm{PSh}}}(\mathcal{A})$β, but since we know that this functor is fully faithful, thatβs equivalent to what we want.

private module RezkβͺPSh = Ffr RezkβͺPSh id-equiv abstract Rezk-completion-is-category : is-category Rezk-completion Rezk-completion-is-category = transfer-identity-system (pullback-identity-system PSh[A]-is-cat (_ , γim.embed-is-embedding)) (Ξ» _ _ β RezkβͺPSh.iso-equiv eβ»ΒΉ) Ξ» x β Cr.β -pathp Rezk-completion refl refl refl

It remains to show that the functor
$\mathcal{A} \to \widehat{\mathcal{A}}$
is a weak equivalence. Itβs fully faithful because the Yoneda embedding
is, and itβs essentially surjective because itβs *literally*
surjective-on-objects.

complete-is-ff : is-fully-faithful complete complete-is-ff = γ-is-fully-faithful A complete-is-eso : is-eso complete complete-is-eso x = do t β γim.inc-is-surjective x pure (t .fst , pathβiso (t .snd))