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