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

import Cat.Functor.Reasoning
import Cat.Reasoning
module Cat.Functor.Kan.Adjoint where
open _=>_
open _⊣_ hiding (ε)

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

Adjoints are Kan extensions🔗

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
  adjoint→is-lan
    : (H : Functor C E)
    → is-lan F H (H F∘ G) (precomposite-adjunction F⊣G .unit .η H)
  adjoint→is-lan = adjoint-precompose→Lan F (precompose G) (precomposite-adjunction F⊣G)

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)
  adjoint→is-lan-id =
    transport (λ i → is-lan F Id (F∘-idl i) (fixNT i))
      (adjoint→is-lan Id)
    where
      fixNT : PathP (λ i → Id => F∘-idl {F = G} i F∘ F) _ _
      fixNT = Nat-pathp refl (λ i → F∘-idl i F∘ F) (λ _ → refl)

  adjoint→is-absolute-lan : is-absolute-lan adjoint→is-lan-id
  adjoint→is-absolute-lan H =
    transport (λ i → is-lan F (F∘-idr (~ i)) (H F∘ G) (fixNT (~ i)))
      (adjoint→is-lan H)
    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
  adjoint→is-ran
    : (H : Functor D E)
    → is-ran G H (H F∘ F) (precomposite-adjunction F⊣G .counit .η H)
  adjoint→is-ran H =
    transport (λ i → is-ran G H (fixF i) (fixNT i))
      (is-co-lan'→is-ran G H
        (adjoint→is-lan (opposite-adjunction F⊣G) (Functor.op H)))
    where
      fixF : unopF (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.

Kan extensions are adjoints🔗

Conversely, any absolute kan extension over the identity is a pair of adjoint functors.

module _ {F : Functor C D} {G : Functor D C} {nt : Id => G F∘ F}
    {lan : is-lan F Id G nt} (is-absolute : is-absolute-lan lan) where
  open is-lan lan
  module is-absolute {E : Precategory o ℓ} (H : Functor C E) where
    open is-lan (is-absolute H) public
  open Cat.Reasoning C
  private
    module F = Cat.Functor.Reasoning F
    module G = Cat.Functor.Reasoning G
    module D = Cat.Reasoning D

    α : F F∘ Id => Id F∘ F
    α = cohere! (idnt {F = F})

    ε-nt : F F∘ G => Id
    ε-nt = is-absolute.σ F α

    ε : ∀ x → D.Hom (F.₀ (G.₀ x)) x
    ε x = ε-nt .η x

    p : ∀ {c} → (G.₁ (ε (F.₀ c)) ∘ nt .η (G.₀ (F.₀ c))) ∘ nt .η c ≡ nt .η c
    p {c} =
      (G.₁ (ε (F.₀ c)) ∘ nt .η (G.₀ (F.₀ c))) ∘ nt .η c ≡⟨ pullr (nt .is-natural c _ _) ⟩
      G.₁ (ε (F.₀ c)) ∘ (G.₁ (F.₁ (nt .η c))) ∘ nt .η c ≡⟨ G.cancell (is-absolute.σ-comm F {α = α} ηᵈ _) ⟩
      nt .η c                                           ∎
  is-absolute-lan→adjoint : F ⊣ G
  is-absolute-lan→adjoint .unit = nt
  is-absolute-lan→adjoint .counit = ε-nt
  is-absolute-lan→adjoint .zig {A} = is-absolute.σ-comm F {α = α} ηᵈ A
  is-absolute-lan→adjoint .zag {B} = σ-uniq₂ nt
    {σ₁' = cohere! ((G ▸ ε-nt) ∘nt nat-unassoc-to (nt ◂ G))}
    {σ₂' = idnt}
    (ext λ _ → sym p)
    (ext λ _ → sym $ idl _)
    ηᵈ B