module Cat.Functor.Kan.Base where

Left Kan extensionsπŸ”—

Suppose we have a functor and a functor β€” perhaps to be thought of as a full subcategory inclusion, where is a completion of 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

extending to a functor 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 along and denote it 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 is equipped with a natural transformation 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 is another functor with a transformation there is a unique natural transformation which commutes with

Note that in general the triangle commutes β€œweakly”, but when is fully faithful and is cocomplete, genuinely extends in that 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 has a natural transformation witnessing the same β€œdirected commutativity” that does for 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 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
module _ {p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eta : F => G F∘ p} where
  is-lan-is-prop : is-prop (is-lan p F G eta)
  is-lan-is-prop a b = path where
    private
      module a = is-lan a
      module b = is-lan b

    σ≑ : {M : Functor _ _} (Ξ± : F => M F∘ p) β†’ a.Οƒ Ξ± ≑ b.Οƒ Ξ±
    σ≑ Ξ± = ext (a.Οƒ-uniq (sym b.Οƒ-comm) Ξ·β‚š_)

    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

  instance
    H-Level-is-lan : βˆ€ {k} β†’ H-Level (is-lan p F G eta) (suc k)
    H-Level-is-lan = prop-instance is-lan-is-prop

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

    σ≑ : {M : Functor _ _} (Ξ± : M F∘ p => F) β†’ a.Οƒ Ξ± ≑ b.Οƒ Ξ±
    σ≑ Ξ± = ext (a.Οƒ-uniq (sym b.Οƒ-comm) Ξ·β‚š_)

    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

  instance
    H-Level-is-ran : βˆ€ {k} β†’ H-Level (is-ran p F G eps) (suc k)
    H-Level-is-ran = prop-instance is-ran-is-prop

Preservation and reflection of Kan extensionsπŸ”—

Let be the left Kan extension of along and suppose that is a functor. We can β€œapply” 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 preserves

  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 Unfortunately, proof assistants; our definition of whiskering lands in but we require a natural transformation to

We say that a Kan extension is absolute if it is preserved by all functors out of An important class of examples is 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 is already a left kan extension of along We say that reflects this Kan extension if is a also a left extension of along

  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

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