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