enriched category theory

Distributive Laws and Tensor Products of Enriched Categories

Distributive laws are a fundamental concept in monad theory. They allow us to form well-behaved composite monads, lift monads to Kleisli and Eilenberg-Moore categories, and play key roles in various computer science applications.

As with any worthwhile mathematical object, it is useful to have multiple perspectives to clarify the underlying idea. This post aims to show how we might rediscover the notion of distributive from an enriched category theory point of view.

Monads and Enrichment

For a monoidal category $(\mathcal{V}, \otimes, I)$ , we can:

Define $\mathcal{V}$ -enriched categories, more concisely referred to as $\mathcal{V}$ -categories.
Define $\mathcal{V}$ -functors between $\mathcal{V}$ -categories.
If $\mathcal{V}$ is a symmetric monoidal category, we can define a tensor product of $\mathcal{V}$ -categories $\mathcal{C}$ and $\mathcal{D}$ , denoted $\mathcal{C} \otimes \mathcal{D}$ , generalising product categories from ordinary category theory.

We considered monads from an enriched point of view in a previous post. For our current discussion, we slightly vary the emphasis, and consider monads on a fixed category $\mathcal{C}$ (or more generally object in a 2-category). We enrich over the endofunctor category $[\mathcal{C},\mathcal{C}]$ with functor composition as the monoidal structure.

In this setting:

A monad $(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \eta, \mu)$ is a one object $[\mathcal{C}, \mathcal{C}]$ -category, which we shall denote $\mathbb{T}$ . The unit and multiplication of the monad encode the identities and composition of the category, and the monad axioms ensure they behave as expected.
A monad map is the same things as a $[\mathcal{C}, \mathcal{C}]$ -functor, encoding the functor action on the hom object, with the monad map axioms enforcing preservation of identities and commuting with composition.
The monoidal category $([\mathcal{C}, \mathcal{C}], \otimes, \mathsf{Id})$ is clearly not symmetric. How do we get an analog of the tensor product of enriched categories?

The tensor product of $\mathcal{V}$ categories has objects pairs of objects from the components categories, and hom objects given by the tensor product of the component homs:

(\mathcal{C} \otimes \mathcal{D})((c_1, d_1), (c_2, d_2)) = \mathcal{C}(c_1,c_2) \otimes \mathcal{D}(d_1,d_2)

In order to define the composition maps

(\mathcal{C} \otimes \mathcal{D})((c_2,d_2),(c_3, d_3)) \otimes (\mathcal{C} \otimes \mathcal{D})((c_1,d_1),(c_2,d_2)) \rightarrow (\mathcal{C} \otimes \mathcal{D})((c_1,d_1),(c_3,d_3))

from the composition maps in the component categories, we need the assumption $\mathcal{V}$ is symmetric to allow us to wire things up in the right order.

Now if we consider our case of interest, monads

(\mathbb{S}, \eta, \mu) \quad\text{and}\quad(\mathbb{T},\eta,\mu)

viewed as one-object $[\mathcal{C}, \mathcal{C}]$ -categories, if we could form the tensor product of these categories,

\mathbb{T} \otimes \mathbb{S}

it would have a single hom object

\mathbb{T} \circ \mathbb{S}

As we have no symmetry, we need to figure out how to form a composition map

\mathbb{T} \circ \mathbb{S} \circ \mathbb{T} \circ \mathbb{S} \Rightarrow \mathbb{T} \circ \mathbb{S}

using the composition maps (monad multiplications) in the component categories. Following the standard tensor product construction, we need a natural transformation

\lambda : \mathbb{S} \circ \mathbb{T} \Rightarrow \mathbb{T} \circ \mathbb{S}

to swap the middle two components of the domain as follows:

\mathbb{T} \circ \mathbb{S} \circ \mathbb{T} \circ \mathbb{S} \xRightarrow{\mathbb{T} \circ \lambda \circ \mathbb{S}} \mathbb{T} \circ \mathbb{T} \circ \mathbb{S} \circ \mathbb{S}

Not any old natural transformation will do, in order to prove the resulting composition map is unital and associative, we will need some equational axioms. In fact, what we need is a distributive law!

Summary

This post stems from a simple line of reasoning:

Monads are special enriched categories
There are standard ways of composing monads and composing enriched categories, are these also related?

I would be very interested to understand if there is a well-known construction on enriched categories of which the perspective on distributive laws above is a special case?

A Pseudomonad is …

The aim of this post is to generalise the notion of monad to incorporate new examples, by weakening the requirement for the usual monad equations to hold exactly to instead be up to isomorphism. The resulting object is known as a pseudomonad. As we have seen several different perspectives on the notion of monad, all of which we will adapt to this new, more flexible setting. The aim is to give a high level overview of the key structures and the relationships between them, whilst skimming over some technical details.

Weakening the notion of monad

The most general definition of monad we have discussed is as a structure in a (strict) 2-category, consisting of:

An object $\mathcal{C}$
A 1-cell $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$
A unit 2-cell $\mathsf{Id} \Rightarrow \mathbb{T}$
A multiplication 2-cell $\mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T}$

such that the unit and multiplication satisfy three equations.

In fact, we generalised this definition to the weaker setting of bicategories, but this was not strictly necessary. As every bicategory is biequivalent to a 2-category, we got “nothing new” by doing so. Of course, if the natural setting of your work is a bicategory, you may beg to differ, at least from the point of view of convenience.

Our aim is to weaken the definition above, so that the three equations defining a monad are only required to hold up to isomorphism. To do so, we require a notion of morphisms between 2-cells. That is, we need 3-cells, which points us in the direction of tricategories. This is a recurring theme, to weaken a definition we need to go up a dimension to provide the room to express the weakness.

Roughly speaking, we can arrive at the notion of tricategory by starting with categories enriched in 2-categories, and then weakening all the equations to coherent isomorphisms. That all sounds a bit scary, so it would be nice to restrict to strict 3-categories, by analogy with the simplifying step from bicategories to 2-categories. Unfortunately, this plan is flawed, as it is not the case that every tricategory is triequivalent to a strict 3-category. Annoying…

Fortunately all is not lost. Every tricategory is triequivalent to what is known as a Gray-category. A Gray-category is a tricategory in which composition is unital and associative on the nose, but interchange only holds up to isomorphism. They can also be seen as categories enriched over a suitable monoidal category $\mathbf{Gray}$ . This allows us to work in a relatively simple setting, without throwing anything fundamental away.

In a Gray category, a pseudomonad consists of the data described above for a monad, along with three invertible 3-cells:

\mathsf{id} \Rrightarrow \mu \cdot \mathbb{T} \circ \eta \qquad \mathsf{id} \Rrightarrow \mu \cdot \eta \circ \mathbb{T} \qquad \mu \cdot \mathbb{T} \circ \mu \Rrightarrow \mu \cdot \mu \circ \mathbb{T}

satisfying two coherence equations.

The Monoid Perspective

We have already encountered the standard monad meme:

A monad is a monoid in the category of endofunctors.

We would hope to get a statement of a similar form for pseudomonads. Mostly this will be an exercise in terminology.

A Gray-monoid is a one-object Gray-category. This is a variation of the notion of monoidal category, and so it seems natural to refer to a pseudomonad in a Gray-monoid as a pseudomonoid. As we can always restrict to the one-object sub-Gray-category induced by the 0-cell our pseudomonad is defined upon, simply by definition we arrive at

A pseudomonad is a pseudomonoid in the Gray-monoid of endo 1-cells.

We did not really do anything here apart from introduce new names for things we have already encountered, but the notion of pseudomonoid provides a different emphasis. As Gray-categories were a simplifying device, we can inevitably extend the definition to one-object tricategories, or equivalently to monoidal bicategories. An alternative motivation for pseudomonoids is the following:

Example: In the monoidal bicategory of categories, functors and natural transformations, with products as the monoidal structure, a pseudomonoid is the same thing as a monoidal category.

We can also pick out more exotic gadgets.

Example: In the monoidal bicategory of monoidal categories, lax monoidal functors and monoidal natural transformations, with products as the monoidal structure, a pseudomonoid is the same thing as a duoidal category.

It is then natural to search for variations of pseudomonoids, living in corresponding variations of monoidal bicategories, corresponding to other types of monoidal categories, such as with braiding or symmetries.

The Functorial Semantics Perspective

We can form what is known as the simplicial category $\Delta$ , with:

Objects: Finite ordinals
Morphisms: Order preserving functions

This category is a strict monoidal category with respect to ordinal sums. Every strict monoidal category can be seen as a 1-object monoidal category, referred to as its suspension. This 2-category can be thought of as the generic monad. We then have an observation of Lawvere that:

A monad is a strict 2-functor from the suspension of the ordinal category.

Or possibly more clearly:

A monad is a strict 2-functor from the generic monad.

These 2-functors stamp out copies of the generic monad in their codomain 2-categories.

It would be nice if we could capture pseudomonads in a similar manner. This is indeed the case, as shown by Lack, using a construction adapting the simplicial category construction to yield a Gray-monoid, with a suspension we might describe as the generic pseudomonad, such that:

A pseudomonad is a Gray-functor from the generic pseudomonad.

Here, Gray-functors are the usual notion from enriched category theory.

The Enriched Perspective

We have seen:

A monad is a one-object enriched category.

This gave yet another perspective on the notion of monad. Can we get something similar for pseudomonads?

Recall that a strict 2-category is a category enriched in the monoidal category of categories and functors, with products as the monoidal structure. We cannot conveniently describe bicategories in the same way, as we need to weaken certain equalities to isomorphisms. This sounds reminiscent of the situation above where we wanted to weaken the notion of monad. Again, in order to incorporate the additional weakness we need to go up a dimension, and enrich in the monoidal bicategory of categories, functors and natural transformations, with products again as the monoidal structure. Of course we cannot use the ordinary notion of enriched category, but there is a notion of a category weakly enriched in a monoidal bicategory or tricategory $\mathcal{V}$ , in which associativity and unitality hold up to specified coherent invertible 3-cells. These structures are referred to as $\mathcal{V}$ -bicategories, as the motivating $\mathsf{Cat}$ -bicategories are the usual notion of bicategory.

With this little detour out of the way, the coherence properties of $\mathcal{V}$ -bicategories and pseudomonads coincide, in that:

A pseudomonad is the same thing as a one object $\mathcal{V}$ -bicategory.

Summary

We have seen several different perspectives on the notion of pseudomonad which pleasingly parallel ideas for ordinary monads. This involved incorporating some possibly intimidating weaker higher-dimensional structures. As the developments for monads and pseudomonads run parallel, hopefully this helps transfer intuitions to the more complex setting.

Some references that I found useful:

Pseudomonads – “Distributive Laws for Pseudomonads” by Marmolejo, along with other work of the same author.
The functorial semantics perspective – “A Coherent Approach to Pseudomonads” by Lack.
My source for weak enrichment was “Enriched Categories as a Free Cocompletion” by Garner and Shulman.

The NLab was very useful for background on pseudomonoids.

Remark: This post developed out of background reading for some ongoing work, and so is slightly outside my useful comfort zone. I welcome comments and feedback to improve the presentation and intuitions, or correct errors.

A monad is just a one object enriched category

We have seen that the notion of monad can be interpreted in any bicategory. The aim of todays post is to explain that for a bicategory $\mathcal{W}$ , a monad in $\mathcal{W}$ is the same thing as a one-object $\mathcal{W}$ -enriched category. Or more tersely:

A monad is the same thing as a one-object $\mathcal{W}$ -category.

Mostly, this is just a case of understanding the definitions, with no complicated translation between the two structures required.

Monads and enrichment

Recall that for a monoidal category $(\mathcal{V}, \otimes, I)$ , a $\mathcal{V}$ –enriched category, or $\mathcal{V}$ -category $\mathcal{A}$ is a generalisation of ordinary categories with:

A collection of objects $X,Y,\ldots$ .
For every pair of object $X,Y$ , a hom object $\mathcal{A}(X,Y)$ .
For each object $X$ , an identity $\mathcal{V}$ -morphism $j_X : I \rightarrow \mathcal{A}(X,X)$ .
For each triple of objects $X,Y,Z$ , a composition $\mathcal{V}$ -morphism $m_{X,Y,Z} : \mathcal{A}(Y,Z) \otimes \mathcal{A}(X,Y) \rightarrow \mathcal{A}(X,Z)$ .

These are subject to some natural axioms such that composition is associative, and unital with respect to the chosen identities. The motivating special case is that a $\mathsf{Set}$ -enriched category is the same thing as an ordinary category.

It is a well-known fact of enriched category theory that a monoid in the monoidal category $\mathcal{V}$ is the same thing as a one object $\mathcal{V}$ -category. The even better known special case, which crops up in most introductions to category theory, is that a one object ordinary category is the same thing as a monoid.

Of course, the special case that we should be interested in as monad theorists is the monoidal category of endofunctors $([\mathcal{C}, \mathcal{C}], \circ, \mathsf{Id}_{\mathcal{C}})$ . Using the fundamental meme of monad theory, that a monad is just a monoid in the category of endofunctors, we can deduce that monads on $\mathcal{C}$ are the same thing as one object $[\mathcal{C},\mathcal{C}]$ -enriched categories. This claim works equally well if we consider monads in an arbitrary bicategory.

Example: We have seen previously that for a monoidal category $\mathcal{V}$ with coproducts, a $\mathcal{V}$ -enriched category is the same thing as a monad in the bicategory of $\mathcal{V}$ -matrices, $\mathbf{Mat}(\mathcal{V})$ . Applying the observation above, the following all describe the same data:

A $\mathcal{V}$ -enriched category with set of objects $O$ .
A monad on $O$ in $\mathbf{Mat}(\mathcal{V})$ .
A one-object $\mathbf{Mat}(\mathcal{V})(O,O)$ -enriched category.

Which is a bit of a funny conclusion, every multi-object enriched category is the same thing as a single-object enriched category over a different base. In particular, every ordinary (small) category with set of objects $O$ is a one-object $\mathbf{Mat}(\mathsf{Set})(O,O)$ -enriched category.

In the example above, it feels a bit clumsy to have to keep saying “…with set of objects $O$ …”. To clean this up, and take this story a bit further, we are going to have to generalise our notion of enriched category, to categories enriched over a bicategory $\mathcal{W}$ . Although this may sound a bit intimidating, it is actually only a small step beyond enrichment in a monoidal category.

A $\mathcal{W}$ -enriched category $\mathcal{A}$ consists of:

A collection of objects $X,Y,Z$ , each with an associated extent, given by a 0-cell $\mathsf{ext}(X)$ in $\mathcal{W}$ .
For every pair of objects $X,Y$ , a hom 1-cell $\mathcal{A}(X,Y) : \mathsf{ext}(X) \rightarrow \mathsf{ext}(Y)$ .
For every object $X$ , an identity 2-cell $j_A : \mathsf{Id}_{\mathsf{ext}(X)} \Rightarrow \mathcal{A}(X,X)$ .
For every triple of objects $X,Y,Z$ , a composition 2-cell $m_{X,Y,Z} : \mathcal{A}(Y,Z) \circ \mathcal{A}(X,Y) \Rightarrow \mathcal{A}(X,Z)$ .

As before, this data is subject to natural unitality and associativity axioms.

With this definition in place, naming things suggestively, a one object $\mathcal{W}$ -category consists of:

An object, with extent a 0-cell $\mathcal{C}$ in $\mathcal{W}$ .
A single hom 1-cell $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ .
An identity 2-cell $\eta : \mathsf{Id} \Rightarrow \mathbb{T}$ .
A single composition 2-cell $\mu : \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T}$ .

This data satisfies exactly the axioms such that $(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \eta, \mu)$ is a monad. That is:

A monad in $\mathcal{W}$ is the same thing as a one-object $\mathcal{W}$ -category.

We rephrase the previous example in this more flexible setting.

Example: For a monoidal category $\mathcal{V}$ , a $\mathcal{V}$ -category is a one object $\mathbf{Mat}(\mathcal{V})$ -enriched category.

A possibly more interesting example is as follows.

Example: We have seen previously that for a category $\mathcal{C}$ with pullbacks, an internal category in $\mathcal{C}$ is the same thing as a monad in the bicategory of spans $\mathbf{Span}(\mathcal{C})$ . Now applying our previous observation, the following all describe the same data:

An internal category in $\mathcal{C}$ .
A monad in $\mathbf{Span}(\mathcal{C})$ .
A one-object $\mathbf{Span}(\mathcal{C})$ -enriched category.

This establishes a slightly surprising connection between internal and enriched category theory.

Conclusion

To an extent, this post is about almost trivial relationships between definitions that happen to coincide. This is not just an exercise in categorical showing-off or pointless abstraction. The relationship between monads and one-object enriched categories is really a matter of perspective. This may allow us to relate monads to other concepts, for example finitary monads and Lawvere theories can be connected in this way. Once monads are viewed as categories, we can consider categorical notions such as completion under certain limits or colimits, which again occur in connection with Lawvere theories. These ideas are used to startling effect in the work of Richard Garner and co-authors, which I highly recommend as further reading.

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.

Bicategories, monoids, internal and enriched categories

Last time, we introduced a more general definition of monads, in the setting of (strict) 2-categories. Unfortunately this strictness is often a bit too rigid to incorporate natural mathematical objects, and this is certainly true for monad theory. This time, we will push our definition of monads beyond this strict setting, into the wider world of bicategories.

Generalising to Bicategories

A bicategory $\mathbf{C}$ consists of:

A collection of 0-cells $A,B,\ldots$
Between every pair of 0-cells $A,B$ , a category $\mathbf{C}(A,B)$ . The objects of these categories are termed 1-cells, and the morphisms 2-cells. Composition of 2-cells is called vertical composition.
For every triple of 0-cells, $A,B,C$ a bifunctor $\circ : \mathbf{C}(B,C) \times \mathbf{C}(A,B) \rightarrow \mathbf{C}(A,B)$ , referred to as horizontal composition. For every 0-cell $A$ , there are identity 1-cells $\mathsf{Id}_A$ in $\mathbf{C}(A,A)$ .

Horizontal composition is associative and unital up to isomorphism. That is, there are natural isomorphisms:

A left unitor $\lambda : \mathsf{Id} \circ (-) \Rightarrow (-)$ .
A right unitor $\rho : (-) \circ \mathsf{Id} \Rightarrow (-)$ .
An associator $\alpha : (-) \circ ((-) \circ (-)) \Rightarrow ((-) \circ (-)) \circ (-)$ , between the two different orders in which we can apply horizontal composition twice.

As you might expect, this structure is subject to some coherence equations, entirely analogous to those for a monoidal category.

Example: A (strict) 2-category is a bicategory in which the unitors and associators are identities, so horizontal composition is unital and associative on the nose.

Example: A monoidal category is “the same thing” as a bicategory with one 0-cell. This is often phrased as “A monoidal category is a one object bicategory”.

Considering one direction in more detail, in a bicategory $\mathbf{C}$ with one 1-cell $A$ consists of a single category $\mathbf{C}(A,A)$ . We also have:

A horizontal composition bifunctor $\mathbf{C}(A,A) \times \mathbf{C}(A,A) \rightarrow \mathbf{C}(A,A)$ . We consider this to be the tensor product of our monoidal category.
The identity 1-cell $\mathsf{Id}_A$ will serve as the monoidal unit.

The coherence axioms for a bicategory is this simple case are exactly those of a monoidal category. Going in the other direction is similar.

We also introduce a couple of more complex bicategories that will be important in subsequent examples.

Example: A span of type $X \rightarrow Y$ in a category $\mathcal{C}$ is a pair of $\mathcal{C}$ -morphisms of the form:

$X \xleftarrow{f} A \xrightarrow{g} Y$ .

If $\mathcal{C}$ has pullbacks, we can form the composite of a span $X \xleftarrow{f} A \xrightarrow{g} Y$ with a span $Y \xleftarrow{h} B \xrightarrow{k} Z$ as:

$X \xleftarrow{f \circ \pi_1} A \times_{Y} B \xrightarrow{g \circ \pi_2} Z$

where $\pi_1, \pi_2$ are the two projection maps given by forming the pullback of $g$ along $h$ .

Given two spans $X \xleftarrow{f_1} A_1 \xrightarrow{g_1} Y$ and $X \xleftarrow{f_2} A_2 \xrightarrow{g_2} Y$ a morphism of spans between them is a $\mathcal{C}$ -morphism $h : A_1 \rightarrow A_2$ such that:

$f_2 \circ h = f_1 \quad\text{and}\quad g_2 \circ h = g_1$

In fact, for a category $\mathcal{C}$ with pullbacks, there is a bicategory $\mathbf{Span}(\mathcal{C})$ with:

0-cells the objects of $\mathcal{C}$ .
$\mathbf{Span}(\mathcal{C})(X,Y)$ consists of all spans of type $X \rightarrow Y$ , and span morphisms between them.
The universal property of pullbacks means composition of spans extends to a bifunctor, which we take to be our horizontal composition.

We are skimming over a size issue here. Readers with the necessary background may want to consider how such questions might creep in to the definition above.

Example: Let $\mathcal{V}$ be a monoidal category with coproducts. For sets $A,B$ , we can consider $\mathcal{V}$ -valued matrices of type $A \rightarrow B$ to be functions:

$M : A \times B \rightarrow \mathsf{obj}(\mathcal{V})$

Given a pair of matrices $M : A \rightarrow B$ and $N : B \rightarrow C$ , we can form their composite as follows:

$(N \circ M)(a,c) = \coprod_{b \in B} M(a,b) \otimes N(b,c)$

Given a pair of matrices $M_1, M_2 : A \rightarrow B$ , a morphism of matrices is a family of $\mathcal{V}$ morphisms:

$f_{a,b} : M_1(a,b) \rightarrow M_2(a,b)$

This data can be combined into a bicategory $\mathbf{Mat}(\mathcal{V})$ with:

0-cells sets.
The category $\mathbf{Mat}(\mathcal{V})(A,B)$ consists of matrices of type $A \rightarrow B$ and morphisms between then.
Horizontal composition is given by composition of matrices, as described above.

The two previous examples are typical for bicategories, in that horizontal composition involves either limits or colimits. In such cases, if we form iterated horizontal composites in different orders, the universal properties involved will ensure they agree up to isomorphism. Insisting that composites formed in different orders agree on the nose would lead to unrealistic requirements on our choice of (co)limits, so the bicategorical rather than strict 2-categorical setting is more natural.

Now we’ve seen a few different bicategories, it’s time to get back to our main motivation, monads. A monad in a bicategory $\mathbf{C}$ consists of:

A 0-cell $\mathcal{C}$ .
A 1-cell $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ .
A unit 2-cell $\eta: \mathsf{Id}_{\mathcal{C}} \Rightarrow \mathbb{T}$ .
A multiplication 2-cell $\mu: \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T}$ .

As before, our notation is suggestive of that for “ordinary” monads on categories. Notice the data above is no different to that which we encountered in the strict 2-categorical setting. Things get more interesting when we consider the coherence equations that need to hold, as now we must account for the fact that horizontal composition is not unital or associative on the nose, but only up to isomorphism. The required equations are:

$\mu \cdot (\eta \circ \mathsf{id}_{\mathbb{T}}) = \lambda$ .
$\mu \cdot (\mathsf{id}_{\mathbb{T}} \circ \eta) = \rho$ .
$\mu \cdot (\mu \circ \mathsf{id}_{\mathbb{T}}) = \mu \cdot (\mathsf{id}_{\mathbb{T}} \circ \mu) \cdot \alpha$ .

Firstly, we see that this really does generalise our previous definition.

Example: As we would expect, a monad in a 2-category is a special case of a monad in a bicategory. The unitors and associators are identities, and the equations above collapse to those of the 2-categorical case.

We also find a fun simple source of monads that would not have made sense before:

Example: We can view any monoidal category $\mathcal{V}$ as a one object bicategory. A monoid in $\mathcal{V}$ is the same thing as a monad in this one object bicategory. For example, every group or monoid can be seen as a monad. There is a certain symmetry here:

In a bicategory $\mathbf{C}$ , every monad on $\mathcal{A}$ is a monoid in the monoidal category $\mathbf{C}(\mathcal{A},\mathcal{A})$ .
A monoid in a monoidal category is a monad in the corresponding one object bicategory.

We now move on to some more interesting examples, which really highlight the benefits afforded by the more liberal bicategorical definition.

Example: A (small) category consists of a set of objects $O$ and a set of morphisms $M$ . There are two functions giving the source and target of a given morphism, forming a span:

$O \xleftarrow{s} M \xrightarrow{t} O$

The identities induce a morphism from the identity span to this span. If we form the pullback of $s$ along $t$ , the object $M \times_O M$ consists of all composable pairs of morphisms, and there is a span morphism from the resulting span to the one defined above, given by the function maps composable pairs to their composite.

Given a category $\mathcal{C}$ with pullbacks, we can define an internal category in $\mathcal{C}$ to consists of the analogous structure. A (small) category is then an internal category in $\mathsf{Set}$ .

The key observation for our purposes is that an internal category in $\mathcal{C}$ is the same thing as a monad in $\mathbf{Span}(\mathcal{C})$ . The monad unit and multiplication correspond to the identities and composition respectively. The rest is “just” an exercise in unravelling definitions.

Example: For a monoidal category $\mathcal{V}$ with coproducts, a $\mathcal{V}$ -enriched category $\mathcal{A}$ consists of:

A set of objects $O$ .
For each pair of objects $o_1, o_2$ a hom-object in $\mathcal{V}$ . We can view this as a $\mathcal{V}$ -valued matrix $A : O \rightarrow O$ .
Morphisms $j_o : \mathcal{I} \rightarrow A(o,o)$ picking out the identities. These form a morphism of matrices from the identity matrix to $A$ .
Composition morphisms $m_{o_1, o_2, o_3} : A(o_2,o_3) \otimes A(o_1,o_2) \rightarrow A(o_1, o_3)$ , which via the universal property of coproducts induce a morphism $\coprod_{o_2 \in O} A(o_1, o_2) \otimes A(o_2, o_3) \rightarrow A(o_1,o_3)$ . Together, these form a morphism of matrices of type $A \circ A \rightarrow A$ .

A more careful unpacking of the definitions following these intuitions shows that a $\mathcal{V}$ -category is the same thing as a monad in $\mathbf{Mat}(\mathcal{V})$ .

As a special case of this construction, the Booleans can be considered as a thin two object monoidal category $\mathcal{B}$ . The category $\mathbf{Mat}(\mathcal{B})$ is equivalent to the bicategory of relations $\mathbf{Rel}$ we encountered last time. The Boolean enriched categories are then exactly preorders.

Conclusion

By considering a further generalisation of the notion of monad to the weak setting of bicategories, many new interesting examples become possible. The examples of internal and enriched categories are well-known, and provide the intuitions for other, more elaborate constructions.

A categorically minded reader should be asking themselves the following question. We have identified internal and enriched categories as monads in certain bicategories, what about the morphisms between them? Do internal and enriched functors correspond to an obvious notion of morphism between these monads? The answer to this question is a bit more subtle than one might hope. We may return to this point in a later post.

More background on bicategories, and the monads corresponding to internal and enriched categories can be found in Lack’s “A 2-Categories Companion”, which is highly recommended reading.

Strong Monads

Strong monads, the topic of this post, are a somewhat technical looking topic at first glance, requiring more definitions and machinery than we have seen up until now. Unfortunately, they are key to some more interesting topics, both mathematically and in terms of computer science application. As usual when dealing with new abstract ideas, it is useful to focus on intuitions and examples to get a feeling for the formal definitions. This post is longer than might be ideal, but there are plenty of examples.

For those interested in the technical details I skip, some recommended reading:

Monoidal categories: “Categories for the Working Mathematician” by Mac Lane has a very readable account of monoidal categories, despite its reputation for requiring a lot of mathematical background.
Enriched categories: Both volume 2 of Borceux’s “Handbook of Categorical Algebra”, and Riehl’s “Categorical Homotopy Theory” have brief introductions to monoidal categories, to set up a concise introduction to enriched category theory. The standard reference for enriched category theory is Kelly’s “Basic Concepts of Enriched Category Theory”, which also contains the necessary background on monoidal categories. This book can be difficult in places, but the material we require is covered at a reasonable pace.

Monoidal Categories

A monoidal category is a category $\mathcal{V}$ with a monoidal product bifunctor, typically denoted $\otimes$ , and a unit object, $I$ . Intuitively, this is a generalization of the notion of monoid from sets to categories. There are isomorphisms

$\lambda : I \otimes A \rightarrow A \qquad \rho : A \otimes I \rightarrow A$ ,

natural in $A$ , and referred to as the left and right unitor respectively. These encode that $I$ acts as a unit for the multiplication, up to isomorphism. There are also associator isomorphisms:

$\alpha : (A \otimes B) \otimes C \rightarrow A \otimes (B \otimes C)$ ,

natural in $A, B, C$ , encoding associativity up to isomorphism. The unitors and associator are required to satisfy some compatibility equations (referred to as coherence conditions). We won’t need the details, but they can be found in any standard category theory reference.

A symmetric monoidal category is a monoidal category with a further symmetry isomorphisms encoding commutativity up to isomorphism:

$\sigma : A \otimes B \rightarrow B \otimes A$

natural in $A,B$ . Again, the symmetry is required to satisfy some coherence conditions (equations) with respect to the other structure. Finally, a (symmetric) monoidal closed category is a (symmetric) monoidal category such that for each object $A$ , there is an adjunction:

$(-) \otimes A \dashv A \multimap (-)$

Example: Any category $\mathcal{C}$ with products is a symmetric monoidal category, with

$A \otimes B = A \times B \qquad I = 1$

The left and right unitors, associator and symmetry are the “obvious” canonical maps induced by the universal property of products. If $\mathcal{C}$ is Cartesian closed, then it is symmetric monoidal closed, with $A \multimap (-)$ given by the exponential $A \Rightarrow (-)$ .

In particular, the category $\mathsf{Set}$ is symmetric monoidal closed with monoidal product given by Cartesian products, and $A \multimap (-)$ given by the function space functor $A \Rightarrow (-)$ . This is the motivating example for much of what follows, and of practical interest in algebraic examples we shall see later. When working with $\mathsf{Set}$ , if not otherwise stated the monoidal structure is taken to be the Cartesian product structure.

Strength

For a monoidal category $\mathcal{V}$ , and endofunctor $T: \mathcal{V} \rightarrow \mathcal{V}$ , a strength (sometimes referred to as a tensorial strength) for $T$ is a natural transformation

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

which satisfies two coherence conditions with respect to the monoidal structure. A strong functor is a functor with a chosen strength. A strong monad is monad $\mathbb{T}$ with a strong underlying endofunctor, satisfying additional coherence conditions with respect to the monad unit and multiplication. Again, the actual coherence conditions can be found in standard sources, we shall focus on examples and intuitions.

Example: The list and powerset monads are both strong in a unique way, with strengths:

$(a, [b_1,\ldots,b_n]) \mapsto [(a,b_1),\ldots,(a,b_n)]$

$(a, \{ b_1,\ldots, b_n \}) \mapsto \{ (a,b_1), \ldots, (a,b_n) \}$

We shall shortly see that form (and uniqueness) of the strengths for the $\mathsf{Set}$ monads in the previous example are in no way special.

So a crude first sketch of a strength is that it is a well-behaved way of commuting an endofunctor and a monoidal product. You may notice that there are other ways you might imagine commuting an endofunctor with a monoidal product. We shall return to that thought in later posts.

To get a more principled mathematical perspective on strength, unfortunately we need to introduce further abstract machinery.

Enriched Categories

Enriched category theory is a large and potentially complex topic. Fortunately we will only need a few of the basic definitions, and no deep theory. The idea of an enriched category is that often for a category $\mathcal{C}$ , the homsets $\mathcal{C}(A,B)$ carry additional mathematical structure, and this structure interacts well with composition. For example:

Example: The homsets in the category $\mathsf{Pre}$ of preorders and monotone maps actually carry a natural pointwise order:

$f \leq g \Leftrightarrow \forall a. f(a) \leq g(a)$ .

This structure satisfies:

$f_1 \leq f_2 \;\wedge\; g_1 \leq g_2 \quad\Rightarrow\quad g_1 \circ f_1 \leq g_2 \leq f_2$

when the composites are well-defined. So the homsets are actually $\mathsf{Pre}$ -objects, and the composition maps are $\mathsf{Pre}$ -morphisms

$\mathsf{Pre}(B,C) \times \mathsf{Pre}(A,B) \rightarrow \mathsf{Pre}(A,B)$

A close relative of the previous example is the following:

Example: The homsets of the category of all (small) categories $\mathsf{Cat}$ are themselves categories, with morphisms the natural transformations. Furthermore, the composition maps are bifunctors

$\mathsf{Set}(B,C) \times \mathsf{Set}(A,B) \rightarrow \mathsf{Set}(A,C)$

An important trivial example is the following:

Example: The homsets of the category $\mathsf{Set}$ are $\mathsf{Set}$ -objects, and the composition maps are $\mathsf{Set}$ -morphisms

$\mathsf{Set}(B,C) \times \mathsf{(Set}(A,B) \rightarrow \mathsf{Set}(A,B)$

Finally, a slightly different example, which motivates the level of generalization of the formal definition.

Example: The homsets of the category of Abelian groups $\mathsf{Ab}$ can be given the structure of Abelian groups pointwise. With this structure, the composition maps satisfy:

$(g_1 + g_2) \circ f = (g_1 \circ f) + (g_2 \circ f) \qquad 0 \circ f = 0$

and the dual conditions for precomposition. This is not the same as saying the composition maps are $\mathsf{Ab}$ morphisms:

$\mathsf{Ab}(B,C) \times \mathsf{Ab}(A,B) \rightarrow \mathbb{Ab}(A,C)$

This temporarily breaks the pattern with the previous examples. However, there is a monoidal structure on $\mathsf{Ab}$ such that the composition maps are $\mathsf{Ab}$ -morphisms

$\mathsf{Ab}(B,C) \otimes \mathsf{Ab}(A,B) \rightarrow \mathsf{Ab}(A,C)$

In fact this monoidal structure arises via some rather beautiful monad theory, which we will hopefully get to in later posts.

The final example motivates defining enriched categories so that the hom objects can live in monoidal categories.

For a monoidal category $\mathcal{V}$ , a $\mathcal{V}$ -enriched category $\mathcal{C}$ has:

A collection of objects $A,B,\ldots$
For each pair of objects $A,B$ , a hom object $\mathcal{C}(A,B)$ in $\mathcal{V}$ .
For each object $A$ , a morphism $j_A : I \rightarrow \mathcal{C}(A,A)$ . Intuitively, these encode the the identities in the category.
For each triple of objects $A,B,C$ , a morphism $m_{A,B,C} : \mathcal{C}(B,C)\otimes \mathcal{C}(A,B) \rightarrow \mathcal{C}(A,C)$ . These encode composition of morphisms with the enriched category.

This data must satisfy some axioms, ensuring that composition is associative and has units the identities. In fact, some mathematical structures that are far away from our motivating examples are also enriched categories. The original surprising example was that a mild generalization of metric spaces can be seen as enriched categories, as shown by Lawvere.

Example: For any monoidal closed category $\mathcal{V}$ , we can regard $\mathcal{V}$ as a $\mathcal{V}$ -category, with hom objects

$\mathcal{V}(A,B) = A \multimap B$

The identity and composition maps are derived in a reasonably routine way, and can be found in standard sources. This is usually described as $\mathcal{V}$ being canonically enriched over itself.

To connect the worlds of ordinary and enriched categories, note that any $\mathcal{V}$ -category $\mathcal{C}$ , has an underlying ordinary category $\mathcal{C}_0$ , with the same objects, and homsets:

$\mathcal{C}_0(A,B) = \mathcal{V}(I, \mathcal{C}(A,B))$

Composition and identities in $\mathcal{V}_0$ are defined in a natural way. Strictly speaking, to give an enrichment for an ordinary category $\mathcal{C}$ is to give a $\mathcal{V}$ -category $\mathcal{C}'$ , and a specified isomorphism $\mathcal{C} \cong \mathcal{C}'_0$ . Generally, this isomorphism is ignored when there is a natural choice.

Once we’ve defined a new class of objects, we should consider the morphisms between them. A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ consists of:

A mapping $F$ from $\mathcal{C}$ -objects to $\mathcal{D}$ -objects.
For each pair of $\mathcal{C}$ -objects, a $\mathcal{V}$ -morphism $\varphi_{A,B} : \mathcal{C}(A,B) \rightarrow \mathcal{D}(F(A),F(B))$ . Intuitively, these describe the action on morphisms of the functor.

The morphism $\varphi_{A,B}$ are required to satisfy axioms generalizing the usual idea that identities and composition are preserved.

Example: For the constructions we have seen previous:

A $\mathsf{Pre}$ -enriched functor is a functor which is monotone, in that $f \leq g \;\Rightarrow\; F(f) \leq F(g)$ .
A $\mathsf{Cat}$ -enriched functor is a (strict) 2-functor.
A $\mathsf{Set}$ -functor is an ordinary functor.
A $\mathsf{Ab}$ -functor is a functor such that $F(0) = 0$ and $F(f + g) = F(f) + F(g)$ .

Again, it is helpful to connect back to the world of ordinary category theory. A $\mathcal{V}$ -functor $F : \mathcal{V} \rightarrow \mathcal{D}$ induces an ordinary functor $F_0 : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ that agrees with $F$ on objects. Morphisms $f : A \rightarrow B$ in $\mathcal{C}_0$ are $\mathcal{V}$ -morphisms $\hat{f} : I \rightarrow \mathcal{C}(A,B)$ . Then $F_0(f)$ is given by:

$I \xrightarrow{\hat{f}} \mathcal{C}(A,B) \xrightarrow{\varphi_{A,B}} \mathcal{D}(F(A),F(B))$ .

A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ is said to an enrichment of ordinary functor $F' : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ if $F' = F_0$ .

Finally, a $\mathcal{V}$ -natural transformation $\alpha : F \Rightarrow G$ is a family of $\mathcal{V}$ -morphisms $\alpha_A : I \rightarrow \mathcal{D}(F(A),G(A))$ satisfying an axiom generalizing the usual notion of naturality to the enriched setting.

Strength and Enrichment

Finally, we are in a position to relate strength and enrichment. If $\mathcal{V}$ is a monoidal closed category, and $T : \mathcal{V} \rightarrow \mathcal{V}$ an ordinary endofunctor, giving a strength for $T$ is “the same thing as” giving a structure for $T$ as a $\mathcal{V}$ -functor.

Lets unpack this a bit. As described above, we view $\mathcal{V}$ as being canonically enriched over itself. Giving an enriched structure, sometimes referred to as a functorial strength, for $T$ is to give a natural family of morphisms:

$\varphi_{A,B} : A \multimap B \rightarrow T(A) \multimap T(B)$

compatible with the identity and composition maps. That these maps are natural in the sense of ordinary category is equivalent to being an enrichment of the ordinary functor $T$ is an important point that is often skimmed over.

To build such a family given a strength

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

we form the composite:

$A \multimap B \otimes T(A) \xrightarrow{\mathsf{st}_{A \multimap B, A}} T(A \multimap B \otimes A) \xrightarrow{T(\epsilon)} T(B)$

where $\epsilon$ is the counit of the adjunction, which can be seen as an evaluation morphism for function spaces. Taking the transpose of this morphism gives a map:

$A \multimap B \rightarrow T(A) \multimap T(B)$

It takes some checking, but these form the components of an enrichment for $T$ as required. In the other direction, given an enrichment, we can form the composite:

$A \xrightarrow{\eta} B \multimap (A \otimes B) \xrightarrow{\varphi_{B, A \otimes B}} T(B) \multimap T(A \otimes B)$

where $\eta$ is the unit of the adjunction. Taking the transpose of this morphism gives a map:

$A \otimes T(B) \rightarrow T(A \otimes B)$

Again, after a bit of checking, it can be seen that this results in a strength for $T$ . The passages in the two directions are mutually inverse, so for monoidal closed category $\mathcal{V}$ to give a strength for $T$ is equivalent to giving an enrichment for $T$ . This dealt with the endofunctor component, but we are really interested in monads. Here, to give a strength for a monad $\mathbb{T}$ on monoidal closed $\mathcal{V}$ is equivalent to giving an enrichment for $\mathbb{T}$ .

Example: As a special case of this result, as every $\mathsf{Set}$ monad is (trivially) enriched over $\mathsf{Set}$ in a unique way. Therefore, given the observations above, every $\mathsf{Set}$ monad has a unique strength. This has a concrete description as:

$\mathsf{st}_{A,B}(a,t) = \mathbb{T}(\lambda b. (a,b))(t)$

This formula can seem slightly magical if given without context, but it is arrived at by unravelling the strength derived from the unique enrichment. Here we use $\lambda$ notion to define a simple function. The strengths given for the list and powerset monads in the earlier example arise via this construction.

As usual, it is useful to think about algebra examples. For a monad $\mathbb{T}$ given by some equational presentation $(\Sigma,E)$ , the unique strength is given on representatives by:

$\mathsf{st}_{A,B}(a, [t]) = [t[(a,b) / b \mid b \in \mathsf{var}(t)]]$

where $\mathsf{var}(t)$ is the set of variables appearing in the representative term $t$ . As usual, square brackets are somewhat overloaded, denoting both equivalence classes and the substitution operation. In words – we replace each variable $b$ appearing in the representative term $t$ with the variable $(a,b)$ .