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 ฮทโ‚‚ โ‰ก ฮทโ‚
    โ†’ 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-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 : F โ‰…โฟ F')
    โ†’ is-lan p F' G (eta โˆ˜nt Isoโฟ.from isos)
  natural-iso-ofโ†’is-lan {F' = F'} isos = lan' where
    open is-lan
    module isos = 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 : G โ‰…โฟ G')
    โ†’ is-lan p F G' ((Isoโฟ.to isos โ—‚ p) โˆ˜nt eta)
  natural-iso-extโ†’is-lan {G' = G'} isos = lan' where
    open is-lan
    module isos = 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 : p โ‰…โฟ p')
    โ†’ is-lan p' F G ((G โ–ธ Isoโฟ.to isos) โˆ˜nt eta)
  natural-iso-alongโ†’is-lan {p'} isos = lan' where
    open is-lan
    module isos = Isoโฟ isos
    open Cat.Functor.Reasoning

    lan' : is-lan p' F G ((G โ–ธ 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 : p โ‰…โฟ p')
    โ†’ (F-iso : F โ‰…โฟ F')
    โ†’ (G-iso : G โ‰…โฟ G')
    โ†’ ((Isoโฟ.to G-iso โ—† Isoโฟ.to p-iso) โˆ˜nt eps โˆ˜nt 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)) โ‰ก ฮตโ‚
    โ†’ 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-invertibleโฟ ฮฑ
  ฯƒ-is-invertiblep {ฮฑ} ฮฑ-factor =
    C'D.inversesโ†’invertible (ฯƒ-inversesp {ฮฑ} ฮฑ-factor rโ‚‚.ฯƒ-comm)

  ฯƒ-inverses : Inversesโฟ (rโ‚.ฯƒ ฮตโ‚‚) (rโ‚‚.ฯƒ ฮตโ‚)
  ฯƒ-inverses = ฯƒ-inversesp rโ‚.ฯƒ-comm rโ‚‚.ฯƒ-comm

  ฯƒ-is-invertible : is-invertibleโฟ (rโ‚.ฯƒ ฮตโ‚‚)
  ฯƒ-is-invertible = ฯƒ-is-invertiblep rโ‚.ฯƒ-comm

  unique : 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-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 : F โ‰…โฟ F')
    โ†’ is-ran p F' G (Isoโฟ.to isos โˆ˜nt eps)
  natural-iso-ofโ†’is-ran {F'} isos = ran' where
    open is-ran
    module isos = 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 : G โ‰…โฟ G')
    โ†’ is-ran p F G' (eps โˆ˜nt (Isoโฟ.from isos โ—‚ p))
  natural-iso-extโ†’is-ran {G'} isos = ran' where
    open is-ran
    module isos = 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 : p โ‰…โฟ p')
    โ†’ is-ran p' F G (eps โˆ˜nt (G โ–ธ Isoโฟ.from isos))
  natural-iso-alongโ†’is-ran {p'} isos = ran' where
    open is-ran
    module isos = Isoโฟ isos
    open Cat.Functor.Reasoning

    ran' : is-ran p' F G (eps โˆ˜nt (G โ–ธ Isoโฟ.from isos))
    ran' .ฯƒ {M} ฮฒ = ran.ฯƒ (ฮฒ โˆ˜nt (M โ–ธ 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 : p โ‰…โฟ p')
    โ†’ (F-iso : F โ‰…โฟ F')
    โ†’ (G-iso : G โ‰…โฟ G')
    โ†’ (Isoโฟ.to F-iso โˆ˜nt eps โˆ˜nt (Isoโฟ.from G-iso โ—† 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