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, \eta)$ is the Kan extension of $F$ along $p$”.

To show uniqueness, suppose that $(G_1, \eta_1)$ and $(G_2, \eta_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 $\mathcal{C}' \leftarrow \mathcal{C} \to \mathcal{D}$. So, to be clear: The upper triangle and the lower triangle are the same.

Recall that $(G_1, \eta_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_2p$ — but $\eta_2$ is right there! In the other direction, we can factor $\eta_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₂ η₂
      (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 $\eta_1$ to $\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' : \mathcal{C}' \to \mathcal{D}$ and candidate “unit” transformation $\eta' : F \to G'p$, if a left extension $\operatorname{Lan}_p(F)$ sends $\eta'$ to a natural isomorphism, then $(G', \eta')$ 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} {α} = 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                                    ∎

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 : \mathcal{C} \to \mathcal{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

That’s because if $\mathcal{D}$ is univalent, then so is $[\mathcal{C}', \mathcal{D}]$, so our natural isomorphism $i : G_1 \cong G_2$ is equivalent to an identification $i' : G_1 \equiv G_2$. Then, our tiny lemma stating that this isomorphism “sends $\eta_1$ to $\eta_2$” is precisely the data of a dependent identification $\eta_1 \equiv \eta_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, \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