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 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))