open import Cat.Instances.Functor.Compose
open import Cat.Instances.Functor
open import Cat.Functor.Base
open import Cat.Functor.Kan
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Kan.Unique



# Uniqueness of Kan extensions🔗

Since (left) Kan extensions are defined by a universal property (they are partial values of a specific adjunction), they are unique: When $\mathcal{D}$ is a category, then the type $\operatorname{Lan}_p(F)$ of left Kan extensions of $F$ along $p$ is a proposition.

Lan-is-prop : is-prop (Lan p F)
Lan-is-prop L₁ L₂ = Lan-unique module Lan-unique where


We diagram the situation generically as follows: $p$ and $F$ are fixed, with $G$ and $G'$ being both left extensions of $F$ along $p$. The functor $G$ (resp. $G'$) is equipped with a natural transformation $\eta : F \to Gp$ (resp. $\eta' : F \to G'p$), and if $M$ is equipped with $\theta : F \to Mp$, then $G$ can cough up a unique natural transformation $\sigma_\theta : G \to M$ (resp. $\sigma'_\theta : G' \to M$) making everything in sight commute.  The isomorphism $G \cong G'$ is constructed as follows: Since $G'$ is equipped with $\eta'$, $G$ can produce $\sigma_{\eta'} : G \to G'$; Since $G$ is equipped with $\eta$, $G'$ can produce $\sigma'_\eta : G' \to G$. To show $\sigma_{\eta'}\sigma'_\eta : G' \to G'$ is the identity, note that both make “everything in sight commute”, so they inhabit a contractible space since $G'$ is an extension. The argument for $\sigma'_\eta\sigma_{\eta'}$ is analogous.

  Ext-unique : [C′,D].Isomorphism L₁.Ext L₂.Ext
Ext-unique = [C′,D].make-iso (L₁.σ L₂.eta) (L₂.σ L₁.eta)
( sym (L₂.σ-uniq {α = L₂.eta}
(Nat-path λ _ → sym ( D.pullr (L₂.σ-comm ηₚ _)
∙ L₁.σ-comm ηₚ _)))
∙ L₂.σ-uniq (Nat-path λ _ → D.introl refl))
( sym (L₁.σ-uniq {α = L₁.eta}
(Nat-path λ _ → sym ( D.pullr (L₁.σ-comm ηₚ _)
∙ L₂.σ-comm ηₚ _)))
∙ L₁.σ-uniq (Nat-path λ _ → D.introl refl))

Ext-uniqueₚ : L₁.Ext ≡ L₂.Ext
Ext-uniqueₚ = cd-cat .to-path Ext-unique


The functor is not the only data associated with a left extension, though: we must also verify that, under the identification $G \equiv G'$ we just produced, the natural transformations $\eta$ and $\eta'$ are also identified. This boils down to verifying, in components, that $\sigma_{\eta'}\eta = \eta'$, but that is immediate by the specification for $\sigma$.

  eta-uniqueₚ : PathP (λ i → F => Ext-uniqueₚ i F∘ p) L₁.eta L₂.eta
eta-uniqueₚ = Nat-pathp refl _ λ _ →
Univalent.Hom-pathp-reflr-iso dcat (L₁.σ-comm ηₚ _)

A similar argument shows that $\sigma_j$ and $\sigma'_j$ are also identified.
  σ-uniqueₚ : ∀ {M} (f : F => M F∘ p)
→ PathP (λ i → Ext-uniqueₚ i => M) (L₁.σ f) (L₂.σ f)
σ-uniqueₚ {M = M} f = Nat-pathp _ _ λ _ →
Univalent.Hom-pathp-refll-iso dcat lemma
where
σ′ : L₂.Ext => M
σ′ .η x = L₁.σ f .η x D.∘ L₂.σ L₁.eta .η x
σ′ .is-natural x y f = D.pullr (L₂.σ _ .is-natural _ _ _)
∙ D.extendl (L₁.σ _ .is-natural _ _ _)

lemma : ∀ {x} → L₁.σ f .η x D.∘ L₂.σ (L₁.eta) .η x ≡ L₂.σ f .η x
lemma {x = x} = sym $ap (λ e → e .η x) {y = σ′}$
L₂.σ-uniq \$ Nat-path λ _ → sym (
D.pullr (L₂.σ-comm ηₚ _) ∙ L₁.σ-comm ηₚ _)


Now $(G, \eta, \sigma)$ is all the data of a left extension: The other two fields are propositions, and so they are automatically identified — regardless of the specific isomorphism we would have exhibited.

  open Lan

Lan-unique : L₁ ≡ L₂
Lan-unique i .Ext = cd-cat .to-path Ext-unique i
Lan-unique i .eta = eta-uniqueₚ i
Lan-unique i .σ f = σ-uniqueₚ f i
Lan-unique i .σ-comm {α = α} =
is-prop→pathp
(λ i → [C,D].Hom-set _ _ ((σ-uniqueₚ α i ◂ p) ∘nt eta-uniqueₚ i) α)
L₁.σ-comm L₂.σ-comm i
Lan-unique i .σ-uniq {M = M} {α = α} {σ′ = σ′} =
is-prop→pathp
(λ i → Π-is-hlevel² {A = cd-cat .to-path Ext-unique i => M}
{B = λ σ′ → α ≡ (σ′ ◂ p) ∘nt eta-uniqueₚ i} 1
λ σ′ x → [C′,D].Hom-set _ _ (σ-uniqueₚ α i) σ′)
(λ σ′ → L₁.σ-uniq {σ′ = σ′})
(λ σ′ → L₂.σ-uniq {σ′ = σ′})
i σ′