Kan extensions, in Kan.

What a Kan extension is

Given a functor F : A → D and a functor p : A → B, the left Kan extension of F along p is the best approximation of F by a functor on all of B: a functor L : B → D with a natural transformation η : F ⇒ L∘p that is universal — every competitor (G, γ : F ⇒ G∘p) factors through a unique mediating σ : L ⇒ G.

In Kan a SmallCategory is a dependent record whose laws are fields, so this universal property is not prose — it is a type the checker accepts:

-- std/kan.kan — the left Kan extension of F along p, as a universal property
def LeftKanExt : (A : SmallCategory) -> (B : SmallCategory) -> (D : SmallCategory)
                 -> Functor A B -> Functor A D -> U
  = lambda A B D p F:
      (L : Functor B D)                                          -- the extending functor
    * (unit : NatTrans A D F (compFunctor A B D p L))            -- η : F ⇒ L∘p
    * ((G : Functor B D) -> NatTrans A D F (compFunctor A B D p G)
                         -> NatTrans B D L G)                    -- the mediating σ

The right Kan extension is the exact dual (mapping in): see RightKanExt.

1 Extend along the identity — and get F back

The simplest genuine Kan extension: every functor is its own extension along the identity. Take L = F and let the unit be the identity F ⇒ F∘id = F. It holds for any F, in both variances — and it type-checks, so it is proven.

-- std/kan.kan — a functor is its own Kan extension along the identity
def lanAlongId : (A : SmallCategory) -> (D : SmallCategory) -> (F : Functor A D)
                 -> LeftKanExt A A D (idFunctor A) F
  = lambda A D F: ( F , ( idNat A D F , lambda G gamma: gamma ) )

-- and the dual, ranAlongId, along the same lines.

Instantiated concretely, the extension really recovers F — this equation is refl:

def lanId : LeftKanExt One One One (idFunctor One) F = lanAlongId One One F
def lanId_recovers_F : Id (Functor One One) (fst lanId) F = refl   -- L = F ✓

2 The universal property computes

A Kan extension isn’t just a functor — it carries its universal mediating map. You can pull that map out of the extension and run it: hand it any competitor (G, γ) and it returns the factoring σ : L ⇒ G. The property doesn’t merely hold — it computes.

-- pull the mediator out of the extension …
def lanId_mediator
  : (G : Functor One One)
    -> NatTrans One One F (compFunctor One One One (idFunctor One) G)
    -> NatTrans One One F G
  = snd (snd lanId)

-- … and run it: out comes a genuine natural transformation σ : F ⇒ F.
def lanId_sigma : NatTrans One One F F = lanId_mediator F (idNat One One F)

3 “All concepts are Kan extensions”

The slogan is Mac Lane’s. In Kan it becomes a definition the checker accepts. The unique functor A → 1 to the terminal category turns limits and colimits into Kan extensions:

-- the unique functor to the terminal category 1
def toOne : (A : SmallCategory) -> Functor A One
  = lambda A: ( lambda a: unit , ( lambda a b f: unit , ( lambda a: refl , lambda a b c g f: refl ) ) )

-- a COLIMIT of F is its left Kan extension along A -> 1
def ColimitOf : (A : SmallCategory) -> (D : SmallCategory) -> Functor A D -> U
  = lambda A D F: LeftKanExt A One D (toOne A) F

-- a LIMIT of F is the right Kan extension along A -> 1
def LimitOf : (A : SmallCategory) -> (D : SmallCategory) -> Functor A D -> U
  = lambda A D F: RightKanExt A One D (toOne A) F

These are well-formed Kan types — the slogan is not a metaphor here, it is a statement the checker accepts. Inhabiting them for a general A is the theory of (co)limits (needs coends — Kan’s next frontier); the identity extensions above are the base cases Kan already builds and verifies.

Check it yourself

Every snippet on this page is real code from the repository. Nothing here is a diagram of intent — it is a diagram Kan filled.

$ kan check examples/kan_extensions.kan
# ...every definition type-checks — which, in Kan, means it holds.

the language named for Kan extensions can express, and check, Kan extensions