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.Functor.Compose
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

we get a “composite” With this perspective in mind, it’s reasonable to expect that, if has an inverse the composite we get should be the actual composite

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

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 is the absolute left Kan extension of 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)
transport (λ i → is-ran G H (fixF i) (fixNT i))
(is-co-lan'→is-ran G H
where
fixF : Functor.op (Functor.op H F∘ Functor.op F) ≡ H F∘ F
fixF = Functor-path (λ _ → refl) (λ _ → refl)
fixNT : PathP (λ i → fixF i F∘ G => H) _ _
fixNT = Nat-pathp (λ i → fixF i F∘ G) refl (λ _ → refl)


Even more dually, we can flip the span above to get a cospan of functors, giving rise to the theory of Kan lifts. We then get analogous statements: left (resp. right) adjoints are absolute left (resp. right) Kan lifts along the identity.