The Codensity Monad Transformer

In recent posts, we have encountered Kan extensions and the codensity monad, and explored some basic aspects of formal monad theory. This lead to a representation result, relating monad morphisms with domain a codensity monad, and monad actions. Todays post will continue those themes, yielding yet another approach to building and moving monads around.

Transferring Monads

We will work in terms of formal monad theory, in a 2-category $\mathcal{C}$ . This is primarily to show that very little structure is actually need for the result to go through, and will require no complicated background. Readers that want to keep things a bit more concrete can think of $\mathcal{C}$ as the 2-category of categories, functors and natural transformations.

If we have a monad $(\mathbb{T}, \eta, \mu)$ on some 0-cell $\mathcal{A}$ , and a 1-cell

$\mathcal{A} \xrightarrow{F} \mathcal{B}$ ,

the question we would like to solve can we transfer the monad $\mathbb{T}$ along $F$ , to give a monad on $\mathcal{B}$ ? Obviously this is a rather imprecise specification, lets explore some possibilities.

We could assume that the right extension of $F$ along itself exists:

$\mathsf{Ran}_F(F) : \mathcal{B} \rightarrow \mathcal{B}$ ,

and this will induce a codensity monad on $\mathcal{B}$ . This isn’t really in the spirit of the question though, as we have completely ignored the monad $\mathbb{T}$ in our construction. So we consider this approach to be unsatisfactory, as would be other trivial solutions, such as simply taking the identity monad on $\mathcal{B}$ .

To get the monad $\mathbb{T}$ into the game, we modify our previous plan, and consider the right extension of $F \circ \mathbb{T}$ along $F$ .

$\mathsf{Ran}_F(F \circ \mathbb{T}) : \mathcal{B} \rightarrow \mathcal{B}$ .

It turns out that this 1-cell carries a unique monad structure such that the universal 2-cell

$\mathsf{run} : \mathsf{Ran}_{F}(F \circ \mathbb{T}) \circ F \Rightarrow F \circ \mathbb{T}$

is an Eilenberg-Moore law. Our aim now is to use this extra criterion to deduce the required unit and multiplication.

The universal property of the required right extension can equivalently be written for all $\alpha H \circ F \Rightarrow F \circ \mathbb{T}$ and $\beta : H \Rightarrow \mathsf{Ran}_F(F \circ \mathbb{T})$ :

$\alpha = \mathsf{run} \cdot (\beta \circ F) \;\Leftrightarrow\; \hat{\alpha} = \beta$

This formulation is useful as the two axioms of an Eilenberg-Moore law require that a pair of equations must hold, and the equivalence allows us to deduce further equations. Defining $\mathbb{S} := \mathsf{Ran}_{F}(F \circ \mathbb{T})$ to simplify notation, we find that:

Plugging in the unit preservation axiom into the left hand side of the right extension universal property, the unit of the monad on $\mathcal{B}$ must be $\widehat{(F \circ \eta)} : \mathsf{Id} \Rightarrow \mathbb{S}$ .
Plugging in the multiplication preservation axiom into the left hand side of the right extension universal property, we find that the multiplication must be $\widehat{\mu \cdot (\mathsf{run} \circ \mathbb{S}) \cdot (\mathbb{S} \circ \mathsf{run})} : \mathbb{S} \circ \mathbb{S} \Rightarrow \mathbb{S}$ .

So there are unique choices of potential unit and multiplication for the resulting monad. It is then a routine calculation using the properties of extensions and the monad $\mathbb{T}$ to show that the monad axioms are satisfied.

So we have found a construction that given a monad on a 0-cell $\mathcal{A}$ , and a 1-cell $F : \mathcal{A} \rightarrow \mathcal{B}$ , such that the right extension $\mathsf{Ran}_F(F \circ \mathbb{T})$ exists, there is a canonical monad induced on $\mathcal{B}$ . We refer to this construction as the codensity monad transformer.

Example: If we take the monad $\mathbb{T}$ in this construction to be the identity monad, we recover ordinary codensity monad as a special case.

We saw a similar construction, building a new monad from a parameter monad and some additional data, in a an earlier post. There, given a monad $\mathbb{T}$ on $\mathcal{A}$ , and an adjunction $L \dashv R : \mathcal{A} \rightarrow \mathcal{B}$ , the composite $R \circ \mathbb{T} \circ L$ is a monad on $\mathcal{B}$ . This result is known as Huber’s construction.

Conclusion

This result is mentioned in Street’s “Formal Theory of Monads”, although not as a theorem in that paper. Presumably the result was well known before that, although I am currently unaware of an original source, and would welcome further information.

As we worked formally in terms of an arbitrary 2-category, we see that the codensity monad transformer does not hinge on anything specific to categories, functors and natural transformations, or specific right Kan extension constructions in terms of certain limits. From this perspective, once you are comfortable with it, the abstraction of working formally actually simplifies the analysis as it removes irrelevant structure and other distracting details.

Further reading: The calculations to verify this result might be somewhat intimidating to readers new to (or less comfortable with) Kan extensions, although they are in principle quite simple. I would recommend using the graphical notation introduced in my co-author Ralf Hinze’s paper “Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick”. This notation might take a little bit of getting used to, but once digested I find it takes a lot of the pain out of reasoning with Kan extensions.

Monad maps and Algebras Redux

In a previous post, we noted that for a $\mathsf{Set}$ monad $\mathbb{T}$ , and set $A$ , there is a bijective correspondence between:

Eilenberg-Moore algebras for the monad $\mathbb{T}$ with underlying set $A$ .
Monad morphisms of type $\mathbb{T} \rightarrow ((-) \Rightarrow A) \Rightarrow A$ with codomain the continuation monad induced by $A$ .

We also briefly remarked that this observation can be generalised beyond the category $\mathsf{Set}$ . In this post, using some of the ideas we have learned in recent posts, we are going to explore relationships of this type between algebras and morphisms of monads in more detail.

Enrichment

We previously encountered enriched monads. Recall that for a monoidal category $\mathcal{V}$ , a $\mathcal{V}$ -enriched category $\mathcal{C}$ has $\mathcal{C}(A,B)$ an object in $\mathcal{V}$ , rather than a mere set. We can also defined $\mathcal{V}$ -enriched functors and natural transformations which respect this structure.

Example: The category $\mathbf{Pre}$ has objects preorders, and morphisms monotone maps. This category has products, and so can be seen as a monoidal category with respect to this structure. A $\mathbf{Pre}$ -enriched category is a category in which:

The collection of morphisms of type $A \rightarrow B$ is a preorder.
Composition of morphisms is monotone in both arguments. That is $f_1 \leq f_2$ and $g_1 \leq g_2$ implies that $g_1 \circ f_1 \leq g_2 \circ f_2$ .

A $\mathbf{Pre}$ -functor a functor which is also monotone in its action on morphisms.

If a category $\mathcal{V}$ s monoidal closed, this category is itself a $\mathcal{V}$ -category, with hom object $\mathcal{V}(A,B)$ the exponential $A \multimap B$ . This is usually phrased as $\mathcal{V}$ being enriched over itself.

Example: The category $\mathbf{Pre}$ is Cartesian closed, and therefore is enriched over itself. The exponential $A \Rightarrow B$ in $\mathbf{Pre}$ is simply the collection of morphisms of that type, with the pointwise order on monotone functions.

If our base of enrichment $\mathcal{V}$ is symmetric monoidal closed, then for a $\mathcal{V}$ -category $\mathcal{C}$ we can define the opposite category $\mathcal{C}^{op}$ by setting $\mathcal{C}^{op}(A,B) = \mathcal{C}(B,A)$ , and defining the composition morphism of type

$\mathcal{C}^{op}(B,C) \otimes \mathcal{C}^{op}(A,B) \rightarrow \mathcal{C}^{op}(A,C)$

as the composite

$\mathcal{C}(C,B) \otimes \mathcal{C}(B,A) \xrightarrow{\sigma} \mathcal{C}(B,A) \otimes \mathcal{C}(C,B) \xrightarrow{m_{C,B,A}} \mathcal{C}(C,A)$

where $\sigma$ is the symmetry, and $m_{C,B,A}$ is the composition morphism in $\mathcal{C}$ .

With these technical preliminaries in place, for a symmetric monoidal category $\mathcal{V}$ , seen as enriched over itself, and $\mathcal{V}$ -object $A$ , there is a $\mathcal{V}$ -functor$:

$(-) \multimap A : \mathcal{V}^{op} \rightarrow \mathcal{V}$

As in the unenriched case, this functor is adjoint to itself, and so induces continuation or double dualisation $\mathcal{V}$ -enriched monad $((-) \multimap A) \multimap A$ . We then get a generalisation of the previous result, that for any other $\mathcal{V}$ -monad $\mathbb{T}$ , and $\mathcal{V}$ -object $A$ there is a bijective correspondence between:

Eilenberg-Moore algebras for the monad $\mathbb{T}$ , with underlying object $A$ .
Monad maps $\mathcal{T} \rightarrow ((-) \multimap A) \multimap A$ .

So the previous result generalises to enriched category theory. Note that the assumptions are unfortunately quite restrictive, as we can only consider monads on the base of enrichment itself. This is the enriched version of the fact the ordinary category theory result only applied to $\mathsf{Set}$ monads. This seems frustrating, so it is natural to ask if we can do any better.

Codensity and Formality

We previously encountered codensity monads. These were built using right Kan extensions. For a functor $F : \mathcal{A} \rightarrow \mathcal{B}$ , the codensity monad induced by $F$ has endofunctor $\mathsf{Ran}_F(F) : \mathcal{B} \rightarrow \mathcal{B}$ . We will write $\langle F,F \rangle$ for this codensity monad.

With any unfamiliar construction, it is natural to consider what it does in some simple cases. One obvious choice is to fix a set $A$ , and consider the codensity monad induced by the functor $A : 1 \rightarrow \mathsf{Set}$ that picks out that object. This will induce a monad on $\mathsf{Set}$ . Using some standard tools for calculating right Kan extensions in $\mathsf{Set}$ , we find something familiar. $\langle A,A \rangle$ is the continuation monad induced by $A$ .

We can therefore rephrase the original result that motivated our investigations as saying for monad $\mathbb{T}$ on $\mathsf{Set}$ , there is a bijective correspondence between:

Eilenberg-Moore algebras for $\mathbb{T}$ , with underlying set $A$ .
Monad morphisms $\mathbb{T} \rightarrow \langle A,A \rangle$ , with codomain the codensity monad induced by the functor $A : 1 \rightarrow \mathsf{Set}$ .

So far, we don’t have anything new, except a shift in viewpoint from emphasising the continuation monad, to a codensity based perspective. It is natural to then consider whether there is anything special about the category $\mathsf{Set}$ in this observation, and in fact there isn’t. So we can make a much stronger statement.

For a monad $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ and $\mathcal{C}$ -object $A$ , assuming the required right Kan extensions exist, there is a bijective correspondence between:

Eilenberg-Moore algebras for $\mathbb{T}$ , with underlying object $A$ .
Monad morphisms $\mathbb{T} \rightarrow \langle A,A \rangle$ , with codomain the codensity monad induced by the functor $A : 1 \rightarrow \mathcal{C}$ .

We can go further still, and ask if there’s anything special about the fact we’re doing category theory? Can we use the formal category theory perspective we’ve introduced in recent posts to get a more general result?

To do so, we must address a couple of wrinkles:

We need to abstract the notion of right Kan extension to an arbitrary 2-category. This is routine, we just require the same universal property, but now of abstract 0,1 and 2-cells, rather than categories, functors and natural transformations. The resulting structures are usually called a right extensions.
We have been making heavy use of the terminal category to pick out objects, via functors of the form $A : 1 \rightarrow \mathcal{C}$ . This may not make sense in an arbitrary 2-category.

To address the second point, we are looking to generalise from Eilenberg-Moore algebras built upon individual objects, to something more suitable in an arbitrary 2-category. We have already seen the required abstraction before, left monad actions, which solved a similar problem when we looked at Eilenberg-Moore objects.

Putting this all together, we get a much more general statement. Let $\mathcal{K}$ be a 2-category, and $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ a monad in $\mathcal{K}$ . For a 1-cell $A : \mathcal{B} \rightarrow \mathcal{C}$ , there is a bijective correspondence between:

Left $\mathbb{T}$ actions with underlying 1-cell $A$ .
Monad morphisms $\mathbb{T} \rightarrow \langle A,A \rangle$ with codomain the codensity monad induced by $A : \mathcal{B} \rightarrow \mathcal{C}$ .

So we learn that the previous result only hinged on the universal property of extensions, and nothing specific to category theory. The previous result about enriched monads arises as a special case in the 2-category of $\mathcal{V}$ -categories.

Conclusion

We’ve explored a classic result that often crops up in many guises in the literature. By exploiting our new tools of codensity monads, formal category theory, and left monad actions, we abstracted away a lot of distracting clutter, and reached a clearer understanding of what was really making this bijection work.

Further reading: This post was motivated by some discussions in the excellent “A 2-Categories Companion” by Lack, which is well worth reading. The material about enriched dual dualisation monads is almost exclusively contained in Kock’s “On Double Dualization Monads”. Readers wanting more than the details we briefly sketched will find a thorough and very readable account in that paper.

Codensity Monads and Kan Extensions

In this post, we are going to look at another method of constructing monads. The details are possibly more mathematically complex that those we have discussed so far, hinging on the topic of Kan extensions. We will study this construction at a fairly high level of abstraction, aiming to highlight the wide applicability of the techniques involved.

Kan Extensions

Given a category $\mathcal{D}$ , with a subcategory $\mathcal{C}$ , and a functor $G : \mathcal{C} \rightarrow \mathcal{E}$ , it is natural to ask if there is some systematic way to extend $G$ to the whole of $\mathcal{D}$ , yielding a functor $G' : \mathcal{D} \rightarrow \mathcal{E}$ ? Of course, when we look for “systematic” or “canonical” ways of doing things in category theory, we are looking for a construction with a universal property.

Although a natural motivation, the restriction to subcategories is unnecessary. Instead, for any functor $J : \mathcal{C} \rightarrow \mathcal{D}$ , and functor $G : \mathcal{C} \rightarrow \mathcal{E}$ , we are looking for a way to extend $G$ “along $J$ ” to construct a functor of type $\mathcal{D} \rightarrow \mathcal{E}$ .

It turns out, there is not one, but two mathematically natural choices, with universal properties given by the following isomorphisms, natural in $F$ :

$\mathsf{Lan}_J(G)\Rightarrow F \quad\cong\quad G \Rightarrow F \circ J$ .
$F \circ J \Rightarrow G \quad\cong\quad F \Rightarrow \mathsf{Ran}_J(G)$ .

$\mathsf{Lan}_J(G)$ and $\mathsf{Ran}_J(G)$ are respectively known as the left and right Kan extensions of $G$ along $J$ . Note that this terminology can be reversed in some parts of the literature, so it is always wise to check which universal property is being assumed. Kan extensions arise all over category theory and mathematics, for example in connection to adjunctions, (co)limits and monads, leading to MacLane’s claim “All concepts are Kan extensions”.

If these extensions exist for all $G$ , we have adjunctions involving precomposition with $J$ :

$\mathsf{Lan}_J(-) \dashv (-) \circ J \qquad\text{ and }\qquad (-) \circ J \dashv \mathsf{Ran}_J(-)$

So left Kan extensions then conveniently yield left adjoints and dually on the right, making the naming convention somewhat logical.

We can rephrase the universal properties for Kan extensions as follows:

For $\mathsf{Lan}_J(G)$ there exists a universal natural transformation $\mathsf{run} : G \Rightarrow \mathsf{Lan}_J(G) \circ J \Rightarrow G$ such that for every $\alpha : G \Rightarrow F \circ J$ there exists a unique $\hat{\alpha} : \mathsf{Lan}_J{G} \Rightarrow F$ such that $\alpha = (\hat{\alpha} \circ J) \cdot \mathsf{run}$ .
For $\mathsf{Ran}_J(G)$ there exists a universal natural transformation $\mathsf{run} : \mathsf{Ran}_J(G) \circ J \Rightarrow G$ such that for every $\alpha : F \circ J \Rightarrow G$ there exists a unique $\hat{\alpha} : F \Rightarrow \mathsf{Ran}_J(G)$ such that $\alpha = \mathsf{run} \cdot (\hat{\alpha} \circ J)$ .

So far, we have no insight into whether we can form left and right Kan extensions. Fortunately, there is some good news on this front, if $\mathcal{C}$ is a small category (has a set of objects):

If $\mathcal{E}$ is cocomplete, then $\mathsf{Lan}_J(G)$ exists for all $G$ .
If $\mathcal{E}$ is complete, then $\mathsf{Ran}_J(G)$ exists for all $G$ .

Under these conditions, there are explicit formulae for the Kan extensions in terms of the assumed (co)limits. These constructions are important, but we omit the details as we shall not need them in this post.

Example: It is common to consider functors between presheaf categories

$[\mathcal{D}^{op},\mathsf{Set}] \rightarrow [\mathcal{C}^{op},\mathsf{Set}]$

induced by precomposing with a functor $J : \mathcal{C} \rightarrow \mathcal{D}$ . By the result above, as $\mathsf{Set}$ is both complete and cocomplete, such functors always have both left and right adjoints, given by the two Kan extensions.

We note that in this way, every such $J$ induces both a monad and a comonad on $[\mathcal{D}^{op}, \mathsf{Set}]$ . These monads are not our main focus for today though.

There is another useful condition for the existence of certain Kan extensions in the presence of an adjunction. Assume $L \dashv R$ with unit and counit $\eta : \mathsf{Id} \Rightarrow R \circ L$ and $\epsilon : L \circ R \Rightarrow \mathsf{Id}$ . Then:

$\mathsf{Lan}_R(\mathsf{Id}) = L$ .
$\mathsf{Ran}_L(\mathsf{Id}) = R$ .

We also have that adjoints preserve Kan extensions in the following sense:

$L \circ \mathsf{Lan}_J(G) = \mathsf{Lan}(L \circ G)$ .
$R \circ \mathsf{Ran}_J(G) = \mathsf{Ran}(R \circ G)$ .

Kan Lifts

As an aside, we briefly mention there is a related concept of Kan lifts. These answer the question for functors $J : \mathcal{C} \rightarrow \mathcal{D}$ , and $G : \mathcal{D} \rightarrow \mathcal{E}$ of when we can “lift” $G$ to a functor $G' : \mathcal{C} \rightarrow \mathcal{E}$ . Notice the difference in direction of travel along $J$ versus Kan extensions. Again there are two possible answers, with universal properties given by natural bijections:

$\mathsf{Lift}_J(G) \Rightarrow F \quad\cong\quad G \Rightarrow J \circ F$ .
$J \circ F \Rightarrow G \quad\cong\quad F \Rightarrow \mathsf{Rift}_J(G)$ .

$\mathsf{Lift}_J(G)$ and $\mathsf{Rift}_J(G)$ are respectively the left and right Kan lifts of $G$ along $J$ . Again, if these exist for all $G$ , we have adjunctions, now involving post composition with $J$ :

$\mathsf{Lift}_J(-) \dashv J \circ (-) \qquad\text{and}\qquad J \circ (-) \dashv \mathsf{Rift}_J(-)$

One should be careful that not all the theory transfers as smoothly to lifts as it is for extensions. For example, I am not aware of an explicit construction in terms of (co)limits, or a construction similar to that we see in the next section.

Codensity Monads

For any functor

$J : \mathcal{C} \rightarrow \mathcal{D}$

we can consider the right Kan extension:

$\mathsf{Ran}_J(J) : \mathcal{D} \rightarrow \mathcal{D}$

of $J$ along itself. Assuming this exists, we have natural transformations:

$\widehat{\mathsf{id}_{\mathsf{Ran}_J(J)}} : \mathsf{Id}_{\mathcal{D}} \Rightarrow \mathsf{Ran}_J(J)$ .

and

$\widehat{ \mathsf{run} \cdot (\mathsf{Ran}_J(J) \circ \mathsf{run}) }: \mathsf{Ran}_J(J) \circ \mathsf{Ran}_J(J) \Rightarrow \mathsf{Ran}_J(J)$

(The hat should cover the whole term above, but we are reaching the limits of the latex formatting technology at our disposal).

So we have an endofunctor $\mathsf{Ran}_J(J)$ and two natural transformations with the right types to serve as a unit and multiplication for a monad. It turns out that this construction does in fact yield a monad.

If $\mathcal{D}$ is a complete category, and $\mathcal{C}$ is small, the required Kan extension always exists, so we can use this as another method to generate monads. We may return to this point in a future point, and consider concrete examples. Our aim for today is to understand exactly which monads can be constructed in this way.

Consider a monad $\mathbb{T}$ . Via the Eilenberg-Moore construction, this always arises from an adjunction $L \dashv R$ . From this, we know from the observations about Kan extensions and adjunctions above that:

$\mathsf{Ran}_L(\mathsf{Id}) = R$

and furthermore

$\mathsf{Ran}_R(R) = R \circ \mathsf{Ran}_L(\mathsf{Id}) = R \circ L = \mathbb{T}$

Therefore the endofunctor part of the monad always arises as the Kan extension of the right adjoint along itself. In fact, if we’re a bit more careful about tracking the unit and multiplication, we find that up to isomorphism, every monad arises as a codensity monad via this construction. Everything about this argument dualises smoothly, so every comonad arises as a density comonad, giving us another handle on the apparently wilder world of comonads.

Remark: Sometime you will see a claim that “this is a codensity monad”. Given that every monad is, what is normally meant by such a statement? I would normally interpret this as being about the concrete description of the monad. The Right Kan extension can be expressed as a limit, and often in a particular category a specific construction of limits is considered standard, pointing to a concrete representation of interest.

Conclusion

We have rather quickly run through some of the high-level theory of Kan extensions and codensity monads. There is a lot more to say here, particularly in terms of how specific monads arise from the codensity construction applied to mathematically natural choices of functors which aren’t merely resolutions of the chosen monad. We may return to concrete examples in later posts.

Further reading: For Kan extensions and related theory, and many other things, I would recommended “(Co)end Calculus” by Fosco Loregian. I would certainly suggest reading about the novel string diagrammatic approach to Kan extensions in “Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick” by my co-author Ralf Hinze. For intriguing examples of the codensity construction, “Codensity and the Ultrafilter Monad” by Leinster is a fascinating read.