open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Coherence
open import Cat.Instances.Functor
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

module Cat.Functor.Kan.Base where

private
variable
o ℓ : Level
C C' D E : Precategory o ℓ
kan-lvl : ∀ {o ℓ o' ℓ' o'' ℓ''} {C : Precategory o ℓ} {C' : Precategory o' ℓ'} {D : Precategory o'' ℓ''}
→ Functor C D → Functor C C' → Level
kan-lvl {a} {b} {c} {d} {e} {f} _ _ = a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ f

open _=>_


# Left Kan extensions🔗

Suppose we have a functor $F : \mathcal{C} \to \mathcal{D}$, and a functor $p : \mathcal{C} \to \mathcal{C}'$ — perhaps to be thought of as a full subcategory inclusion, where $\mathcal{C}'$ is a completion of $\mathcal{C}$, but the situation applies just as well to any pair of functors — which naturally fit into a commutative diagram  but as we can see this is a particularly sad commutative diagram; it’s crying out for a third edge $\mathcal{C}' \to \mathcal{D}$  extending $F$ to a functor $\mathcal{C}' \to \mathcal{D}$. If there exists an universal such extension (we’ll define what “universal” means in just a second), we call it the left Kan extension of $F$ along $p$, and denote it $\operatorname{Lan}_p F$. Such extensions do not come for free (in a sense they’re pretty hard to come by), but concept of Kan extension can be used to rephrase the definition of both limit and adjoint functor.

A left Kan extension $\operatorname{Lan}_p F$ is equipped with a natural transformation $\eta : F \Rightarrow \operatorname{Lan}_p F \circ p$ witnessing the (“directed”) commutativity of the triangle (so that it need not commute on-the-nose) which is universal among such transformations; Meaning that if $M : \mathcal{C'} \to \mathcal{D}$ is another functor with a transformation $\alpha : F \Rightarrow M \circ p$, there is a unique natural transformation $\sigma : \operatorname{Lan}_p F \Rightarrow M$ which commutes with $\alpha$.

Note that in general the triangle commutes “weakly”, but when $p$ is fully faithful and $\mathcal{D}$ is cocomplete, $\operatorname{Lan}_p F$ genuinely extends $p$, in that $\eta$ is a natural isomorphism.

record
is-lan (p : Functor C C') (F : Functor C D) (L : Functor C' D) (eta : F => L F∘ p)
: Type (kan-lvl p F) where
field


Universality of eta is witnessed by the following fields, which essentially say that, in the diagram below (assuming $M$ has a natural transformation $\alpha$ witnessing the same “directed commutativity” that $\eta$ does for $\operatorname{Lan}_p F$), the 2-cell exists and is unique.  σ : {M : Functor C' D} (α : F => M F∘ p) → L => M
σ-comm : {M : Functor C' D} {α : F => M F∘ p} → (σ α ◂ p) ∘nt eta ≡ α
σ-uniq : {M : Functor C' D} {α : F => M F∘ p} {σ' : L => M}
→ α ≡ (σ' ◂ p) ∘nt eta
→ σ α ≡ σ'

σ-uniq₂
: {M : Functor C' D} (α : F => M F∘ p) {σ₁' σ₂' : L => M}
→ α ≡ (σ₁' ◂ p) ∘nt eta
→ α ≡ (σ₂' ◂ p) ∘nt eta
→ σ₁' ≡ σ₂'
σ-uniq₂ β p q = sym (σ-uniq p) ∙ σ-uniq q

σ-uniqp
: ∀ {M₁ M₂ : Functor C' D}
→ {α₁ : F => M₁ F∘ p} {α₂ : F => M₂ F∘ p}
→ (q : M₁ ≡ M₂)
→ PathP (λ i → F => q i F∘ p) α₁ α₂
→ PathP (λ i → L => q i) (σ α₁) (σ α₂)
σ-uniqp q r = Nat-pathp refl q λ c' i →
σ {M = q i} (r i) .η c'

open _=>_ eta


We also provide a bundled form of this data.

record Lan (p : Functor C C') (F : Functor C D) : Type (kan-lvl p F) where
field
Ext     : Functor C' D
eta     : F => Ext F∘ p
has-lan : is-lan p F Ext eta

module Ext = Func Ext
open is-lan has-lan public


# Right Kan extensions🔗

Our choice of universal property in the section above isn’t the only choice; we could instead require a terminal solution to the lifting problem, instead of an initial one. We can picture the terminal situation using the following 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 is-ran
(p : Functor C C') (F : Functor C D) (Ext : Functor C' D)
(eps : Ext F∘ p => F)
: Type (kan-lvl p F) where
no-eta-equality

field
σ : {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)
→ σ β ≡ σ'

open _=>_ eps renaming (η to ε)

σ-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

record Ran (p : Functor C C') (F : Functor C D) : Type (kan-lvl p F) where
no-eta-equality
field
Ext     : Functor C' D
eps     : Ext F∘ p => F
has-ran : is-ran p F Ext eps

module Ext = Func Ext
open is-ran has-ran public

is-lan-is-prop
: {p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eta : F => G F∘ p}
→ is-prop (is-lan p F G eta)
is-lan-is-prop {p = p} {F} {G} {eta} a b = path where
private
module a = is-lan a
module b = is-lan b

σ≡ : {M : Functor _ _} (α : F => M F∘ p) → a.σ α ≡ b.σ α
σ≡ α = Nat-path λ x → a.σ-uniq (sym b.σ-comm) ηₚ x

open is-lan
path : a ≡ b
path i .σ α = σ≡ α i
path i .σ-comm {α = α} =
is-prop→pathp (λ i → Nat-is-set ((σ≡ α i ◂ p) ∘nt eta) α)
(a.σ-comm {α = α}) (b.σ-comm {α = α})
i
path i .σ-uniq {α = α} β =
is-prop→pathp (λ i → Nat-is-set (σ≡ α i) _)
(a.σ-uniq β) (b.σ-uniq β)
i

is-ran-is-prop
: {p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eps : G F∘ p => F}
→ is-prop (is-ran p F G eps)
is-ran-is-prop {p = p} {F} {G} {eps} a b = path where
private
module a = is-ran a
module b = is-ran b

σ≡ : {M : Functor _ _} (α : M F∘ p => F) → a.σ α ≡ b.σ α
σ≡ α = Nat-path λ x → a.σ-uniq (sym b.σ-comm) ηₚ x

open is-ran
path : a ≡ b
path i .σ α = σ≡ α i
path i .σ-comm {β = α} =
is-prop→pathp (λ i → Nat-is-set (eps ∘nt (σ≡ α i ◂ p)) α)
(a.σ-comm {β = α}) (b.σ-comm {β = α})
i
path i .σ-uniq {β = α} γ =
is-prop→pathp (λ i → Nat-is-set (σ≡ α i) _)
(a.σ-uniq γ) (b.σ-uniq γ)
i


# Preservation and reflection of Kan extensions🔗

Let $(G : C' \to D, \eta : F \to G \circ p)$ be the left Kan extension of $F : C \to D$ along $p : C \to C'$, and suppose that $H : D \to E$ is a functor. We can “apply” $H$ to all the data of the Kan extension, obtaining the following diagram.  This looks like yet another Kan extension diagram, but it may not be universal! If this diagram is a left Kan extension, we say that $H$ preserves $(G, \eta)$.

module _
{p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eta : F => G F∘ p} where

  preserves-lan : (H : Functor D E) → is-lan p F G eta → Type _
preserves-lan H _ =
is-lan p (H F∘ F) (H F∘ G) (nat-assoc-to (H ▸ eta))


In the diagram above, the 2-cell is simply the whiskering $H\eta$. Unfortunately, proof assistants; our definition of whiskering lands in $H(Gp)$, but we requires a natural transformation to $(HG)p$.

We say that a Kan extension is absolute if it is preserved by all functors out of $D$. An important class of examples given by adjoint functors.

  is-absolute-lan : is-lan p F G eta → Typeω
is-absolute-lan lan =
{o ℓ : Level} {E : Precategory o ℓ} (H : Functor D E) → preserves-lan H lan


It may also be the case that $(HG, H\eta)$ is already a left kan extension of $HF$ along $p$. We say that $H$ reflects this Kan extension if $G, \eta$ is a also a left extension of $F$ along $p$.

  reflects-lan
: (H : Functor D E)
→ is-lan p (H F∘ F) (H F∘ G) (nat-assoc-to (H ▸ eta))
→ Type _
reflects-lan _ _ =
is-lan p F G eta

module _
{p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eps : G F∘ p => F} where


We can define dual notions for right Kan extensions as well.

  preserves-ran : (H : Functor D E) → is-ran p F G eps → Type _
preserves-ran H _ =
is-ran p (H F∘ F) (H F∘ G) (nat-assoc-from (H ▸ eps))

is-absolute-ran : is-ran p F G eps → Typeω
is-absolute-ran ran =
{o ℓ : Level} {E : Precategory o ℓ} (H : Functor D E) → preserves-ran H ran

reflects-ran
: (H : Functor D E)
→ is-ran p (H F∘ F) (H F∘ G) (nat-assoc-from (H ▸ eps))
→ Type _
reflects-ran _ _ =
is-ran p F G eps

to-lan
: ∀ {p : Functor C C'} {F : Functor C D} {L : Functor C' D} {eta : F => L F∘ p}
→ is-lan p F L eta
→ Lan p F
to-lan {L = L} lan .Lan.Ext = L
to-lan {eta = eta} lan .Lan.eta = eta
to-lan lan .Lan.has-lan = lan