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.