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

module Cat.Functor.Kan.Adjoint where

open _=>_
open _⊣_

private
variable
o ℓ : Level
C D E : Precategory o ℓ


One way to think about Kan extensions is that, when they exist, they allow us to “compose” two functors when one of them is going the wrong way: given a span

$D \xleftarrow{F} C \xrightarrow{H} E$

we get a “composite” $\operatorname{Lan}_F(H) : D \to E$. With this perspective in mind, it’s reasonable to expect that, if $F$ has an inverse $G : D \to C$, the composite we get should be the actual composite $H \circ G$.

In fact, we can do better: if $F$ only has a right adjoint $F \dashv G$ (which we can think of as a directed inverse), then the induced precomposite adjunction $- \circ G \dashv - \circ F$ means that left (global) Kan extensions along $F$ are given by precomposition with $G$ (and, dually, right Kan extensions along $G$ are given by precomposition with $F$).

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F ⊣ G) where
: (H : Functor C E)
→ is-lan F H (H F∘ G) (precomposite-adjunction F⊣G .unit .η H)


A more common way to say this is that $G$ is the absolute left Kan extension of $F$ along the identity; this is essentially a reformulation of the above fact:

  adjoint→is-lan-id : is-lan F Id G (F⊣G .unit)
transport (λ i → is-lan F Id (F∘-idl i) (fixNT i))
where
fixNT : PathP (λ i → Id => F∘-idl {F = G} i F∘ F) _ _
fixNT = Nat-pathp refl (λ i → F∘-idl i F∘ F) (λ _ → refl)

transport (λ i → is-lan F (F∘-idr (~ i)) (H F∘ G) (fixNT (~ i)))
where
fixNT : PathP (λ i → F∘-idr {F = H} i => (H F∘ G) F∘ F) _ _
fixNT = Nat-pathp F∘-idr refl (λ _ → refl)


The dual statement is obtained by… duality, this time using the counit of the precomposite adjunction:

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F ⊣ G) where
: (H : Functor D E)
→ is-ran G H (H F∘ F) (precomposite-adjunction F⊣G .counit .η H)