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
    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
    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-is-lan : (H : Functor D E) β†’ is-lan p F G eta β†’ Type _
  preserves-is-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-is-lan H lan

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

  preserves-is-ran : (H : Functor D E) β†’ is-ran p F G eps β†’ Type _
  preserves-is-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-is-ran H ran

It may also be the case that is already a Kan extension of along We say that reflects this Kan extension if is a also an extension of along

  reflects-lan
    : (H : Functor D E)
    β†’ Type _
  reflects-lan H =
    βˆ€ {G : Functor C' D} {eta : F => G F∘ p}
    β†’ is-lan p (H F∘ F) (H F∘ G) (nat-assoc-to (H β–Έ eta))
    β†’ is-lan p F G eta

  reflects-ran
    : (H : Functor D E)
    β†’ Type _
  reflects-ran H =
    βˆ€ {G : Functor C' D} {eps : G F∘ p => F}
    β†’ is-ran p (H F∘ F) (H F∘ G) (nat-assoc-from (H β–Έ eps))
    β†’ is-ran p F G eps

Lifting and creation of Kan extensionsπŸ”—

While the notions of lifted and created limits are commonplace in the literature on category theory, their evident generalisations to Kan extensions are less often encountered. We define those here, but refer the reader to the page about limits for more details.

Given a Kan extension of along we say that lifts this extension if there is a Kan extension of along that is preserved by

  record lifts-lan (lan : Lan p (H F∘ F)) : Type (kan-lvl p F βŠ” cat-lvl E) where
    no-eta-equality
    field
      lifted : Lan p F
      preserved : preserves-is-lan H (Lan.has-lan lifted)

  record lifts-ran (ran : Ran p (H F∘ F)) : Type (kan-lvl p F βŠ” cat-lvl E) where
    no-eta-equality
    field
      lifted : Ran p F
      preserved : preserves-is-ran H (Ran.has-ran lifted)

We say that creates Kan extensions of along if it lifts them and reflects them.

  record creates-lan : Type (kan-lvl p F βŠ” cat-lvl E) where
    no-eta-equality
    field
      has-lifts-lan : (lan : Lan p (H F∘ F)) β†’ lifts-lan H lan
      reflects : reflects-lan p F H

  record creates-ran : Type (kan-lvl p F βŠ” cat-lvl E) where
    no-eta-equality
    field
      has-lifts-ran : (ran : Ran p (H F∘ F)) β†’ lifts-ran H ran
      reflects : reflects-ran p F H