open import Cat.Functor.Naturality
open import Cat.Functor.Univalence
open import Cat.Functor.Kan.Base
open import Cat.Functor.Compose
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

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

private variable
  o ℓ : Level
  C C' D : Precategory o ℓ

module
  Lan-unique
    {p : Functor C C'} {F : Functor C D}
    {G₁ G₂ : Functor C' D} {η₁ η₂}
    (l₁ : is-lan p F G₁ η₁)
    (l₂ : is-lan p F G₂ η₂)
  where

  private
    module l₁ = is-lan l₁
    module l₂ = is-lan l₂
    module D = Cat.Reasoning D
    module C'D = Cat.Reasoning Cat[ C' , D ]

  open C'D._≅_
  open C'D.Inverses

To show uniqueness, suppose that $(G_{1}, η_{1})$ and $(G_{2}, η_{2})$ and both left extensions of $F$ along $p .$ 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^{'} \leftarrow C \to D .$ So, to be clear: The upper triangle and the lower triangle are the same.

Recall that $(G_{1}, η_{1})$ being a left extension means we can (uniquely) factor natural transformations $F \to Mp$ through transformations $G_{1} \to M .$ We want a map $G_{1} \to G_{2},$ for which it will suffice to find a map $F \to G_{2} p$ — but $η_{2}$ is right there! In the other direction, we can factor $η_{1}$ to get a map $G_{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₂ η₂
      (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 _)))

  σ-is-invertiblep
    : ∀ {α : G₁ => G₂}
    → (α ◂ p) ∘nt η₁ ≡ η₂
    → is-invertibleⁿ α
  σ-is-invertiblep {α = α} α-factor =
    C'D.inverses→invertible (σ-inversesp {α} α-factor l₂.σ-comm)

  σ-inverses : Inversesⁿ (l₁.σ η₂) (l₂.σ η₁)
  σ-inverses = σ-inversesp l₁.σ-comm l₂.σ-comm

  σ-is-invertible : is-invertibleⁿ (l₁.σ η₂)
  σ-is-invertible = σ-is-invertiblep l₁.σ-comm

  unique : G₁ ≅ⁿ G₂
  unique = C'D.invertible→iso (l₁.σ η₂) (σ-is-invertiblep l₁.σ-comm)

It’s immediate from the construction that this isomorphism “sends $η_{1}$ to $η_{2}$ ”.

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

module _
    {p : Functor C C'} {F : Functor C D}
    {G : Functor C' D} {eta}
    (lan : is-lan p F G eta)
    where

  private
    module lan = is-lan lan
    module D = Cat.Reasoning D
    module C'D = Cat.Reasoning Cat[ C' , D ]
    open _=>_

Another uniqueness-like result we can state for left extensions is the following: Given any functor $G^{'} : C^{'} \to D$ and candidate “unit” transformation $η^{'} : F \to G^{'} p,$ if a left extension $Lan_{p} (F)$ sends $η^{'}$ to a natural isomorphism, then $(G^{'}, η^{'})$ is also a left extension of $F$ along $p .$

  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'

  natural-isos→is-lan p-iso F-iso G-iso q lan =
    universal-path→is-lan
      (natural-iso-ext→is-lan
        (natural-iso-of→is-lan (natural-iso-along→is-lan lan p-iso) F-iso)
        G-iso)
      (ext λ x → D.extendl (D.pulll (G-iso .to .is-natural _ _ _)) ∙ q ηₚ _)
    where open Isoⁿ

Into univalent categories🔗

As traditional with universal constructions, if $F : C \to D$ takes values in a univalent category, we can sharpen our result: the type of left extensions of $F$ along $p$ 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

  module L₁ = Lan L₁
  module L₂ = Lan L₂
  module Lu = Lan-unique L₁.has-lan L₂.has-lan

  open Lan

  c'd-cat : is-category Cat[ C' , D ]
  c'd-cat = Functor-is-category d-cat

That’s because if $D$ is univalent, then so is $[C^{'}, D]$ , so our natural isomorphism $i : G_{1} ≅ G_{2}$ is equivalent to an identification $i^{'} : G_{1} \equiv G_{2} .$ Then, our tiny lemma stating that this isomorphism “sends $η_{1}$ to $η_{2}$ ” is precisely the data of a dependent identification $η_{1} \equiv η_{2}$ over $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, η),$ 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