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 (Functor-is-category Sets-is-category) (γim.embed , γim.embed-is-embedding)) (Ξ» x y β 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))