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 : \ca{C} \to \ca{D}$ along a functor $p : \ca{C}' \to \ca{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 $\eps$ 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 β ap (Ξ» e β e .Ξ· _) lan.Ο-comm
ran .Ο-uniq {M = M} {Οβ² = Οβ²} p =
Nat-path Ξ» x β ap (Ξ» e β e .Ξ· x) $lan.Ο-uniq {Οβ² = Οβ²op}$ Nat-path Ξ» x β
ap (Ξ» e β e .Ξ· x) p
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 $\ca{E}$ admits limits of $\kappa$-small diagrams, $\ca{C}$ is $\kappa$-small, and $\ca{D}$ is locally $\kappa$-small, then for any $p : \ca{C} \to \ca{D}$ and $F : \ca{D} \to \ca{E}$, the right Kan extension $\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.