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:C→DF : \mathcal{C} \to \mathcal{D} along a functor p:C′→Cp : \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
    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)
           β†’ Οƒ Ξ² ≑ Οƒβ€²

    : {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
        Οƒβ€²op : lan.Ext => Functor.op M
        Οƒβ€²op .Ξ· x = Οƒβ€² .Ξ· x
        Οƒβ€²op .is-natural x y f = sym (Οƒβ€² .is-natural y x f)


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 E\mathcal{E} admits limits of ΞΊ\kappa-small diagrams, C\mathcal{C} is ΞΊ\kappa-small, and D\mathcal{D} is locally ΞΊ\kappa-small, then for any p:Cβ†’Dp : \mathcal{C} \to \mathcal{D} and F:Dβ†’EF : \mathcal{D} \to \mathcal{E}, the right Kan extension Ran⁑pF\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)

  complete→ran : Ran p F
  complete→ran =
    Co-lan→Ran p F $
        (λ 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.