% !TEX root = ../../ctfp-print.tex

\lettrine[lhang=0.17]{S}{o far we've been} mostly working with a single category or a pair of
categories. In some cases that was a little too constraining.

For instance, when defining a limit in a category $\cat{C}$, we introduced an
index category $\cat{I}$ as the template for the pattern that would
form the basis for our cones. It would have made sense to introduce
another category, a trivial one, to serve as a template for the apex of
the cone. Instead we used the constant functor $\Delta_c$ from
$\cat{I}$ to $\cat{C}$.

It's time to fix this awkwardness. Let's define a limit using three
categories. Let's start with the functor $D$ from the index
category $\cat{I}$ to $\cat{C}$. This is the functor that selects the base
of the cone --- the diagram functor.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan2.jpg}
\end{figure}

\noindent
The new addition is the category $\cat{1}$ that contains a single
object (and a single identity morphism). There is only one possible
functor $K$ from $\cat{I}$ to this category. It maps all objects
to the only object in $\cat{1}$, and all morphisms to the identity
morphism. Any functor $F$ from $\cat{1}$ to $\cat{C}$ picks a
potential apex for our cone.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan15.jpg}
\end{figure}

\noindent
A cone is a natural transformation $\varepsilon$ from $F \circ K$ to
$D$. Notice that $F \circ K$ does exactly the same thing as
our original $\Delta_c$. The following diagram shows this
transformation.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan3-e1492120491591.jpg}
\end{figure}

\noindent
We can now define a universal property that picks the ``best'' such
functor $F$. This $F$ will map $\cat{1}$ to the object
that is the limit of $D$ in $\cat{C}$, and the natural
transformation $\varepsilon$ from $F \circ K$ to $D$ will
provide the corresponding projections. This universal functor is called
the right Kan extension of $D$ along $K$ and is denoted by
$\Ran_{K}D$.

Let's formulate the universal property. Suppose we have another cone ---
that is another functor $F'$ together with a natural
transformation $\varepsilon'$ from $F' \circ K$ to
$D$.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan31-e1492120512209.jpg}
\end{figure}

\noindent
If the Kan extension $F = Ran_{K}D$ exists, there must be a unique
natural transformation $\sigma$ from $F'$ to it, such
that $\varepsilon'$ factorizes through $\varepsilon$, that is:
\[\varepsilon' = \varepsilon\ .\ (\sigma \circ K)\]
Here, $\sigma \circ K$ is the horizontal composition of two natural
transformations (one of them being the identity natural transformation
on $K$). This transformation is then vertically composed with
$\varepsilon$.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan5.jpg}
\end{figure}

\noindent
In components, when acting on an object $i$ in $\cat{I}$, we get:
\[\varepsilon'_i = \varepsilon_i \circ \sigma_{K i}\]
In our case, $\sigma$ has only one component corresponding to the
single object of $\cat{1}$. So, indeed, this is the unique morphism
from the apex of the cone defined by $F'$ to the apex of
the universal cone defined by $\Ran_{K}D$. The commuting conditions
are exactly the ones required by the definition of a limit.

But, importantly, we are free to replace the trivial category $\cat{1}$
with an arbitrary category $\cat{A}$, and the definition of the right Kan
extension remains valid.

\section{Right Kan Extension}

The right Kan extension of the functor $D \Colon \cat{I} \to \cat{C}$
along the functor $K \Colon \cat{I} \to \cat{A}$ is a functor
$F \Colon \cat{A} \to \cat{C}$ (denoted $\Ran_{K}D$) together with a
natural transformation
\[\varepsilon \Colon F \circ K \to D\]
such that for any other functor $F' \Colon \cat{A} \to \cat{C}$ and
a natural transformation
\[\varepsilon' \Colon F' \circ K \to D\]
there is a unique natural transformation
\[\sigma \Colon F' \to F\]
that factorizes $\varepsilon'$:
\[\varepsilon' = \varepsilon\ .\ (\sigma \circ K)\]
This is quite a mouthful, but it can be visualized in this nice diagram:

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan7.jpg}
\end{figure}

\noindent
An interesting way of looking at this is to notice that, in a sense, the
Kan extension acts like the inverse of ``functor multiplication.'' Some
authors go as far as use the notation $D/K$ for $\Ran_{K}D$.
Indeed, in this notation, the definition of $\varepsilon$, which is also
called the counit of the right Kan extension, looks like simple
cancellation:
\[\varepsilon \Colon D/K \circ K \to D\]
There is another interpretation of Kan extensions. Consider that the
functor $K$ embeds the category $\cat{I}$ inside $\cat{A}$. In the
simplest case $\cat{I}$ could just be a subcategory of $\cat{A}$. We have
a functor $D$ that maps $\cat{I}$ to $\cat{C}$. Can we extend
$D$ to a functor $F$ that is defined on the whole of
$\cat{A}$? Ideally, such an extension would make the composition
$F \circ K$ be isomorphic to $D$. In other words, $F$
would be extending the domain of $D$ to $\cat{A}$. But a
full-blown isomorphism is usually too much to ask, and we can do with
just half of it, namely a one-way natural transformation $\varepsilon$ from
$F \circ K$ to $D$. (The left Kan extension picks the other direction.)

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan6.jpg}
\end{figure}

\noindent
Of course, the embedding picture breaks down when the functor $K$
is not injective on objects or not faithful on hom-sets, as in the
example of the limit. In that case, the Kan extension tries its best to
extrapolate the lost information.

\section{Kan Extension as Adjunction}

Now suppose that the right Kan extension exists for any $D$ (and
a fixed $K$). In that case $\Ran_{K}-$ (with the dash
replacing $D$) is a functor from the functor category
${[}\cat{I}, \cat{C}{]}$ to the functor category ${[}\cat{A}, \cat{C}{]}$. It
turns out that this functor is the right adjoint to the precomposition
functor $- \circ K$. The latter maps functors in ${[}\cat{A}, \cat{C}{]}$
to functors in ${[}\cat{I}, \cat{C}{]}$. The adjunction is:
\[[\cat{I}, \cat{C}](F' \circ K, D) \cong [\cat{A}, \cat{C}](F', \Ran_{K}D)\]
It is just a restatement of the fact that to every natural
transformation we called $\varepsilon'$ corresponds a unique natural
transformation we called $\sigma$.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan92.jpg}
\end{figure}

\noindent
Furthermore, if we chose the category $\cat{I}$ to be the same as
$\cat{C}$, we can substitute the identity functor $I_{\cat{C}}$ for
$D$. We get the following identity:
\[[\cat{C}, \cat{C}](F' \circ K, I_{\cat{C}}) \cong [\cat{A}, \cat{C}](F', \Ran_{K}I_{\cat{C}})\]
We can now chose $F'$ to be the same as $\Ran_{K}I_{\cat{C}}$. In
that case the right hand side contains the identity natural
transformation and, corresponding to it, the left hand side gives us the
following natural transformation:
\[\varepsilon \Colon \Ran_{K}I_{\cat{C}} \circ K \to I_{\cat{C}}\]
This looks very much like the counit of an adjunction:
\[\Ran_{K}I_{\cat{C}} \dashv K\]
Indeed, the right Kan extension of the identity functor along a functor
$K$ can be used to calculate the left adjoint of $K$. For
that, one more condition is necessary: the right Kan extension must be
preserved by the functor $K$. The preservation of the extension
means that, if we calculate the Kan extension of the functor precomposed
with $K$, we should get the same result as precomposing the
original Kan extension with $K$. In our case, this condition
simplifies to:
\[K \circ \Ran_{K}I_{\cat{C}} \cong \Ran_{K}K\]
Notice that, using the division-by-$K$ notation, the adjunction can be
written as:
\[I/K \dashv K\]
which confirms our intuition that an adjunction describes some kind of
an inverse. The preservation condition becomes:
\[K \circ I/K \cong K/K\]
The right Kan extension of a functor along itself, $K/K$, is
called a codensity monad.

The adjunction formula is an important result because, as we'll see
soon, we can calculate Kan extensions using ends (coends), thus giving
us practical means of finding right (and left) adjoints.

\section{Left Kan Extension}

There is a dual construction that gives us the left Kan extension. To
build some intuition, we'll can start with the definition of a colimit
and restructure it to use the singleton category $\cat{1}$. We build a
cocone by using the functor $D \Colon \cat{I} \to \cat{C}$ to form its
base, and the functor $F \Colon \cat{1} \to \cat{C}$ to select its apex.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan81.jpg}
\end{figure}

\noindent
The sides of the cocone, the injections, are components of a natural
transformation $\eta$ from $D$ to $F \circ K$.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan10a.jpg}
\end{figure}

\noindent
The colimit is the universal cocone. So for any other functor
$F'$ and a natural transformation
\[\eta' \Colon D \to F' \circ K\]

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan10b.jpg}
\end{figure}

\noindent
there is a unique natural transformation $\sigma$ from $F$ to $F'$

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan14.jpg}
\end{figure}

\noindent
such that:
\[\eta' = (\sigma \circ K)\ .\ \eta\]
This is illustrated in the following diagram:

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan112.jpg}
\end{figure}

\noindent
Replacing the singleton category $\cat{1}$ with $\cat{A}$, this
definition naturally generalized to the definition of the left Kan
extension, denoted by $\Lan_{K}D$.

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan12.jpg}
\end{figure}

\noindent
The natural transformation:
\[\eta \Colon D \to \Lan_{K}D \circ K\]
is called the unit of the left Kan extension.

As before, we can recast the one-to-one correspondence between natural
transformations:
\[\eta' = (\sigma \circ K)\ .\ \eta\]
in terms of the adjunction:
\[[\cat{A}, \cat{C}](\Lan_{K}D, F') \cong [\cat{I}, \cat{C}](D, F' \circ K)\]
In other words, the left Kan extension is the left adjoint, and the
right Kan extension is the right adjoint of the precomposition with
$K$.

Just like the right Kan extension of the identity functor could be used
to calculate the left adjoint of $K$, the left Kan extension of
the identity functor turns out to be the right adjoint of $K$
(with $\eta$ being the unit of the adjunction):
\[K \dashv \Lan_{K}I_{\cat{C}}\]
Combining the two results, we get:
\[\Ran_{K}I_{\cat{C}} \dashv K \dashv \Lan_{K}I_{\cat{C}}\]

\section{Kan Extensions as Ends}

The real power of Kan extensions comes from the fact that they can be
calculated using ends (and coends). For simplicity, we'll restrict our
attention to the case where the target category $\cat{C}$ is
$\Set$, but the formulas can be extended to any category.

Let's revisit the idea that a Kan extension can be used to extend the
action of a functor outside of its original domain. Suppose that
$K$ embeds $\cat{I}$ inside $\cat{A}$. Functor $D$ maps
$\cat{I}$ to $\Set$. We could just say that for any object
$a$ in the image of $K$, that is $a = K i$, the
extended functor maps $a$ to $D i$. The problem is, what
to do with those objects in $\cat{A}$ that are outside of the image of
$K$? The idea is that every such object is potentially connected
through lots of morphisms to every object in the image of $K$. A
functor must preserve these morphisms. The totality of morphisms from an
object $a$ to the image of $K$ is characterized by the
hom-functor:
\[\cat{A}(a, K -)\]

\begin{figure}[H]
  \centering
  \includegraphics[width=0.4\textwidth]{images/kan13.jpg}
\end{figure}

\noindent
Notice that this hom-functor is a composition of two functors:
\[\cat{A}(a, K -) = \cat{A}(a, -) \circ K\]
The right Kan extension is the right adjoint of functor composition:
\[[\cat{I}, \Set](F' \circ K, D) \cong [\cat{A}, \Set](F', \Ran_{K}D)\]
Let's see what happens when we replace $F'$ with the hom
functor:
\[[\cat{I}, \Set](\cat{A}(a, -) \circ K, D) \cong [\cat{A}, \Set](\cat{A}(a, -), \Ran_{K}D)\]
and then inline the composition:
\[[\cat{I}, \Set](\cat{A}(a, K -), D) \cong [\cat{A}, \Set](\cat{A}(a, -), \Ran_{K}D)\]
The right hand side can be reduced using the Yoneda lemma:
\[[\cat{I}, \Set](\cat{A}(a, K -), D) \cong \Ran_{K}D a\]
We can now rewrite the set of natural transformations as the end to get
this very convenient formula for the right Kan extension:
\[\Ran_{K}D a \cong \int_i \Set(\cat{A}(a, K i), D i)\]
There is an analogous formula for the left Kan extension in terms of a
coend:
\[\Lan_{K}D a = \int^i \cat{A}(K i, a)\times{}D i\]
To see that this is the case, we'll show that this is indeed the left
adjoint to functor composition:
\[[\cat{A}, \Set](\Lan_{K}D, F') \cong [\cat{I}, \Set](D, F' \circ K)\]
Let's substitute our formula in the left hand side:
\[[\cat{A}, \Set](\int^i \cat{A}(K i, -)\times{}D i, F')\]
This is a set of natural transformations, so it can be rewritten as an
end:
\[\int_a \Set(\int^i \cat{A}(K i, a)\times{}D i, F' a)\]
Using the continuity of the hom-functor, we can replace the coend with
the end:
\[\int_a \int_i \Set(\cat{A}(K i, a)\times{}D i, F' a)\]
We can use the product-exponential adjunction:
\[\int_a \int_i \Set(\cat{A}(K i, a),\ (F' a)^{D i})\]
The exponential is isomorphic to the corresponding hom-set:
\[\int_a \int_i \Set(\cat{A}(K i, a),\ \Set(D i, F' a))\]
There is a theorem called the Fubini theorem that allows us to swap the
two ends:
\[\int_i \int_a \Set(\cat{A}(K i, a),\ \Set(D i, F' a))\]
The inner end represents the set of natural transformations between two
functors, so we can use the Yoneda lemma:
\[\int_i \Set(D i, F' (K i))\]
This is indeed the set of natural transformations that forms the right
hand side of the adjunction we set out to prove:
\[[\cat{I}, \Set](D, F' \circ K)\]
These kinds of calculations using ends, coends, and the Yoneda lemma are
pretty typical for the ``calculus'' of ends.

\section{Kan Extensions in Haskell}

The end/coend formulas for Kan extensions can be easily translated to
Haskell. Let's start with the right extension:
\[\Ran_{K}D a \cong \int_i \Set(\cat{A}(a, K i), D i)\]
We replace the end with the universal quantifier, and hom-sets with
function types:

\src{snippet01}
Looking at this definition, it's clear that \code{Ran} must contain a
value of type \code{a} to which the function can be applied, and a
natural transformation between the two functors \code{k} and
\code{d}. For instance, suppose that \code{k} is the tree functor,
and \code{d} is the list functor, and you were given a
\code{Ran Tree {[}{]} String}. If you pass it a function:

\src{snippet02}
you'll get back a list of \code{Int}, and so on. The right Kan
extension will use your function to produce a tree and then repackage it
into a list. For instance, you may pass it a parser that generates a
parsing tree from a string, and you'll get a list that corresponds to
the depth-first traversal of this tree.

The right Kan extension can be used to calculate the left adjoint of a
given functor by replacing the functor \code{d} with the identity
functor. This leads to the left adjoint of a functor \code{k} being
represented by the set of polymorphic functions of the type:

\src{snippet03}
Suppose that \code{k} is the forgetful functor from the category of
monoids. The universal quantifier then goes over all monoids. Of course,
in Haskell we cannot express monoidal laws, but the following is a
decent approximation of the resulting free functor (the forgetful
functor \code{k} is an identity on objects):

\src{snippet04}
As expected, it generates free monoids, or Haskell lists:

\src{snippet05}
The left Kan extension is a coend:
\[\Lan_{K}D a = \int^i \cat{A}(K i, a)\times{}D i\]
so it translates to an existential quantifier. Symbolically:

\begin{snip}{haskell}
Lan k d a = exists i. (k i -> a, d i)
\end{snip}
This can be encoded in Haskell using \acronym{GADT}s, or using a universally
quantified data constructor:

\src{snippet06}
The interpretation of this data structure is that it contains a function
that takes a container of some unspecified \code{i}s and produces an
\code{a}. It also has a container of those \code{i}s. Since you have
no idea what \code{i}s are, the only thing you can do with this data
structure is to retrieve the container of \code{i}s, repack it into
the container defined by the functor \code{k} using a natural
transformation, and call the function to obtain the \code{a}. For
instance, if \code{d} is a tree, and \code{k} is a list, you can
serialize the tree, call the function with the resulting list, and
obtain an \code{a}.

The left Kan extension can be used to calculate the right adjoint of a
functor. We know that the right adjoint of the product functor is the
exponential, so let's try to implement it using the Kan extension:

\src{snippet07}
This is indeed isomorphic to the function type, as witnessed by the
following pair of functions:

\src{snippet08}
Notice that, as described earlier in the general case, we performed the
following steps:

\begin{enumerate}
  \tightlist
  \item
        Retrieved the container of \code{x} (here, it's
        just a trivial identity container), and the function \code{f}.
  \item
        Repackaged the container using the natural transformation between the
        identity functor and the pair functor.
  \item
        Called the function \code{f}.
\end{enumerate}

\section{Free Functor}

An interesting application of Kan extensions is the construction of a
free functor. It's the solution to the following practical problem:
suppose you have a type constructor --- that is a mapping of objects. Is
it possible to define a functor based on this type constructor? In other
words, can we define a mapping of morphisms that would extend this type
constructor to a full-blown endofunctor?

The key observation is that a type constructor can be described as a
functor whose domain is a discrete category. A discrete category has no
morphisms other than the identity morphisms. Given a category $\cat{C}$,
we can always construct a discrete category $\cat{|C|}$
by simply discarding all non-identity morphisms. A functor $F$
from $\cat{|C|}$ to $\cat{C}$ is then a simple mapping
of objects, or what we call a type constructor in Haskell. There is also
a canonical functor $J$ that injects $\cat{|C|}$
into $\cat{C}$: it's an identity on objects (and on identity morphisms).
The left Kan extension of $F$ along $J$, if it exists, is
then a functor for $\cat{C}$ to $\cat{C}$:
\[\Lan_{J}F a = \int^i \cat{C}(J i, a)\times{}F i\]
It's called a free functor based on $F$.

In Haskell, we would write it as:

\src{snippet09}
Indeed, for any type constructor \code{f}, \code{FreeF f} is a
functor:

\src{snippet10}
As you can see, the free functor fakes the lifting of a function by
recording both the function and its argument. It accumulates the lifted
functions by recording their composition. Functor rules are
automatically satisfied. This construction was used in a paper
\urlref{http://okmij.org/ftp/Haskell/extensible/more.pdf}{Freer Monads,
  More Extensible Effects}.

Alternatively, we can use the right Kan extension for the same purpose:

\src{snippet11}
It's easy to check that this is indeed a functor:

\src{snippet12}
