module Cat.Univalent.Rezk.Universal where

Universal property of the Rezk completionπŸ”—

With the Rezk completion, we defined, for any precategory C\mathcal{C}, a univalent category C+\mathcal{C}^+, together with a weak equivalence functor R:C→C+R : \mathcal{C} \to \mathcal{C}^+. We also stated, but did not in that module prove, the universal property of the Rezk completion: The functor RR is the universal map from C\mathcal{C} to categories. This module actually proves it, but be warned: the proof is very technical, and is mostly a calculation.

In generic terms, universality of the Rezk completion follows from univalent categories being the class of local objects for the weak equivalences1: A category C\mathcal{C} is univalent precisely if any weak equivalence H:Aβ†’BH : \mathcal{A} \to \mathcal{B} induces2 a proper equivalence of categories βˆ’βˆ˜H:[B,C]β†’[A,C]- \circ H : [\mathcal{B},\mathcal{C}] \to [\mathcal{A},\mathcal{C}].

The high-level overview of the proof is as follows:

  • For any eso H:Aβ†’BH : \mathcal{A} \to \mathcal{B}, and for any C\mathcal{C}, all precategories, the functor βˆ’βˆ˜H:[A,B]β†’[B,C]- \circ H : [\mathcal{A},\mathcal{B}] \to [\mathcal{B},\mathcal{C}] is faithful. This is the least technical part of the proof, so we do it first.

  • If HH is additionally full, then βˆ’βˆ˜H- \circ H is fully faithful.

  • If HH is a weak equivalence, and C\mathcal{C} is univalent, then βˆ’βˆ˜H- \circ H is essentially surjective. By the principle of unique choice, it is an equivalence, and thus3 an isomorphism.

FaithfulnessπŸ”—

The argument here is almost elementary: We’re given a witness that Ξ³H=Ξ΄H\gamma H = \delta H, so all we have to do is manipulate the expression Ξ³b\gamma_b to something which has a Ξ³H\gamma H subexpression. Since HH is eso, given b:Bb : \mathcal{B}, we can find a:Aa : \mathcal{A} and an iso m:Haβ‰…bm : Ha \cong b, from which we can calculate:

eso→pre-faithful
  : (H : Functor A B) {F G : Functor B C}
  β†’ is-eso H β†’ (Ξ³ Ξ΄ : F => G)
  β†’ (βˆ€ b β†’ Ξ³ .Ξ· (H .Fβ‚€ b) ≑ Ξ΄ .Ξ· (H .Fβ‚€ b)) β†’ Ξ³ ≑ Ξ΄
eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p =
  Nat-path Ξ» b β†’ βˆ₯-βˆ₯-proj {ap = C.Hom-set _ _ _ _} do
  (bβ€² , m) ← h-eso b
  βˆ₯_βˆ₯.inc $
    Ξ³ .Ξ· b                                      β‰‘βŸ¨ C.intror (F-map-iso F m .invl) βŸ©β‰‘
    Ξ³ .Ξ· b C.∘ F.₁ (m .to) C.∘ F.₁ (m .from)    β‰‘βŸ¨ C.extendl (Ξ³ .is-natural _ _ _) βŸ©β‰‘
    G.₁ (m .to) C.∘ Ξ³ .Ξ· _ C.∘ F.₁ (m .from)    β‰‘βŸ¨ apβ‚‚ C._∘_ refl (apβ‚‚ C._∘_ (p bβ€²) refl) βŸ©β‰‘
    G.₁ (m .to) C.∘ Ξ΄ .Ξ· _ C.∘ F.₁ (m .from)    β‰‘βŸ¨ C.extendl (sym (Ξ΄ .is-natural _ _ _)) βŸ©β‰‘
    Ξ΄ .Ξ· b C.∘ F.₁ (m .to) C.∘ F.₁ (m .from)    β‰‘βŸ¨ C.elimr (F-map-iso F m .invl) βŸ©β‰‘
    δ .η b                                      ∎
  where module C = Cat.Reasoning C
        module F = Functor F
        module G = Functor G

The above is, unfortunately, the simplest result in this module. The next two proofs are both quite technical: that’s because we’re given some mere4 data, from the assumption that HH is a weak equivalence, so to use it as proper data, we need to show that whatever we want lives in a contractible space, after which we are free to project only the data we are interested in, and forget about the coherences.

It will turn out, however, that the coherence data necessary to make these types contractible is exactly the coherence data we need to show that we are indeed building functors, natural transformations, etc. So, not only do we need it to use unique choice, we also need it to show we’re doing category theory.

Full-faithfulnessπŸ”—

Let AA, BB, CC and HH be as before, except now assume that HH is full (in addition to eso).

eso-full→pre-ff
  : (H : Functor A B)
  β†’ is-eso H β†’ is-full H
  β†’ is-fully-faithful {C = Cat[ B , C ]} (precompose H)
eso-full→pre-ff {A = A} {B = B} {C = C} H H-eso H-full = res where

We will show that, for every natural transformation Ξ³:FHβ†’GH\gamma : FH \to GH, and each b:Bb : \mathcal{B}, there is a contractible type of β€œcomponent data” over bb. These data consist of morphisms g:Fbβ†’Gbg : Fb \to Gb, each equipped with a witness that gg acts naturally when faced with isomorphisms Haβ‰…bHa \cong b.

In more detail, if we’re given an essential fibre (a,f)(a,f) of HH over bb, we can use ff to β€œmatch up” our component gg with the components of the natural transformation Ξ³\gamma: since Ξ³a:FH(a)β†’FG(a)\gamma_a : FH(a) \to FG(a), we’ve claimed to have a Fbβ†’GbFb \to Gb, and someone has just handed us a H(a)β‰…bH(a) \cong b, then it darn well better be the case that Ξ³\gamma is

FH(a)β†’FfFbβ†’gGbβ†’Gfβˆ’1FG(a). FH(a) \xrightarrow{Ff} Fb \xrightarrow{g} Gb \xrightarrow{Gf^{-1}} FG(a)\text{.}

    T : B.Ob β†’ Type _
    T b = Ξ£ (C.Hom (F.β‚€ b) (G.β‚€ b)) Ξ» g β†’
      (a : A.Ob) (f : H.β‚€ a B.β‰… b) β†’
      Ξ³.Ξ· a ≑ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to)

We’ll first show that components exist at all. Assume that we have some b:Bb : \mathcal{B} and an essential fibre (a0,h0)(a_0, h_0) of HH over it5. In this situation, guided by the compatibility condition (and isomorphisms being just the best), we can actually define the component to be β€œwhatever satisfies compatibility at (a0,h0)(a_0,h_0),” and a short calculation establishes that defining

      g = G.₁ h.to C.∘ Ξ³.Ξ· aβ‚€ C.∘ F.₁ h.from

is indeed a possible choice. We present the formalisation below, but do not comment on the calculation, leaving it to the curious reader to load this file in Agda and poke around the proof.

      lemma : (a : A.Ob) (f : H.β‚€ a B.β‰… b)
            β†’ Ξ³.Ξ· a ≑ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to)
      lemma a f = βˆ₯-βˆ₯-proj {ap = C.Hom-set _ _ _ _} do
        (k , p)   ← H-full (h.from B.∘ B.to f)
        (k⁻¹ , q) ← H-full (B.from f B.∘ h.to)
        βˆ₯_βˆ₯.inc $
             C.intror (F.annihilate
               (apβ‚‚ B._∘_ q p Β·Β· B.cancel-inner h.invl Β·Β· f .invr))
          Β·Β· C.extendl (Ξ³.is-natural _ _ _)
          Β·Β· apβ‚‚ (Ξ» e eβ€² β†’ G.₁ e C.∘ Ξ³.Ξ· aβ‚€ C.∘ F.₁ eβ€²) q p
          Β·Β· apβ‚‚ (Ξ» e eβ€² β†’ e C.∘ Ξ³.Ξ· aβ‚€ C.∘ eβ€²) (G.F-∘ _ _) (F.F-∘ _ _)
          Β·Β· C.pullr (ap (G.₁ h.to C.∘_) (C.pulll refl) βˆ™ C.pulll refl)

Anyway, because of how we’ve phrased the coherence condition, if gg, gβ€²g' both satisfy it, then we have Ξ³\gamma equal to both G(h)gF(hβˆ’1)G(h)gF(h^{-1}) and G(h)gβ€²F(hβˆ’1)G(h)g'F(h^{-1}).6 Since isomorphisms are both monic and epic, we can cancel G(h)G(h) and F(hβˆ’1)F(h^{-1}) from these equations to conclude g=gβ€²g = g'. Since the coherence condition is a proposition, the type of component data over bb is a proposition.

    T-prop : βˆ€ b β†’ is-prop (T b)
    T-prop b (g , coh) (gβ€² , cohβ€²) =
      Ξ£-prop-path (Ξ» x β†’ Ξ -is-hlevelΒ² 1 Ξ» _ _ β†’ C.Hom-set _ _ _ _) $
        βˆ₯-βˆ₯-proj {ap = C.Hom-set _ _ _ _} do
        (aβ‚€ , h) ← H-eso b
        pure $ C.iso→epic (F-map-iso F h) _ _
          (C.isoβ†’monic (F-map-iso G (h B.Iso⁻¹)) _ _
            (sym (coh aβ‚€ h) βˆ™ cohβ€² aβ‚€ h))

Given any bb, HH being eso means that we merely have an essential fibre (a,h)(a,h) of HH over bb. But since the type of components over bb is a proposition, if we’re going to use it to construct a component over bb, then we are granted the honour of actually getting hold of an (a,h)(a,h) pair.

    mkTβ€² : βˆ€ b β†’ βˆ₯ Essential-fibre H b βˆ₯ β†’ βˆ₯ T b βˆ₯
    mkTβ€² b he = do
      (aβ‚€ , h) ← he
      βˆ₯_βˆ₯.inc (Mk.g b aβ‚€ h , Mk.lemma b aβ‚€ h)

    mkT : βˆ€ b β†’ T b
    mkT b = βˆ₯-βˆ₯-proj {ap = T-prop b} (mkTβ€² b (H-eso b))

Another calculation shows that, since HH is full, given any pair of essential fibres (a,h)(a, h) over bb and (aβ€²,hβ€²)(a', h') over bβ€²b', with a mediating map f:bβ†’bβ€²f : b \to b', we can choose a map k:Haβ†’Haβ€²k : Ha \to Ha' satisfying Hk=hβ€²fhHk = h'fh, and since both the components at bb and bb β€œcome from Ξ³\gamma” (which is natural), we get a naturality result for the transformation we’re defining, too.

That computation is a bit weirder, so it’s hidden in this <details> tag.
    module
      _ {b bβ€²} (f : B.Hom b bβ€²) (a aβ€² : A.Ob)
        (h : H.β‚€ a B.β‰… b) (hβ€² : H.β‚€ aβ€² B.β‰… bβ€²)
      where
      private
        module hβ€² = B._β‰…_ hβ€²
        module h = B._β‰…_ h

      naturality : _
      naturality = βˆ₯-βˆ₯-proj {ap = C.Hom-set _ _ _ _} do
        (k , p) ← H-full (hβ€².from B.∘ f B.∘ h.to)
        pure $ C.pullr (C.pullr (F.weave (sym
                  (B.pushl p βˆ™ apβ‚‚ B._∘_ refl (B.cancelr h.invl)))))
            Β·Β· apβ‚‚ C._∘_ refl (C.extendl (Ξ³.is-natural _ _ _))
            Β·Β· C.extendl (G.weave (B.lswizzle p hβ€².invl))

Because of this naturality result, all the components we’ve chosen piece together into a natural transformation. And since we defined Ξ΄\delta parametrically over the choice of essential fibre, if we’re looking at some HbHb, then we can choose the identity isomorphism, from which it falls out that Ξ΄H=Ξ³\delta H = \gamma. Since we had already established that βˆ’βˆ˜H- \circ H is faithful, and now we’ve shown it is full, it is fully faithful.

    Ξ΄ : F => G
    Ξ΄ .Ξ· b = mkT b .fst
    Ξ΄ .is-natural b bβ€² f = βˆ₯-βˆ₯-elimβ‚‚
      {P = Ξ» Ξ± Ξ² β†’ βˆ₯-βˆ₯-proj {ap = T-prop bβ€²} (mkTβ€² bβ€² Ξ±) .fst C.∘ F.₁ f
                 ≑ G.₁ f C.∘ βˆ₯-βˆ₯-proj {ap = T-prop b} (mkTβ€² b Ξ²) .fst}
      (Ξ» _ _ β†’ C.Hom-set _ _ _ _)
      (Ξ» (aβ€² , hβ€²) (a , h) β†’ naturality f a aβ€² h hβ€²) (H-eso bβ€²) (H-eso b)

  full : is-full (precompose H)
  full {x = x} {y = y} Ξ³ = pure (Ξ΄ _ _ Ξ³ , Nat-path p) where
    p : βˆ€ b β†’ Ξ΄ _ _ Ξ³ .Ξ· (H.β‚€ b) ≑ Ξ³ .Ξ· b
    p b = subst
      (Ξ» e β†’ βˆ₯-βˆ₯-proj {ap = T-prop _ _ Ξ³ (H.β‚€ b)} (mkTβ€² _ _ Ξ³ (H.β‚€ b) e) .fst
           ≑ Ξ³ .Ξ· b)
      (squash (inc (b , B.id-iso)) (H-eso (H.β‚€ b)))
      (C.eliml (y .F-id) βˆ™ C.elimr (x .F-id))

  res : is-fully-faithful (precompose H)
  res = full+faithful→ff (precompose H) full λ {F} {G} {γ} {δ} p →
    esoβ†’pre-faithful H H-eso Ξ³ Ξ΄ Ξ» b β†’ p Ξ·β‚š b

Essential surjectivityπŸ”—

The rest of the proof proceeds in this same way: Define a type which characterises, up to a compatible space of choices, first the action on morphisms of a functor which inverts βˆ’βˆ˜H- \circ H, and in terms of this type, the action on morphisms. It’s mostly the same trick as above, but a lot wilder. We do not comment on it too extensively: the curious reader, again, can load this file in Agda and play around.

The type of object-candidates Obs is indexed by a b:Bb : \mathcal{B}, and any object candidate cc must come with a family of isomorphisms khk_h giving, for every way of expressing bb as coming from HaHa, a way of cc coming from FaFa. To show this type is a proposition, we additionally require a naturality condition for these isomorphisms.

  private module _ (F : Functor A C) where
    private module F = FR F

    Obs : B.Ob β†’ Type _
    Obs b =
      Ξ£ C.Ob Ξ» c β†’
      Ξ£ ((a : A.Ob) (h : H.β‚€ a B.β‰… b) β†’ F.β‚€ a C.β‰… c) Ξ» k β†’
      ((a , h) (aβ€² , hβ€²) : Essential-fibre H b) (f : A.Hom a aβ€²) β†’
      hβ€² .to B.∘ H.₁ f ≑ h .to β†’
      k aβ€² hβ€² .to C.∘ F.₁ f ≑ k a h .to

Note that we can derive an object candidate over bb from a fibre (a,h)(a,h) of HH over bb. Moreover, this choice is a center of contraction, so we can once more apply unique choice and the assumption that HH is eso to conclude that every b:Bb : \mathcal{B} has an object candidate over it.

    objβ€² : βˆ€ {b} β†’ Essential-fibre H b β†’ Obs b
    objβ€² (aβ‚€ , hβ‚€) .fst = F.β‚€ aβ‚€
    objβ€² (aβ‚€ , hβ‚€) .snd .fst a h = F-map-iso F (H.iso.from (h B.∘Iso (hβ‚€ B.Iso⁻¹)))
    objβ€² (aβ‚€ , hβ‚€) .snd .snd (a , h) (aβ€² , hβ€²) f p = F.collapse (H.ipushr p)

    Obs-is-prop : βˆ€ {b} (f : Essential-fibre H b) (c : Obs b) β†’ objβ€² f ≑ c
    Obs-is-prop (aβ‚€ , hβ‚€) (cβ€² , kβ€² , Ξ²) =
      Σ-pathp (Univalent.iso→path c-cat c≅c′) $
      Ξ£-prop-pathp
        (Ξ» i x β†’ Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β†’ Ξ -is-hlevel 1 Ξ» _ β†’ C.Hom-set _ _ _ _) $
        funextP Ξ» a β†’ funextP Ξ» h β†’ C.β‰…-pathp _ _ $
          Univalent.Hom-pathp-reflr-iso c-cat {q = c≅c′}
            ( C.pullr (F.eliml (H.from-id (hβ‚€ .invr)))
            βˆ™ Ξ² _ _ _ (H.Ξ΅-lswizzle (hβ‚€ .invl)))
      where
        ckΞ± = objβ€² (aβ‚€ , hβ‚€)
        c = ckΞ± .fst
        k = ckΞ± .snd .fst
        Ξ± = ckΞ± .snd .snd
        cβ‰…cβ€² = (k aβ‚€ hβ‚€ C.Iso⁻¹) C.∘Iso kβ€² aβ‚€ hβ‚€

We will write G₀ for the canonical choice of object candidate, and k for the associated family of isomorphisms. The type of morphism candidates over f:b→b′f : b \to b' consists of maps G0(b)→G0(b′)G_0(b) \to G_0(b') which are compatible with the reindexing isomorphisms kk for any essential fibre (a,h)(a,h) over bb, (a′,h′)(a',h') over b′b', and map l:a→a′l : a \to a' satisfying h′H(l)=fhh'H(l) = fh.

    compat : βˆ€ {b bβ€²} (f : B.Hom b bβ€²) β†’ C.Hom (Gβ‚€ b) (Gβ‚€ bβ€²) β†’ Type _
    compat {b} {bβ€²} f g =
      βˆ€ a (h : H.β‚€ a B.β‰… b) aβ€² (hβ€² : H.β‚€ aβ€² B.β‰… bβ€²) (l : A.Hom a aβ€²)
      β†’ hβ€² .to B.∘ H.₁ l ≑ f B.∘ h .to
      β†’ k aβ€² hβ€² .to C.∘ F.₁ l ≑ g C.∘ k a h .to

    Homs : βˆ€ {b bβ€²} (f : B.Hom b bβ€²) β†’ Type _
    Homs {b = b} {bβ€²} f = Ξ£ (C.Hom (Gβ‚€ b) (Gβ‚€ bβ€²)) (compat f)
It will again turn out that any initial choice of fibre over bb and b′b' gives a morphism candidate over f:b→b′f : b \to b', and the compatibility data is exactly what we need to show the type of morphism candidates is a proposition.

This proof really isn’t commented. I’m sorry.

    module _ {b bβ€²} (f : B.Hom b bβ€²)
             aβ‚€ (hβ‚€ : H.β‚€ aβ‚€ B.β‰… b)
             aβ‚€β€² (hβ‚€β€² : H.β‚€ aβ‚€β€² B.β‰… bβ€²) where
      lβ‚€ : A.Hom aβ‚€ aβ‚€β€²
      lβ‚€ = H.from (hβ‚€β€² .from B.∘ f B.∘ hβ‚€ .to)

      p : hβ‚€β€² .to B.∘ H.₁ lβ‚€ ≑ (f B.∘ hβ‚€ .to)
      p = H.Ξ΅-lswizzle (hβ‚€β€² .invl)

      gβ‚€ : C.Hom (Gβ‚€ b) (Gβ‚€ bβ€²)
      gβ‚€ = k aβ‚€β€² hβ‚€β€² .to C.∘ F.₁ lβ‚€ C.∘ k aβ‚€ hβ‚€ .from

      module _ a (h : H.β‚€ a B.β‰… b) aβ€² (hβ€² : H.β‚€ aβ€² B.β‰… bβ€²)
                (l : A.Hom a aβ€²) (w : hβ€² .to B.∘ H.₁ l ≑ f B.∘ h .to) where
        m : aβ‚€ A.β‰… a
        m = H.iso.from (hβ‚€ B.∘Iso (h B.Iso⁻¹))

        mβ€² : aβ‚€β€² A.β‰… aβ€²
        mβ€² = H.iso.from (hβ‚€β€² B.∘Iso (hβ€² B.Iso⁻¹))

        Ξ± : k aβ‚€ hβ‚€ .from ≑ F.₁ (m .from) C.∘ k a h .from
        Ξ± = C.inverse-unique _ _ {f = k aβ‚€ hβ‚€} {g = F-map-iso F m C.∘Iso k a h} $
          sym (kcomm _ _ _ (H.Ξ΅-lswizzle (h .invl)))

        Ξ³ : H.₁ (mβ€² .to) B.∘ H.₁ lβ‚€ ≑ H.₁ l B.∘ H.₁ (m .to)
        Ξ³ =  B.pushl (H.Ξ΅ _)
          Β·Β· apβ‚‚ B._∘_ refl (p βˆ™
              B.pushl (B.insertr (h .invl) βˆ™ apβ‚‚ B._∘_ (sym w) refl))
          Β·Β· B.deletel (hβ€² .invr)
          βˆ™ apβ‚‚ B._∘_ refl (sym (H.Ξ΅ _))

        Ξ³β€² : lβ‚€ A.∘ m .from ≑ mβ€² .from A.∘ l
        γ′ = A.iso→monic m′ _ _ $ A.extendl (H.injective (H.swap γ))
                               Β·Β· A.elimr (m .invl)
                               Β·Β· A.insertl (mβ€² .invl)

        Ξ΄ : gβ‚€ C.∘ k a h .to ≑ k aβ€² hβ€² .to C.∘ F.₁ l
        Ξ΄ = C.pullr ( C.pullr refl Β·Β· apβ‚‚ C._∘_ refl (C.pushl Ξ±)
                   Β·Β· C.pulll refl βˆ™ C.elimr (k a h .invr))
          Β·Β· apβ‚‚ C._∘_ refl (F.weave Ξ³β€²)
          Β·Β· C.pulll (C.pushl (sym (kcomm _ _ _ (H.Ξ΅-lswizzle (hβ€² .invl))))
              βˆ™ C.elimr (F.annihilate (mβ€² .invl)))

      Homs-pt : Homs f
      Homs-pt = gβ‚€ , Ξ» a h aβ€² hβ€² l w β†’ sym (Ξ΄ a h aβ€² hβ€² l w)

      Homs-propβ€² : (hβ€² : Homs f) β†’ hβ€² .fst ≑ gβ‚€
      Homs-propβ€² (g₁ , w) = C.isoβ†’epic (k aβ‚€ hβ‚€) _ _
        (sym (Ξ΄ aβ‚€ hβ‚€ aβ‚€β€² hβ‚€β€² lβ‚€ p βˆ™ w aβ‚€ hβ‚€ aβ‚€β€² hβ‚€β€² lβ‚€ p))

    Homs-contrβ€² : βˆ€ {b bβ€²} (f : B.Hom b bβ€²) β†’ βˆ₯ is-contr (Homs f) βˆ₯
    Homs-contrβ€² {b = b} {bβ€²} f = do
      (aβ‚€ , h)   ← H-eso b
      (aβ‚€β€² , hβ€²) ← H-eso bβ€²
      inc (contr (Homs-pt f aβ‚€ h aβ‚€β€² hβ€²) Ξ» hβ€² β†’ Ξ£-prop-path
        (Ξ» _ β†’ compat-prop f) (sym (Homs-propβ€² f _ _ _ _ hβ€²)))

    Homs-contr : βˆ€ {b bβ€²} (f : B.Hom b bβ€²) β†’ is-contr (Homs f)
    Homs-contr f = βˆ₯-βˆ₯-proj (Homs-contrβ€² f)

    G₁ : βˆ€ {b bβ€²} β†’ B.Hom b bβ€² β†’ C.Hom (Gβ‚€ b) (Gβ‚€ bβ€²)
    G₁ f = Homs-contr f .centre .fst
Using the compatibility condition, and choices of (a,h)(a, h), we can show that the assignment of morphism candidates does assemble into a functor.
    module G∘ {x y z} (f : B.Hom y z) (g : B.Hom x y)
              {ax ay az} (hx : H.β‚€ ax B.β‰… x) (hy : H.β‚€ ay B.β‰… y)
              (hz : H.β‚€ az B.β‰… z) where

      af : A.Hom ay az
      af = H.from (hz .from B.∘ f B.∘ hy .to)

      ag : A.Hom ax ay
      ag = H.from (hy .from B.∘ g B.∘ hx .to)

      hβ€² : H.₁ (af A.∘ ag) ≑ hz .from B.∘ f B.∘ g B.∘ hx .to
      hβ€² = H.Ξ΅-expand refl βˆ™ B.pullr (B.cancel-inner (hy .invl))

      commutes : G₁ (f B.∘ g) ≑ G₁ f C.∘ G₁ g
      commutes = C.iso→epic (k ax hx) _ _ $
          sym (Homs-contr (f B.∘ g) .centre .snd ax hx az hz (af A.∘ ag)
                (apβ‚‚ B._∘_ refl hβ€² Β·Β· B.cancell (hz .invl) Β·Β· B.pulll refl))
        βˆ™ sym ( C.pullr (sym (Homs-contr g .centre .snd ax hx ay hy ag
                  (H.Ξ΅-lswizzle (hy .invl))))
              βˆ™ C.pulll (sym (Homs-contr f .centre .snd ay hy az hz af
                  (H.Ξ΅-lswizzle (hz .invl))))
              βˆ™ F.pullr refl)

In this manner, the assignment of object candidates and morphism candidates fits together into a functor G:Bβ†’CG : \mathcal{B} \to \mathcal{C}. After finishing this, we have to show that GH=FGH = F. But the compatibility data which we have used to uniquely characterise GG… uniquely characterises GG, after all, and it does so as composing with HH to give FF.

    G : Functor B C
    G .Fβ‚€ b = Gβ‚€ b
    G .F₁ f = G₁ f

    G .F-id = ap fst $ Homs-contr B.id .paths $ C.id , Ξ» a h aβ€² hβ€² l w β†’
      sym (C.idl _ βˆ™ sym (kcomm (a , h) (aβ€² , hβ€²) l (w βˆ™ B.idl _)))

Note that we proved7 that G1G_1 is functorial given choices of essential fibres of all three objects involved in the composition. Since we’re showing an equality in a set β€” a proposition β€” these choices don’t matter, so we can use essential surjectivity of HH.

    G .F-∘ {x} {y} {z} f g = βˆ₯-βˆ₯-proj do
      (ax , hx) ← H-eso x
      (ay , hy) ← H-eso y
      (az , hz) ← H-eso z
      inc (G∘.commutes f g hx hy hz)

To use the unique charactersation of GG as β€œthe functor satisfying GH=FGH = F”, observe: for any x:Ax : \mathcal{A}, the object F(x)F(x) can be made into an object candidate over H(x)H(x), and since the type of object candidates is a proposition, our candidate F(x)F(x) is identical to the value of GH(x)GH(x). That’s half of GH=FGH = F established right off the bat!

    module _ (x : A.Ob) where
      hf-obs : Obs (H.β‚€ x)
      hf-obs .fst = F.Fβ‚€ x
      hf-obs .snd .fst a h = F-map-iso F (H.iso.from h)
      hf-obs .snd .snd (a , h) (aβ€² , hβ€²) f Ξ± = F.collapse (H.inv∘l Ξ±)

      abstract
        objp : Gβ‚€ (H.β‚€ x) ≑ F.β‚€ x
        objp = ap fst $ summon {H.β‚€ x} (H-eso _) .paths hf-obs

Over that identification, we can show that, for any f:x→yf : x \to y in A\mathcal{A}, the value F(f)F(f) is also a candidate for the morphism GH(f)GH(f), so these are also identical. This proof is a bit hairier, because F(f)F(f) only has the right type if we adjust it by the proof that GH(x)=F(x)GH(x) = F(x): we have to transport F(f)F(f), and then as punishment for our hubris, invoke a lot of technical lemmas about the characterisation of PathP in the morphism spaces of (pre)categories.

    module _ {x y} (f : A.Hom x y) where
      homβ€² : Homs (H.₁ f)
      homβ€² .fst = transport (Ξ» i β†’ C.Hom (objp x (~ i)) (objp y (~ i))) (F.₁ f)
      homβ€² .snd a h aβ€² hβ€² l w = sym $
        C.pushl (Hom-transport C (sym (objp x)) (sym (objp y)) (F.₁ f))
        Β·Β· apβ‚‚ C._∘_ refl
          ( C.pullr (from-pathp-from C (objp x) (Ξ» i β†’ kp x a h i .to))
          βˆ™ F.weave (H.Ξ΅-twist (sym w)))
        Β·Β· C.pulll (from-pathp-to C (sym (objp y)) Ξ» i β†’ kp y aβ€² hβ€² (~ i) .to)

      homp : transport (Ξ» i β†’ C.Hom (objp x (~ i)) (objp y (~ i))) (F.₁ f)
           ≑ Homs-contr (H.₁ f) .centre .fst
      homp = ap fst $ sym $ Homs-contr (H.₁ f) .paths homβ€²

    correct : G F∘ H ≑ F
    correct = Functor-path objp Ξ» {x} {y} f β†’ symP
      {A = Ξ» i β†’ C.Hom (objp x (~ i)) (objp y (~ i))} $
      to-pathp (homp f)

Since we’ve shown that GH=FGH = F, so in particular GHβ‰…FGH \cong F, we’ve now put together proofs that βˆ’βˆ˜H- \circ H is fully faithful and, since the construction above works for any FF, essentially surjective. Even better, since we’ve actually constructed a functor GG, we’ve shown that βˆ’βˆ˜H- \circ H is split essentially surjective! Since [βˆ’,C][-,\mathcal{C}] is univalent whenever C\mathcal{C} is, the splitting would be automatic, but this is a nice strengthening.

  weak-equiv→pre-equiv : is-equivalence {C = Cat[ B , C ]} (precompose H)
  weak-equiv→pre-equiv = ff+split-eso→is-equivalence {F = precompose H}
    (eso-full→pre-ff H H-eso λ g → inc (H.from g , H.Ρ g))
    λ F → G F , path→iso (correct F)

And since a functor is an equivalence of categories iff. it is an isomorphism of categories, we also have that the rule sending FF to its GG is an equivalence of types.

  weak-equiv→pre-iso : is-precat-iso {C = Cat[ B , C ]} (precompose H)
  weak-equiv→pre-iso = is-equivalence→is-precat-iso (precompose H) weak-equiv→pre-equiv
    (Functor-is-category c-cat)
    (Functor-is-category c-cat)

Restating the result that βˆ’βˆ˜H- \circ H acts on objects as an equivalence of types, we have the following result: If R:Cβ†’C+R : \mathcal{C} \to \mathcal{C}^+ is a weak equivalence (a fully faithful and essentially surjective functor), then for any category D\mathcal{D} and functor G:Cβ†’DG : \mathcal{C} \to \mathcal{D}, there is a contractible space(!) of extensions H:C+β†’DH : \mathcal{C}^+ \to \mathcal{D} which factor GG through FF.

weak-equiv→reflection
  : (F : Functor C C⁺) β†’ is-eso F β†’ is-fully-faithful F
  β†’ {D : Precategory o β„“} β†’ is-category D
  β†’ (G : Functor C D)
  β†’ is-contr (Ξ£ (Functor C⁺ D) Ξ» H β†’ H F∘ F ≑ G)
weak-equiv→reflection F F-eso F-ff D-cat G =
  weak-equiv→pre-iso F F-eso F-ff D-cat
    .is-precat-iso.has-is-iso .is-eqv G

Note that this is only half of the point of the Rezk completion: we would also like for C+\mathcal{C}^+ to be univalent, but that is not necessary for DD to think that precomposition with FF is an isomorphism.


  1. a weak equivalence is a fully faithful, essentially surjective functorβ†©οΈŽ

  2. by precompositionβ†©οΈŽ

  3. since both its domain and codomain are univalentβ†©οΈŽ

  4. truncatedβ†©οΈŽ

  5. Don’t worry about actually getting your hands on an (a0,h0)(a_0, h_0).β†©οΈŽ

  6. I’ve implicitly used that HH is eso to cough up an (a,h)(a,h) over bb, since we’re proving a propositionβ†©οΈŽ

  7. in the second <details> tag aboveβ†©οΈŽ