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 D\mathcal{D} is a category, then the type Lan⁑p(F)\operatorname{Lan}_p(F) of left Kan extensions of FF along pp 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: pp and FF are fixed, with GG and Gβ€²G' being both left extensions of FF along pp. The functor GG (resp. Gβ€²G') is equipped with a natural transformation Ξ·:Fβ†’Gp\eta : F \to Gp (resp. Ξ·β€²:Fβ†’Gβ€²p\eta' : F \to G'p), and if MM is equipped with ΞΈ:Fβ†’Mp\theta : F \to Mp, then GG can cough up a unique natural transformation σθ:Gβ†’M\sigma_\theta : G \to M (resp. σθ′:Gβ€²β†’M\sigma'_\theta : G' \to M) making everything in sight commute.

The isomorphism Gβ‰…Gβ€²G \cong G' is constructed as follows: Since Gβ€²G' is equipped with Ξ·β€²\eta', GG can produce ση′:Gβ†’Gβ€²\sigma_{\eta'} : G \to G'; Since GG is equipped with Ξ·\eta, Gβ€²G' can produce ση′:Gβ€²β†’G\sigma'_\eta : G' \to G. To show ση′ση′:Gβ€²β†’Gβ€²\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β€²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≑Gβ€²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 Οƒj\sigma_j and Οƒjβ€²\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,Ξ·,Οƒ)(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 Οƒβ€²