Previously: Tabulation Tribulations.

If you think of functor composition as a form of multiplication, Kan extensions are an attempt to construct inverses of this multiplication. But unlike multiplication, composition is not symmetric, so we have extensions that attempt to undo precomposition, and lifts that do the same for postcomposition. Furthermore, there rarely is a single inverse to any form of composition, so we have the parsimonious right extensions and lifts, and the generous left extensions and lifts. We end up with four combinations that correspond to four different adjunctions:

(- \circ j) \dashv \text{Ran}_j -

\text{Lan}_j - \dashv (- \circ j )

(j \circ -) \dashv \text{Rift}_j -

\text{Lift}_j - \dashv (j \circ -)

We’ll concentrate on the extensions, since we can provide explicit point-wise formulas for them in cases that are of interest to us, that is in \mathbf{Cat} and in \mathbb{P}rof.

Right Kan extensions

The definition of the right Kan extension relates the mapping out of the composition to the mapping into \text{Ran}. In Haskell, we can define them as two types:

type Phi  j s d = Compose s j ~> d
type Phi' j s d = s ~> Ran j d

The wavy arrows denote natural transformations:

type f ~> g = forall x. f x -> g x

To show that there is an adjunction we can either prove the (natural) isomorphism between Phi and Phi', or implement the unit and counit of the adjunction (together with zigzag identities):

eta     :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

In Haskell we can implement the right Kan extension as:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

This is a straightforward translation of the categorical formula that uses an end:

(\text{Ran}_j d) \,a = \int_x \text{Set}(C(a, j \,x), d \, x)

The adjunction can then be implemented as a pair of mappings:

leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
leftAdj phi sx = Ran (\x_jx -> phi (Compose (fmap x_jx sx)))
rightAdj ::  (Functor j, Functor d, Functor s) =>
   Phi' j s d -> Phi j s d
rightAdj phi' (Compose sj) = 
    let (Ran ran) = phi' sj
    in ran id

Or as the unit/counit pair:

eta :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
eta dx = Ran (\x_jx -> Compose (fmap x_jx dx))
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d
epsilon (Compose (Ran ran)) = ran id

Universal arrows

There is a third way, which gives a better starting point for generalizations. It can be used on an object-by-object basis, even if there is no global adjunction. It’s based on the idea of the universal arrow.

A universal arrow is a terminal object in the comma category. For a given functor L \colon D \to C, the comma category L/c consists of pairs (d, f \colon L d \to c). In other words, it’s a category of arrows from the image of L to some fixed object c \in C. Morphisms in the comma category are arrows h: d \to d' in D that make the corresponding triangles in C commute:

A terminal object in L/c is a pair (t, \tau) , through which every arrow \Phi \colon L d \to c factorizes uniquely. That means, there is a unique arrow h \colon d \to t that makes the following triangle commute:

If there is an adjunction L \dashv R, then we can easily construct the universal arrow as a pair (R c, \epsilon_c), where \epsilon_c is a component of the counit of the adjunction. Indeed, every \Phi \colon L d \to c factorizes through \epsilon_c:

\Phi = \epsilon_c \circ L \Phi'

where \Phi' = \text{leftAdj}\, \Phi.

The advantage of the universal arrow approach is that it’s pointwise. We can do it for each object c separately.

Reversing this process, rather than building an adjuncion, we can directly construct a universal arrow. We start by defining of a component of a counit. Then we postulate that any other counit-like mapping factorizes uniquely throught that counit.

Let’s see how it works for our definition of the right Kan extension. The counit has the following signature:

epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

We can illustrate it with the following string diagram:

In general, the functors go between three different categories: A, B, and M. In Haskell we have just one category and three endofunctors.

Any other mapping of this form has the signature (replacing Ran j d with an arbitrary functor s):

type Phi j s d = Compose s j ~> d

Or, as a string diagram:

We postulate that, for every Phi, there is a unique Phi' that factorizes it through epsilon. That is, we have a function:

leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d

such that:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = epsilon . Compose . leftAdj phi . getCompose

Modulo newtype shenanigans, this is exactly \epsilon \circ (L_j \Phi'), where L_j s = s \circ j is functor precomposition. Or as a string diagram:

Notice that rightAdj doesn’t appear anywhere in this construction.

The computational interpretation of this universal construction lets us calculate a mapping into a right Kan extension. Namely, to determine a natural transformation from some functor s to Ran j d, it’s enough to provide a mapping phi from Compose s j to d.

Left Kan extensions

We can now apply the same idea to the left Kan extension. This time we start with the unit:

eta :: (Functor j, Functor d) => d ~> Compose (Lan j d) j

We postulate that for any other mapping of this form (replacing Lan j d with and arbitrary s):

type Phi j s d = d ~> Compose s j

there is a unique Phi':

type Phi' j s d = Lan j d ~> s

that factorizes it through eta:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

In Haskell, the left Kan extension is given by the existential data type:

data Lan j d a where
    Lan :: (j x -> a) -> d x -> Lan j d a

In category theory, this formula uses a coend:

(\text{Lan}_j d) \, a = \int^x C(j \, x, a) \times d \, x

Indeed, for any given Phi, we can obtain a Phi' by applying this function:

rightAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
rightAdj d_sj (Lan jx_a dx) = 
    let Compose sjx = d_sj dx
    in fmap jx_a sjx

The result factorizes Phi through eta:

factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

The computational interpretation of this universal construction let us calculate a mapping out of the left Kan extension.

See Haskell code for right and left Kan extensions.

Next, we’ll generalize these construction to a double category setting.