module Cat.Functor.Kan.Duality where

Duality for Kan extensions🔗

Left Kan extensions are dual to right Kan extensions. This is straightforward enough to prove, but does involve some bureaucracy involving opposite categories.

  is-co-lan'→is-ran
    : ∀ {G : Functor (C' ^op) (D ^op)} {eta : Functor.op F => G F∘ Functor.op p}
    → is-lan (Functor.op p) (Functor.op F) G eta
    → is-ran p F (Functor.op G) (co-unit→counit eta)
  is-co-lan'→is-ran {G = G} {eta = eta} is-lan = ran where
    module lan = is-lan is-lan

    ran : is-ran p F (Functor.op G) (co-unit→counit eta)
    ran .σ {M = M} α = op (lan.σ α') where
      unquoteDecl α' = dualise-into α'
        (Functor.op F => Functor.op M F∘ Functor.op p)
        α

    ran .σ-comm = ext (lan.σ-comm ηₚ_)
    ran .σ-uniq {M = M} {σ' = σ'} p = ext λ x →
      lan.σ-uniq {σ' = dualise! σ'} (reext! p) ηₚ x