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\mathcal{A} by a category A^\widehat{\mathcal{A}}, such that there is a weak equivalence (a fully faithful, essentially surjective functor) A→A^\mathcal{A} \to \widehat{\mathcal{A}}, such that any map from A\mathcal{A} to a univalent category C\mathcal{C} factors uniquely through A^\widehat{\mathcal{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\mathcal{A} admits a full inclusion into [Aop,Sets][\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 A\mathcal{A} with objects living in a universe oo and homs in hh, we now have A^\widehat{\mathcal{A}} with objects living in oβŠ”(1+h)o \sqcup (1 + h).

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

Since PSh(A)\mathrm{PSh}(\mathcal{A}) is a category, isomorphism is an identity system on its objects, which lives at the level of its morphisms β€” oβŠ”ho \sqcup h β€” rather than of its objects, oβŠ”(1+h)o \sqcup (1 + h). Therefore, using the construction of small images, we may take imβ‘γ‚ˆA\operatorname*{im}γ‚ˆ_{\mathcal{A}} to be a oβŠ”ho \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 A^\widehat{\mathcal{A}} factors the Yoneda embedding γ‚ˆAγ‚ˆ_\mathcal{A} as a functor

Aβ†’βˆΌA^β†ͺPSh(A) \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 PSh(A)\mathrm{PSh}(\mathcal{A}) to one on A^\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 β€œPSh(A)\mathrm{PSh}(\mathcal{A})-isomorphisms on the image of the functor A^β†ͺPSh(A)\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 Aβ†’A^\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))