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 along is a universal solution to extending to a functor . In particularly happy cases (e.g.Β when is small and is cocomplete), the left Kan extension along exists for any ; When this happens, the assignment *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 Ξ» _ β D.id-comm) 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 .
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 has any left adjoint, then its values generate Kan extensions:
adjointβLan : (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)