open import Cat.Instances.Functor.Compose
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Functor
open import Cat.Diagram.Duals
open import Cat.Functor.Kan
open import Cat.Prelude

module Cat.Functor.Kan.Right where

Right Kan extensions🔗

Dually to our setup for a left Kan extension, we have right Kan extensions: The (suitably weakly) terminal solution to the problem of lifting a functor $F : \mathcal{C} \to \mathcal{D}$ along a functor $p : \mathcal{C}' \to \mathcal{C}$. We picture the situation as in the following commutative diagram:

Note the same warnings about “weak, directed” commutativity as for [left Kan extensions] apply here, too. Rather than either of the triangles commuting on the nose, we have natural transformations $\varepsilon$ witnessing their commutativity.

record Ran (p : Functor C C′) (F : Functor C D) : Type (kan-lvl p F) where
  field
    Ext : Functor C′ D
    eps : Ext F∘ p => F

    σ : {M : Functor C′ D} (α : M F∘ p => F) → M => Ext
    σ-comm : {M : Functor C′ D} {β : M F∘ p => F} → eps ∘nt (σ β ◂ p) ≡ β
    σ-uniq : {M : Functor C′ D} {β : M F∘ p => F} {σ′ : M => Ext}
           → β ≡ eps ∘nt (σ′ ◂ p)
           → σ β ≡ σ′

  σ-uniq₂
    : {M : Functor C′ D} (β : M F∘ p => F) {σ₁′ σ₂′ : M => Ext}
    → β ≡ eps ∘nt (σ₁′ ◂ p)
    → β ≡ eps ∘nt (σ₂′ ◂ p)
    → σ₁′ ≡ σ₂′
  σ-uniq₂ β p q = sym (σ-uniq p) ∙ σ-uniq q

The first thing we’ll verify is that this construction is indeed dual to the left Kan extension. This is straightforward enough to do, but we have some administrative noise from all the opposite categories getting in the way.

module _ (p : Functor C C′) (F : Functor C D) where
  open Ran
  open _=>_

  Co-lan→Ran : Lan (Functor.op p) (Functor.op F) -> Ran p F
  Co-lan→Ran lan = ran where
    module lan = Lan lan
    ran : Ran p F
    ran .Ext = Functor.op lan.Ext
    ran .eps .η x = lan.eta .η x
    ran .eps .is-natural x y f = sym (lan.eta .is-natural y x f)

    ran .σ {M = M} α = op (lan.σ α′) where
      α′ : Functor.op F => Functor.op M F∘ Functor.op p
      α′ .η x = α .η x
      α′ .is-natural x y f = sym (α .is-natural y x f)

    ran .σ-comm = Nat-path λ x → lan.σ-comm ηₚ x
    ran .σ-uniq {M = M} {σ′ = σ′} p =
      Nat-path λ x → lan.σ-uniq {σ′ = σ′op} (Nat-path λ x → p ηₚ x) ηₚ x
      where
        σ′op : lan.Ext => Functor.op M
        σ′op .η x = σ′ .η x
        σ′op .is-natural x y f = sym (σ′ .is-natural y x f)

Computation🔗

Using the helper Co-lan→Ran defined above and the formula for computing left Kan extensions, we can formulate a condition for the existence of right Kan extensions based on the size and completeness of the categories involved. If $\mathcal{E}$ admits limits of $\kappa$-small diagrams, $\mathcal{C}$ is $\kappa$-small, and $\mathcal{D}$ is locally $\kappa$-small, then for any $p : \mathcal{C} \to \mathcal{D}$ and $F : \mathcal{D} \to \mathcal{E}$, the right Kan extension $\operatorname{Ran}_p F$ exists.

module _
  {o o′ ℓ κ} {C : Precategory κ κ} {D : Precategory o′ κ} {E : Precategory o ℓ}
  (lims : is-complete κ κ E) (p : Functor C D) (F : Functor C E)
  where

  complete→ran : Ran p F
  complete→ran =
    Co-lan→Ran p F $
      cocomplete→lan
        (λ F → Co-limit→Colimit (E ^op) (lims (Functor.op F)))
        (Functor.op p) (Functor.op F)

As before, it’s impossible to cheat the size limitations for computing Kan extensions as (co)limits, but this does not preclude the existence of extensions in other situations.