open import Cat.Instances.Functor.Compose
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Adjoint.Hom
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Adjoint
open import Cat.Functor.Kan
open import Cat.Prelude

import Cat.Reasoning

open Functor
open _=>_
open Lan

module Cat.Functor.Kan.Global

Global Kan extensionsπŸ”—

Recall that a left Kan extension of F:Cβ†’DF : C \to D along p:Cβ†’Cβ€²p : C \to C' is a universal solution Lan⁑p(F)\operatorname{Lan}_p(F) to extending FF to a functor Cβ€²β†’DC' \to D. In particularly happy cases (e.g.Β when CC is small and DD is cocomplete), the left Kan extension Lan⁑p(F)\operatorname{Lan}_p(F) along pp exists for any FF; When this happens, the assignment F↦Lan⁑p(F)F \mapsto \operatorname{Lan}_p(F) *extends to a functor, which we call a global Kan extension.

module _ (has-lan : (G : Functor C D) β†’ Lan p G) where
  Lan-functor : Functor Cat[ C , D ] Cat[ Cβ€² , D ]
  Lan-functor .Fβ‚€ G = has-lan G .Ext
  Lan-functor .F₁ {x} {y} ΞΈ =
    has-lan x .Οƒ (has-lan y .eta ∘nt ΞΈ)
  Lan-functor .F-id {x} = has-lan x .Οƒ-uniq (Nat-path Ξ» _ β†’
  Lan-functor .F-∘ {x} {y} {z} f g =
    has-lan x .Οƒ-uniq $ Nat-path Ξ» a β†’ sym $
        D.pullr   (has-lan x .Οƒ-comm Ξ·β‚š a)
      βˆ™ D.extendl (has-lan y .Οƒ-comm Ξ·β‚š a)

Functoriality follows, essentially, from the fact that left Kan extensions are universal: we can map between them in a functorial way using only the defining natural transformations in the diagram, without appealing to the details of a particular computation. Moreover, the left Kan extension functor itself has a universal property: it is a left adjoint to the precomposition functor p!p_!.

  Lan⊣! : Lan-functor ⊣ p !
  Lan⊣! = hom-isoβ†’adjoints f (is-isoβ†’is-equiv eqv) natural where
    f : βˆ€ {x : Functor C D} {y : Functor Cβ€² D} β†’ has-lan x .Ext => y β†’ x => y F∘ p
    f {x} {y} ΞΈ = (ΞΈ β—‚ p) ∘nt has-lan x .eta

    open is-iso

    eqv : βˆ€ {x} {y} β†’ is-iso (f {x} {y})
    eqv {x} {y} .inv ΞΈ = has-lan _ .Οƒ ΞΈ
    eqv {x} {y} .rinv ΞΈ = has-lan x .Οƒ-comm
    eqv {x} {y} .linv ΞΈ = has-lan _ .Οƒ-uniq refl

    natural : hom-iso-natural {L = Lan-functor} {p !} f
    natural {b = b} g h x = Nat-path Ξ» a β†’
      D.pullr (D.pullr (has-lan _ .Οƒ-comm Ξ·β‚š a))
      βˆ™ apβ‚‚ D._∘_ refl (D.pushr refl)

And, since adjoints are unique, if p!p_! has any left adjoint, then its values generate Kan extensions:

  : (F : Functor Cat[ C , D ] Cat[ Cβ€² , D ])
  β†’ F ⊣ p !
  β†’ (G : Functor C D) β†’ Lan p G
adjointβ†’Lan F F⊣p! G = ext where
  open Lan
  module F⊣p! = _⊣_ F⊣p!

  ext : Lan p G
  ext .Ext = F .Fβ‚€ G
  ext .eta = F⊣p!.unit .η G
  ext .Οƒ Ξ± = R-adjunct F⊣p! Ξ±
  ext .Οƒ-comm {M = M} {Ξ± = Ξ±} = Nat-path Ξ» a β†’
      D.pullr   (sym (F⊣p!.unit .is-natural _ _ _) Ξ·β‚š a)
    βˆ™ D.cancell (F⊣p!.zag Ξ·β‚š a)
  ext .Οƒ-uniq x = Equiv.injective (_ , L-adjunct-is-equiv F⊣p!)
    (L-R-adjunct F⊣p! _ βˆ™ x)