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

import Cat.Reasoning

open Functor
open _=>_
open Lan

module Cat.Functor.Kan.Global

  {o β oβ² ββ² oβ²β² ββ²β²}
{C : Precategory o β}
{Cβ² : Precategory oβ² ββ²}
{D : Precategory oβ²β² ββ²β²}
(p : Functor C Cβ²)
where


# Global Kan extensionsπ

Recall that a left Kan extension of $F : C \to D$ along $p : C \to C'$ is a universal solution $\operatorname{Lan}_p(F)$ to extending $F$ to a functor $C' \to D$. In particularly happy cases (e.g.Β when $C$ is small and $D$ is cocomplete), the left Kan extension $\operatorname{Lan}_p(F)$ along $p$ exists for any $F$; When this happens, the assignment $F \mapsto \operatorname{Lan}_p(F)$ extends to a functor, which we call a global Kan extension.

private
module D = Cat.Reasoning D
module C = Cat.Reasoning C
module Cβ² = Cat.Reasoning Cβ²

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 $- \circ p$.

  Lanβ£precompose : Lan-functor β£ precompose p
Lanβ£precompose = 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} {precompose 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 $- \circ p$ has any left adjoint, then its values generate Kan extensions:

adjoint-precomposeβLan
: (F : Functor Cat[ C , D ] Cat[ Cβ² , D ])
β (adj : F β£ precompose p)
β (G : Functor C D)
β is-lan p G (F .Fβ G) (adj ._β£_.unit .Ξ· G)
open Lan
open is-lan