module Cat.Functor.Kan.Unique where

Uniqueness of Kan extensionsπŸ”—

Kan extensions (both left and right) are universal constructions, so they are unique when they exist. To get a theorem out of this intuition, we must be careful about how the structure and the properties are separated: Informally, we refer to the functor as β€œthe Kan extension”, but in reality, the data associated with β€œthe Kan extension of FF along pp” also includes the natural transformation. For accuracy, using the setup from the diagram below, we should say β€œ(G,Ξ·)(G, \eta) is the Kan extension of FF along pp”.

To show uniqueness, suppose that (G1,Ξ·1)(G_1, \eta_1) and (G2,Ξ·2)(G_2, \eta_2) and both left extensions of FF along pp. Diagramming this with both natural transformations shown is a bit of a nightmare: the option which doesn’t result in awful crossed arrows is to duplicate the span C′←Cβ†’D\mathcal{C}' \leftarrow \mathcal{C} \to \mathcal{D}. So, to be clear: The upper triangle and the lower triangle are the same.

Recall that (G1,η1)(G_1, \eta_1) being a left extension means we can (uniquely) factor natural transformations F→MpF \to Mp through transformations G1→MG_1 \to M. We want a map G1→G2G_1 \to G_2, for which it will suffice to find a map F→G2pF \to G_2p — but η2\eta_2 is right there! In the other direction, we can factor η1\eta_1 to get a map G2→G1G_2 \to G_1. Since these factorisations are unique, we have a natural isomorphism.

  Οƒ-inversesp
    : βˆ€ {Ξ± : G₁ => Gβ‚‚} {Ξ² : Gβ‚‚ => G₁}
    β†’ (Ξ± β—‚ p) ∘nt η₁ ≑ Ξ·β‚‚
    β†’ (Ξ² β—‚ p) ∘nt Ξ·β‚‚ ≑ η₁
    β†’ natural-inverses Ξ± Ξ²
  Οƒ-inversesp Ξ±-factor Ξ²-factor = Cβ€²D.make-inverses
    (lβ‚‚.Οƒ-uniqβ‚‚ Ξ·β‚‚
      (Nat-path Ξ» j β†’ sym (D.pullr (Ξ²-factor Ξ·β‚š j) βˆ™ Ξ±-factor Ξ·β‚š j))
      (Nat-path Ξ» j β†’ sym (D.idl _)))
    (l₁.Οƒ-uniqβ‚‚ η₁
      (Nat-path Ξ» j β†’ sym (D.pullr (Ξ±-factor Ξ·β‚š j) βˆ™ Ξ²-factor Ξ·β‚š j))
      (Nat-path Ξ» j β†’ sym (D.idl _)))

It’s immediate from the construction that this isomorphism β€œsends Ξ·1\eta_1 to Ξ·2\eta_2”.

  unit : (l₁.Οƒ Ξ·β‚‚ β—‚ p) ∘nt η₁ ≑ Ξ·β‚‚
  unit = l₁.Οƒ-comm

Another uniqueness-like result we can state for left extensions is the following: Given any functor Gβ€²:Cβ€²β†’DG' : \mathcal{C}' \to \mathcal{D} and candidate β€œunit” transformation Ξ·β€²:Fβ†’Gβ€²p\eta' : F \to G'p, if a left extension Lan⁑p(F)\operatorname{Lan}_p(F) sends Ξ·β€²\eta' to a natural isomorphism, then (Gβ€²,Ξ·β€²)(G', \eta') is also a left extension of FF along pp.

  is-invertible→is-lan
    : βˆ€ {G' : Functor Cβ€² D} {eta' : F => G' F∘ p}
    β†’ is-natural-invertible (lan.Οƒ eta')
    β†’ is-lan p F G' eta'
  is-invertible→is-lan {G' = G'} {eta'} invert = lan' where
    open is-lan
    open Cβ€²D.is-invertible invert

    lan' : is-lan p F G' eta'
    lan' .Οƒ Ξ± = lan.Οƒ Ξ± ∘nt inv
    lan' .Οƒ-comm {M} {Ξ±} = Nat-path Ξ» j β†’
      (lan.Οƒ Ξ± .Ξ· _ D.∘ inv .Ξ· _) D.∘ eta' .Ξ· j                      β‰‘Λ˜βŸ¨ D.refl⟩∘⟨ (lan.Οƒ-comm Ξ·β‚š _) βŸ©β‰‘Λ˜
      (lan.Οƒ Ξ± .Ξ· _ D.∘ inv .Ξ· _) D.∘ (lan.Οƒ eta' .Ξ· _ D.∘ eta .Ξ· j) β‰‘βŸ¨ D.cancel-inner (invr Ξ·β‚š _) βŸ©β‰‘
      lan.Οƒ Ξ± .Ξ· _ D.∘ eta .Ξ· j                                      β‰‘βŸ¨ lan.Οƒ-comm Ξ·β‚š _ βŸ©β‰‘
      α .η j                                                         ∎
    lan' .Οƒ-uniq {M} {Ξ±} {Οƒβ€²} p = Nat-path Ξ» j β†’
      lan.Οƒ Ξ± .Ξ· j D.∘ inv .Ξ· j                  β‰‘βŸ¨ (lan.Οƒ-uniq {Οƒβ€² = Οƒβ€² ∘nt lan.Οƒ eta'} (Nat-path Ξ» j β†’ p Ξ·β‚š j βˆ™ D.pushr (sym (lan.Οƒ-comm Ξ·β‚š j))) Ξ·β‚š j) D.⟩∘⟨refl βŸ©β‰‘
      (Οƒβ€² .Ξ· j D.∘ lan.Οƒ eta' .Ξ· j) D.∘ inv .Ξ· _ β‰‘βŸ¨ D.cancelr (invl Ξ·β‚š _) βŸ©β‰‘
      Οƒβ€² .Ξ· j                                    ∎
  natural-iso-of→is-lan
    : {F' : Functor C D}
    β†’ (isos : natural-iso F F')
    β†’ is-lan p F' G (eta ∘nt natural-iso.from isos)
  natural-iso-of→is-lan {F' = F'} isos = lan' where
    open is-lan
    module isos = natural-iso isos

    lan' : is-lan p F' G (eta ∘nt isos.from)
    lan' .Οƒ Ξ± = lan.Οƒ (Ξ± ∘nt isos.to)
    lan' .Οƒ-comm {M} {Ξ±} = Nat-path Ξ» j β†’
      lan.Οƒ (Ξ± ∘nt isos.to) .Ξ· _ D.∘ eta .Ξ· j D.∘ isos.from .Ξ· j β‰‘βŸ¨ D.pulll (lan.Οƒ-comm Ξ·β‚š j) βŸ©β‰‘
      (Ξ± .Ξ· j D.∘ isos.to .Ξ· j) D.∘ isos.from .Ξ· j               β‰‘βŸ¨ D.cancelr (isos.invl Ξ·β‚š _) βŸ©β‰‘
      α .η j ∎
    lan' .Οƒ-uniq {M} {Ξ±} {Οƒβ€²} p =
      lan.Οƒ-uniq $ Nat-path Ξ» j β†’
        Ξ± .Ξ· j D.∘ isos.to .Ξ· j                                    β‰‘βŸ¨ (p Ξ·β‚š j) D.⟩∘⟨refl βŸ©β‰‘
        (Οƒβ€² .Ξ· _ D.∘ eta .Ξ· j D.∘ isos.from .Ξ· j) D.∘ isos.to .Ξ· j β‰‘βŸ¨ D.deleter (isos.invr Ξ·β‚š _) βŸ©β‰‘
        Οƒβ€² .Ξ· _ D.∘ eta .Ξ· j ∎

  natural-iso-ext→is-lan
    : {G' : Functor Cβ€² D}
    β†’ (isos : natural-iso G G')
    β†’ is-lan p F G' ((natural-iso.to isos β—‚ p) ∘nt eta)
  natural-iso-ext→is-lan {G' = G'} isos = lan' where
    open is-lan
    module isos = natural-iso isos

    lan' : is-lan p F G' ((isos.to β—‚ p) ∘nt eta)
    lan' .Οƒ Ξ± = lan.Οƒ Ξ± ∘nt isos.from
    lan' .Οƒ-comm {M} {Ξ±} = Nat-path Ξ» j β†’
      (lan.Οƒ Ξ± .Ξ· _ D.∘ isos.from .Ξ· _) D.∘ isos.to .Ξ· _ D.∘ eta .Ξ· j β‰‘βŸ¨ D.cancel-inner (isos.invr Ξ·β‚š _) βŸ©β‰‘
      lan.Οƒ Ξ± .Ξ· _ D.∘ eta .Ξ· j                                       β‰‘βŸ¨ lan.Οƒ-comm Ξ·β‚š _ βŸ©β‰‘
      α .η j                                                          ∎
    lan' .Οƒ-uniq {M} {Ξ±} {Οƒβ€²} p = Nat-path Ξ» j β†’
      lan.Οƒ Ξ± .Ξ· j D.∘ isos.from .Ξ· j             β‰‘βŸ¨ D.pushl (lan.Οƒ-uniq {Οƒβ€² = Οƒβ€² ∘nt isos.to} (Nat-path Ξ» j β†’ p Ξ·β‚š j βˆ™ D.assoc _ _ _) Ξ·β‚š j) βŸ©β‰‘
      Οƒβ€² .Ξ· j D.∘ isos.to .Ξ· j D.∘ isos.from .Ξ· j β‰‘βŸ¨ D.elimr (isos.invl Ξ·β‚š _) βŸ©β‰‘
      Οƒβ€² .Ξ· j                                     ∎

  natural-iso-along→is-lan
    : {p' : Functor C Cβ€²}
    β†’ (isos : natural-iso p p')
    β†’ is-lan p' F G ((G β–Έ natural-iso.to isos) ∘nt eta)
  natural-iso-along→is-lan {p'} isos = lan' where
    open is-lan
    module isos = natural-iso isos
    open Cat.Functor.Reasoning

    lan' : is-lan p' F G ((G β–Έ natural-iso.to isos) ∘nt eta)
    lan' .Οƒ {M} Ξ± = lan.Οƒ ((M β–Έ isos.from) ∘nt Ξ±)
    lan' .Οƒ-comm {M = M} = Nat-path Ξ» j β†’
      D.pulll ((lan.Οƒ _ .is-natural _ _ _))
      βˆ™ D.pullr (lan.Οƒ-comm Ξ·β‚š _)
      βˆ™ cancell M (isos.invl Ξ·β‚š _)
    lan' .Οƒ-uniq {M = M} {Ξ± = Ξ±} {Οƒβ€² = Οƒβ€²} q = Nat-path Ξ» c' β†’
      lan.Οƒ-uniq {Ξ± = (M β–Έ isos.from) ∘nt Ξ±} {Οƒβ€² = Οƒβ€²}
        (Nat-path Ξ» j β†’
          D.pushr (q Ξ·β‚š _)
          βˆ™ D.pulll (D.pullr (Οƒβ€² .is-natural _ _ _)
                     βˆ™ cancell M (isos.invr Ξ·β‚š _))) Ξ·β‚š c'

  universal-pathβ†’is-lan : βˆ€ {eta'} β†’ eta ≑ eta' β†’ is-lan p F G eta'
  universal-path→is-lan {eta'} q = lan' where
    open is-lan

    lan' : is-lan p F G eta'
    lan' .Οƒ = lan.Οƒ
    lan' .Οƒ-comm = ap (_ ∘nt_) (sym q) βˆ™ lan.Οƒ-comm
    lan' .Οƒ-uniq r = lan.Οƒ-uniq (r βˆ™ ap (_ ∘nt_) (sym q))

module _
    {p p' : Functor C Cβ€²} {F F' : Functor C D}
    {G G' : Functor Cβ€² D} {eps eps'}
    where
  private
    module D = Cat.Reasoning D
    open Cat.Functor.Reasoning
    open _=>_

Left Kan extensions are also invariant under arbitrary natural isomorphisms. To get better definitional control, we allow β€œadjusting” the resulting construction to talk about any natural transformation which is propositionally equal to the whiskering:

  natural-isos→is-lan
    : (p-iso : natural-iso p p')
    β†’ (F-iso : natural-iso F F')
    β†’ (G-iso : natural-iso G G')
    β†’ (natural-iso.to G-iso β—† natural-iso.to p-iso) ∘nt eps ∘nt natural-iso.from F-iso ≑ eps'
    β†’ is-lan p F G eps
    β†’ is-lan p' F' G' eps'

Into univalent categoriesπŸ”—

As traditional with universal constructions, if F:C→DF : \mathcal{C} \to \mathcal{D} takes values in a univalent category, we can sharpen our result: the type of left extensions of FF along pp is a proposition.

Lan-is-prop
  : βˆ€ {p : Functor C Cβ€²} {F : Functor C D} β†’ is-category D β†’ is-prop (Lan p F)
Lan-is-prop {C = C} {Cβ€² = Cβ€²} {D = D} {p = p} {F = F} d-cat L₁ Lβ‚‚ = path where

That’s because if D\mathcal{D} is univalent, then so is [Cβ€²,D][\mathcal{C}', \mathcal{D}], so our natural isomorphism i:G1β‰…G2i : G_1 \cong G_2 is equivalent to an identification iβ€²:G1≑G2i' : G_1 \equiv G_2. Then, our tiny lemma stating that this isomorphism β€œsends Ξ·1\eta_1 to Ξ·2\eta_2” is precisely the data of a dependent identification Ξ·1≑η2\eta_1 \equiv \eta_2 over iβ€²i'.

  functor-path : L₁.Ext ≑ Lβ‚‚.Ext
  functor-path = cβ€²d-cat .to-path Lu.unique

  eta-path : PathP (Ξ» i β†’ F => functor-path i F∘ p) L₁.eta Lβ‚‚.eta
  eta-path = Nat-pathp _ _ Ξ» x β†’
    Univalent.Hom-pathp-reflr-iso d-cat (Lu.unit Ξ·β‚š _)

Since being a left extension is always a proposition when applied to (G,Ξ·)(G, \eta), even when the categories are not univalent, we can finish our proof.

  path : L₁ ≑ Lβ‚‚
  path i .Ext = functor-path i
  path i .eta = eta-path i
  path i .has-lan =
    is-prop→pathp (λ i → is-lan-is-prop {p = p} {F} {functor-path i} {eta-path i})
      L₁.has-lan Lβ‚‚.has-lan i
module
  Ran-unique
    {p : Functor C Cβ€²} {F : Functor C D}
    {G₁ Gβ‚‚ : Functor Cβ€² D} {Ρ₁ Ξ΅β‚‚}
    (r₁ : is-ran p F G₁ Ρ₁)
    (rβ‚‚ : is-ran p F Gβ‚‚ Ξ΅β‚‚)
  where

  private
    module r₁ = is-ran r₁
    module rβ‚‚ = is-ran rβ‚‚
    module D = Cat.Reasoning D
    module Cβ€²D = Cat.Reasoning Cat[ Cβ€² , D ]

  open Cβ€²D._β‰…_
  open Cβ€²D.Inverses

  Οƒ-inversesp
    : βˆ€ {Ξ± : Gβ‚‚ => G₁} {Ξ² : G₁ => Gβ‚‚}
    β†’ (Ρ₁ ∘nt (Ξ± β—‚ p)) ≑ Ξ΅β‚‚
    β†’ (Ξ΅β‚‚ ∘nt (Ξ² β—‚ p)) ≑ Ρ₁
    β†’ natural-inverses Ξ± Ξ²
  Οƒ-inversesp Ξ±-factor Ξ²-factor =
    Cβ€²D.make-inverses
      (r₁.Οƒ-uniqβ‚‚ Ρ₁
        (Nat-path Ξ» j β†’ sym (D.pulll (Ξ±-factor Ξ·β‚š j) βˆ™ Ξ²-factor Ξ·β‚š j))
        (Nat-path Ξ» j β†’ sym (D.idr _)))
      (rβ‚‚.Οƒ-uniqβ‚‚ Ξ΅β‚‚
        (Nat-path Ξ» j β†’ sym (D.pulll (Ξ²-factor Ξ·β‚š j) βˆ™ Ξ±-factor Ξ·β‚š j))
        (Nat-path Ξ» j β†’ sym (D.idr _)))

  Οƒ-is-invertiblep
    : βˆ€ {Ξ± : Gβ‚‚ => G₁}
    β†’ (Ρ₁ ∘nt (Ξ± β—‚ p)) ≑ Ξ΅β‚‚
    β†’ is-natural-invertible Ξ±
  Οƒ-is-invertiblep {Ξ±} Ξ±-factor =
    C′D.inverses→invertible (σ-inversesp {α} α-factor r₂.σ-comm)

  Οƒ-inverses : natural-inverses (r₁.Οƒ Ξ΅β‚‚) (rβ‚‚.Οƒ Ρ₁)
  Οƒ-inverses = Οƒ-inversesp r₁.Οƒ-comm rβ‚‚.Οƒ-comm

  Οƒ-is-invertible : is-natural-invertible (r₁.Οƒ Ξ΅β‚‚)
  Οƒ-is-invertible = Οƒ-is-invertiblep r₁.Οƒ-comm

  unique : natural-iso G₁ Gβ‚‚
  unique = Cβ€²D.invertibleβ†’iso (r₁.Οƒ Ξ΅β‚‚) (Οƒ-is-invertiblep r₁.Οƒ-comm) ni⁻¹

  counit : Ρ₁ ∘nt (r₁.Οƒ Ξ΅β‚‚ β—‚ p) ≑ Ξ΅β‚‚
  counit = r₁.Οƒ-comm

module _
    {p : Functor C Cβ€²} {F : Functor C D}
    {G : Functor Cβ€² D} {eps}
    (ran : is-ran p F G eps)
    where

  private
    module ran = is-ran ran
    module D = Cat.Reasoning D
    module Cβ€²D = Cat.Reasoning Cat[ Cβ€² , D ]
    open _=>_

  -- These are more annoying to do via duality then it is to do by hand,
  -- due to the natural isos.
  is-invertible→is-ran
    : βˆ€ {G' : Functor Cβ€² D} {eps'}
    β†’ is-natural-invertible (ran.Οƒ eps')
    β†’ is-ran p F G' eps'
  is-invertible→is-ran {G' = G'} {eps'} invert = ran' where
    open is-ran
    open Cβ€²D.is-invertible invert

    ran' : is-ran p F G' eps'
    ran' .Οƒ Ξ² = inv ∘nt ran.Οƒ Ξ²
    ran' .Οƒ-comm {M} {Ξ²} = Nat-path Ξ» j β†’
      sym ((ran.Οƒ-comm Ξ·β‚š _) D.⟩∘⟨refl)
      Β·Β· D.cancel-inner (invl Ξ·β‚š _)
      Β·Β· (ran.Οƒ-comm Ξ·β‚š _)
    ran' .Οƒ-uniq {M} {Ξ²} {Οƒβ€²} p = Nat-path Ξ» j β†’
      (D.refl⟩∘⟨ ran.Οƒ-uniq {Οƒβ€² = ran.Οƒ eps' ∘nt Οƒβ€²} (Nat-path Ξ» j β†’ p Ξ·β‚š j βˆ™ D.pushl (sym (ran.Οƒ-comm Ξ·β‚š j))) Ξ·β‚š _)
      βˆ™ D.cancell (invr Ξ·β‚š _)

  natural-iso-of→is-ran
    : {F' : Functor C D}
    β†’ (isos : natural-iso F F')
    β†’ is-ran p F' G (natural-iso.to isos ∘nt eps)
  natural-iso-of→is-ran {F'} isos = ran' where
    open is-ran
    module isos = natural-iso isos

    ran' : is-ran p F' G (isos.to ∘nt eps)
    ran' .Οƒ Ξ² = ran.Οƒ (isos.from ∘nt Ξ²)
    ran' .Οƒ-comm {M} {Ξ²} = Nat-path Ξ» j β†’
      D.pullr (ran.Οƒ-comm Ξ·β‚š j)
      βˆ™ D.cancell (isos.invl Ξ·β‚š _)
    ran' .Οƒ-uniq {M} {Ξ²} {Οƒβ€²} p =
      ran.Οƒ-uniq $ Nat-path Ξ» j β†’
        (D.refl⟩∘⟨ p Ξ·β‚š j)
        βˆ™ D.deletel (isos.invr Ξ·β‚š _)

  natural-iso-ext→is-ran
    : {G' : Functor Cβ€² D}
    β†’ (isos : natural-iso G G')
    β†’ is-ran p F G' (eps ∘nt (natural-iso.from isos β—‚ p))
  natural-iso-ext→is-ran {G'} isos = ran' where
    open is-ran
    module isos = natural-iso isos

    ran' : is-ran p F G' (eps ∘nt (isos.from β—‚ p))
    ran' .Οƒ Ξ² = isos.to ∘nt ran.Οƒ Ξ²
    ran' .Οƒ-comm {M} {Ξ²} = Nat-path Ξ» j β†’
      D.cancel-inner (isos.invr Ξ·β‚š _)
      βˆ™ ran.Οƒ-comm Ξ·β‚š _
    ran' .Οƒ-uniq {M} {Ξ²} {Οƒβ€²} p = Nat-path Ξ» j β†’
      D.pushr (ran.Οƒ-uniq {Οƒβ€² = isos.from ∘nt Οƒβ€²} (Nat-path Ξ» j β†’ p Ξ·β‚š j βˆ™ sym (D.assoc _ _ _)) Ξ·β‚š j)
      βˆ™ D.eliml (isos.invl Ξ·β‚š _)

  natural-iso-along→is-ran
    : {p' : Functor C Cβ€²}
    β†’ (isos : natural-iso p p')
    β†’ is-ran p' F G (eps ∘nt (G β–Έ natural-iso.from isos))
  natural-iso-along→is-ran {p'} isos = ran' where
    open is-ran
    module isos = natural-iso isos
    open Cat.Functor.Reasoning

    ran' : is-ran p' F G (eps ∘nt (G β–Έ natural-iso.from isos))
    ran' .Οƒ {M} Ξ² = ran.Οƒ (Ξ² ∘nt (M β–Έ natural-iso.to isos))
    ran' .Οƒ-comm {M = M} = Nat-path Ξ» j β†’
      D.pullr (sym (ran.Οƒ _ .is-natural _ _ _))
      βˆ™ D.pulll (ran.Οƒ-comm Ξ·β‚š _)
      βˆ™ cancelr M (isos.invl Ξ·β‚š _)
    ran' .Οƒ-uniq {M = M} {Ξ² = Ξ²} {Οƒβ€² = Οƒβ€²} q = Nat-path Ξ» c' β†’
      ran.Οƒ-uniq {Ξ² = Ξ² ∘nt (M β–Έ isos.to)} {Οƒβ€² = Οƒβ€²}
        (Nat-path Ξ» j β†’
          D.pushl (q Ξ·β‚š _)
          βˆ™ D.pullr (D.pulll (sym (Οƒβ€² .is-natural _ _ _))
                     βˆ™ cancelr M (isos.invr Ξ·β‚š _))) Ξ·β‚š c'

  universal-pathβ†’is-ran : βˆ€ {eps'} β†’ eps ≑ eps' β†’ is-ran p F G eps'
  universal-path→is-ran {eps'} q = ran' where
    open is-ran

    ran' : is-ran p F G eps'
    ran' .Οƒ = ran.Οƒ
    ran' .Οƒ-comm = ap (_∘nt _) (sym q) βˆ™ ran.Οƒ-comm
    ran' .Οƒ-uniq r = ran.Οƒ-uniq (r βˆ™ ap (_∘nt _) (sym q))

module _
    {p p' : Functor C Cβ€²} {F F' : Functor C D}
    {G G' : Functor Cβ€² D} {eps eps'}
    where
  private
    module D = Cat.Reasoning D
    open _=>_

  natural-isos→is-ran
    : (p-iso : natural-iso p p')
    β†’ (F-iso : natural-iso F F')
    β†’ (G-iso : natural-iso G G')
    β†’ (natural-iso.to F-iso ∘nt eps ∘nt (natural-iso.from G-iso β—† natural-iso.from p-iso)) ≑ eps'
    β†’ is-ran p F G eps
    β†’ is-ran p' F' G' eps'
  natural-isos→is-ran p-iso F-iso G-iso p ran =
    universal-path→is-ran
      (natural-iso-ext→is-ran
        (natural-iso-of→is-ran
          (natural-iso-along→is-ran ran p-iso)
        F-iso)
      G-iso)
    (Nat-path Ξ» c β†’
      sym (D.assoc _ _ _)
      Β·Β· apβ‚‚ D._∘_ refl (sym $ D.assoc _ _ _)
      Β·Β· p Ξ·β‚š _)

Ran-is-prop
  : βˆ€ {p : Functor C Cβ€²} {F : Functor C D} β†’ is-category D β†’ is-prop (Ran p F)
Ran-is-prop {C = C} {Cβ€² = Cβ€²} {D = D} {p = p} {F = F} d-cat R₁ Rβ‚‚ = path where
  module R₁ = Ran R₁
  module Rβ‚‚ = Ran Rβ‚‚
  module Ru = Ran-unique R₁.has-ran Rβ‚‚.has-ran

  open Ran

  cβ€²d-cat : is-category Cat[ Cβ€² , D ]
  cβ€²d-cat = Functor-is-category d-cat

  fp : R₁.Ext ≑ Rβ‚‚.Ext
  fp = cβ€²d-cat .to-path Ru.unique

  Ξ΅p : PathP (Ξ» i β†’ fp i F∘ p => F) R₁.eps Rβ‚‚.eps
  Ξ΅p = Nat-pathp _ _ Ξ» x β†’ Univalent.Hom-pathp-refll-iso d-cat (Ru.counit Ξ·β‚š _)

  path : R₁ ≑ Rβ‚‚
  path i .Ext = fp i
  path i .eps = Ξ΅p i
  path i .has-ran =
    is-prop→pathp (λ i → is-ran-is-prop {p = p} {F} {fp i} {Ρp i})
      R₁.has-ran Rβ‚‚.has-ran i