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 along ” also includes the natural transformation. For accuracy, using the setup from the diagram below, we should say “ is the Kan extension of along ”.

To show uniqueness, suppose that and and both left extensions of along 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 So, to be clear: The upper triangle and the lower triangle are the same.

Recall that being a left extension means we can (uniquely) factor natural transformations through transformations We want a map for which it will suffice to find a map — but is right there! In the other direction, we can factor to get a map 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₂ η₂
      (ext λ j → sym (D.pullr (β-factor ηₚ j) ∙ α-factor ηₚ j))
      (ext λ j → sym (D.idl _)))
    (l₁.σ-uniq₂ η₁
      (ext λ j → sym (D.pullr (α-factor ηₚ j) ∙ β-factor ηₚ j))
      (ext λ j → sym (D.idl _)))

It’s immediate from the construction that this isomorphism “sends to ”.

  unit : (l₁.σ η₂ ◂ p) ∘nt η₁ ≡ η₂
  unit = l₁.σ-comm

Another uniqueness-like result we can state for left extensions is the following: Given any functor and candidate “unit” transformation if a left extension sends to a natural isomorphism, then is also a left extension of along

  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} {α} = ext λ 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 = ext λ j →
      lan.σ α .η j D.∘ inv .η j                  ≡⟨ (lan.σ-uniq {σ' = σ' ∘nt lan.σ eta'} (ext λ 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} {α} = ext λ 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 $ ext λ 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} {α} = ext λ 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 = ext λ j →
      lan.σ α .η j D.∘ isos.from .η j             ≡⟨ D.pushl (lan.σ-uniq {σ' = σ' ∘nt isos.to} (ext λ 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} = ext λ j →
      D.pulll ((lan.σ _ .is-natural _ _ _))
      ∙ D.pullr (lan.σ-comm ηₚ _)
      ∙ cancell M (isos.invl ηₚ _)
    lan' .σ-uniq {M = M} {α = α} {σ' = σ'} q = ext λ c' →
      lan.σ-uniq {α = (M ▸ isos.from) ∘nt α} {σ' = σ'}
        (ext λ 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 takes values in a univalent category, we can sharpen our result: the type of left extensions of along 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 is univalent, then so is , so our natural isomorphism is equivalent to an identification Then, our tiny lemma stating that this isomorphism “sends to ” is precisely the data of a dependent identification over

  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 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₂ ε₁
        (ext λ j → sym (D.pulll (α-factor ηₚ j) ∙ β-factor ηₚ j))
        (ext λ j → sym (D.idr _)))
      (r₂.σ-uniq₂ ε₂
        (ext λ j → sym (D.pulll (β-factor ηₚ j) ∙ α-factor ηₚ j))
        (ext λ 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} {β} = ext λ j →
      sym ((ran.σ-comm ηₚ _) D.⟩∘⟨refl)
      ·· D.cancel-inner (invl ηₚ _)
      ·· (ran.σ-comm ηₚ _)
    ran' .σ-uniq {M} {β} {σ'} p = ext λ j →
      (D.refl⟩∘⟨ ran.σ-uniq {σ' = ran.σ eps' ∘nt σ'} (ext λ 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} {β} = ext λ j →
      D.pullr (ran.σ-comm ηₚ j)
      ∙ D.cancell (isos.invl ηₚ _)
    ran' .σ-uniq {M} {β} {σ'} p =
      ran.σ-uniq $ ext λ 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} {β} = ext λ j →
      D.cancel-inner (isos.invr ηₚ _)
      ∙ ran.σ-comm ηₚ _
    ran' .σ-uniq {M} {β} {σ'} p = ext λ j →
      D.pushr (ran.σ-uniq {σ' = isos.from ∘nt σ'} (ext λ 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} = ext λ j →
      D.pullr (sym (ran.σ _ .is-natural _ _ _))
      ∙ D.pulll (ran.σ-comm ηₚ _)
      ∙ cancelr M (isos.invl ηₚ _)
    ran' .σ-uniq {M = M} {β = β} {σ' = σ'} q = ext λ c' →
      ran.σ-uniq {β = β ∘nt (M ▸ isos.to)} {σ' = σ'}
        (ext λ 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)
    (ext λ 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