strong monads

Quotients of Commutative, Affine and Relevant Monads

We have seen that nice properties such as being commutative, affine, or relevant can be transferred to strong submonads. A natural question to ask is whether something similar applies to quotients? In fact, we can apply the tricks we’ve already seen to get straight to some answers.

Commutative Monads

As strong monad morphisms commute with double strengths, if

\varphi : (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{Q}, \mathsf{st})

is a strong monad morphism, and $\mathbb{T}$ is commutative, we can immediately show

\mathsf{dst}^{\mathbb{Q}} \cdot \varphi \otimes \varphi = \mathsf{dst}^{\mathbb{Q}’} \cdot \varphi \otimes \varphi

If $\varphi \otimes \varphi$ is component-wise epimorphic, then

\mathsf{dst}^{\mathbb{Q}} = \mathsf{dst}^{\mathbb{Q}’}

and $\mathbb{Q}$ is commutative. Even if we restrict attention to where the monoidal structure is products, this condition is not as straightforward as that for monomorphisms. Fortunately there are many special cases where $\varphi$ being a component-wise epimorphism implies $\varphi \times \varphi$ is. In particular, this works nicely for $\mathsf{Set}$ -monads. As all natural transformation are strong in that case, we have

Quotients of commutative monads are commutative.

Affine, Relevant and Cartesian Monads

\varphi : (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{Q}, \mathsf{st})

is a strong monad morphism, and $\mathbb{T}$ is affine, then using the same calculational properties as we did for submonads, but in reverse, we can conclude

\langle \mathbb{Q}\pi_1, \mathbb{Q}\pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{Q}} \cdot \varphi \times \varphi = \varphi \times \varphi

and so if $\varphi \times \varphi$ is component-wise epimorphic

\langle \mathbb{Q}\pi_1, \mathbb{Q}\pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{Q}} = \mathsf{id}

If we restrict attention to $\mathsf{Set}$ -monads, using the result of the previous section, we can conclude

Quotients of affine monads are affine.

A very similar argument allows us to conclude that for $\mathsf{Set}$ -monads

Quotients of relevant monads are relevant.

Combining both these observations gives

Quotients of Cartesian monads are Cartesian.

Algebraic Interpretation

As usual, it pays to see if we use algebraic intuition to justify our conclusions. If we consider $\mathsf{Set}$ -monads presented by operations and equations, being commutative, affine, relevant or Cartesian requires that certain equations between terms hold. We can think of quotient monads as imposing extra equations between terms, so it is unsurprising quotient monads continue to have these nice properties.

Summary

The conclusions above are less general than for submonads. This is because epimorphisms do not interact as nicely with products as monomorphisms do. In the case of $\mathsf{Set}$ -monads everything was about as well-behaved as we could possibly hope.

Affine and Relevant Strong Submonads

We have seen that we can transfer commutativity to strong submonads. Can we transfer other good properties, such as being an affine or relevant monad as well?

Another Commutativity Property

As we are now interested in affine and relevant monads, this post will assume we are working in a category with finite products. We have seen that strong natural transformations commute with double strength. This property will be crucial again today, but we will also need another simple equation.

For a natural transformation

\varphi : F \Rightarrow G

the following equation holds

\varphi \times \varphi \cdot \langle F \pi_1, F \pi_1 \rangle = \langle G \pi_2, G \pi_2 \rangle \cdot \varphi

The proof is a straightforward combination of properties of products and naturality.

Affine Monads

Assume that $\mathbb{T}$ is a affine monad. That is, it is a commutative monad such that the following equation holds

\langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{T}} = \mathsf{id}

\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

a strong monad morphism, then

\varphi \times \varphi \cdot \langle \mathbb{S}\pi_1, \mathbb{S}\pi2 \rangle \cdot \mathsf{dst}^{\mathbb{S}} = \langle \mathbb{T}\pi_1, \mathbb{T}\pi2 \rangle \cdot \varphi \cdot \mathsf{dst}^{\mathbb{S}} = \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{T}} \cdot \varphi \times \varphi = \varphi \times \varphi

If $\varphi$ is component-wise a monomorphism, then so is $\varphi \times \varphi$ , and so

\langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{S}} = \mathsf{id}

Combining this with the results of the previous post, $\mathbb{S}$ is then an affine monad. In categories with pullbacks, we can strengthen this to

Strong submonads of affine monads are affine.

When the base category is set we can go further, to the slogan

Submonads of affine monads are affine.

Relevant Monads

The argument for relevant monads is even easier. Assume $\mathbb{T}$ is a relevant monad, so the following equation holds:

\mathsf{dst}^{\mathbb{T}} \cdot \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle = \mathsf{id}

\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

is a strong monad morphism, then:

\varphi \cdot \mathsf{dst}^{\mathbb{S}} \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{dst}^{\mathbb{T}} \cdot \varphi \times \varphi \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{dst}^{\mathbb{T}} \cdot \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \varphi = \varphi

and so if $\varphi$ is component-wise a monomorphism

\mathsf{dst}^{\mathbb{S}} \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{id}

and from the results of the previous post, $\mathbb{S}$ is relevant. For categories with pullbacks, we have the slogan

Strong submonads of relevant monads are relevant.

and in the case of set monads we get the punchier

Submonads of relevant monads are relevant.

Cartesian Monads

As Cartesian monads are simply monads which are both affine and relevant, we can combine the previous two results to deduce that:

Strong submonads of Cartesian monads are Cartesian.

Algebraic Intuitions

For set monads, being affine or relevant requires that certain equations hold between terms. If we think of a submonad as dropping some of the algebraic structure whilst retaining all applicable equations, intuitively we would expect being affine or relevant to still hold.

Summary

Commutative, affine, relevant and Cartesian monads were important when we discussed both well-known and more recent sufficient conditions for the existence of distributive laws. These results allow us to extract new such monads from those we already understand.

Commutativity of Strong Submonads

In this post we begin to explore transferring nice properties of monads to their submonads. A key tool will be strong monad morphisms. These are monad morphisms which are also strong natural transformations.

Strong Natural Transformations and Right-Strength

In a symmetric monoidal category $\mathcal{C}$ , given a strong endofunctor

(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y)

we can define a right-strength natural transformation

\mathsf{st}’ : F(X) \otimes Y \Rightarrow F(X \otimes Y)

by pre and post-composition with the symmetry of $\mathcal{C}$ .

For strong endofunctors

(F,\mathsf{st})\quad\text{and}\quad (G, \mathsf{st})

requiring that an ordinary natural transformation

\varphi : F \Rightarrow G

be a strong natural transformation is equivalent to requiring it commutes with the left-strengths as follows:

\mathsf{st}’ \cdot \varphi \otimes \mathsf{id} = \varphi \cdot \mathsf{st}’

We see that in this case, being a strong natural transformation can equivalently be phrased in terms of commuting with either the left or right strength. This gives us another convenient equation we can apply in calculations.

Strong Monad Morphisms and Double Strengths

Recall for a strong monad on a monoidal category, using the left and right strength, and the monad multiplication, we can define two double strength natural transformations:

\mathsf{dst}, \mathsf{dst}’ : \mathbb{T}(X) \otimes \mathbb{T}(Y) \Rightarrow \mathbb{T}(X \otimes Y)

A monad is commutative when the double strengths are equal.

For a strong monad morphism

\varphi : (\mathbb{S},\mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

we can apply commutativity with respect to the left and right strength, and the monad morphism assumption to show that $\varphi$ commutes with both double strengths. That is:

\mathsf{dst}^{\mathbb{T}} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathbb{S}} \quad\text{and}\quad \mathsf{dst}^{\mathbb{T}’} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathbb{S}’}

We have added explicit superscripts to indicate to which monad each double strength corresponds.

This is a key property of strong monad morphisms that allows us to prove some interesting results.

Strong Submonads of Commutative Monads

If we have a $\varphi$ as above, assuming the monad $\mathbb{T}$ is commutative, we can calculate:

\varphi \cdot \mathsf{dst}^{\mathbb{S}} = \mathsf{dst}^{\mathbb{T}} \cdot \varphi \otimes \varphi = \mathsf{dst}^{\mathbb{T}’} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathsf{S}’}

where the middle equality uses the commutativity assumption. Now if $\varphi$ is component-wise a monomorphism, we can conclude that:

\mathsf{dst}^{\mathbb{S}} = \mathsf{dst}^{\mathbb{S}’}

and so the monad $\mathbb{S}$ is commutative.

In full generality, we need the component-wise monomorphism assumption, but if the base category has pullbacks, this is equivalent to requiring $\varphi$ be a monomorphism. In this case it seems appropriate to use the following slogan:

A strong submonad of a commutative monad is commutative.

It is not hard to verify that every natural transformation between set endofunctors is strong. We then get the snappier slogan:

A submonad of a commutative monad is commutative.

Algebraic Intuitions

If we present a set monad by algebraic operations and equations, we have seen that commutativity of a monad is equivalent to all the algebraic operations commuting with each other. If we think of a submonad as dropping some of the algebraic structure whilst retaining all the applicable equations, it is perhaps unsurprising that the monad remains commutative.

Summary

Commutativity is a valuable property to identify in a monad. As verifying commutativity can be a bit of a pain, being able to transfer it to strong submonads can be very convenient.

We will see in forthcoming posts that this is not the only nice property we can transfer along strong monad morphisms.

A Strong Monad is Monoid in the Category of Strong Endofunctors

We encountered the notion of strength when we introduced strong monads. Strength has turned out to be an important idea, for example in discussion of commutative monads which underpin a lot of monad theory.

As strength is so important, we are going to back up, and examine it in a bit more detail, eventually arriving at a concise definition of strong monad.

Our ulterior motive is to set up some background on strong natural transformations so we can learn more about commutative, affine, relevant and cartesian monads in future posts.

Strong functors

Recall, a strength for an endofunctor

F : \mathcal{C} \rightarrow \mathcal{C}

on a monoidal category is a natural transformation

\mathsf{st} : X \otimes F(Y) \Rightarrow F (X \otimes Y)

compatible with the monoidal left unitor and associator, in that

F \lambda \cdot \mathsf{st} = \lambda

and

F \alpha \cdot \mathsf{st} = \mathsf{st} \cdot \mathsf{id} \otimes \mathsf{st} \cdot \alpha

A strong functor is a pair

(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y))

consisting of an endofunctor and a choice of strength.

Strong natural transformations

We now introduce the key notion of this post. A strong natural transformation

\varphi : (F,\mathsf{st}) \rightarrow (G,\mathsf{st})

is an ordinary natural transformation

\varphi : F \Rightarrow G

which commutes with strengths. That is:

\mathsf{st} \cdot \mathsf{id} \otimes \varphi = \varphi \cdot \mathsf{st}

We will overload the symbol $\mathsf{st}$ for any strength to avoid a proliferation of symbols.

Categorical Structure

For a monoidal category $\mathcal{C}$ there is a category $\mathsf{Strong(\mathcal{C})}$ with:

Objects: Strong endofunctors on $\mathcal{C}$
Morphisms: Strong natural transformations, with composition and identities as for ordinary natural transformations.

Checking the required closure properties of strong natural transformations is a routine exercise.

Monoidal Structure

For a monoidal category $\mathcal{C}$ , there is a strict monoidal structure on $\mathsf{Strong}(\mathcal{C})$ with unit

(\mathsf{Id}_{\mathcal{C}}, \mathsf{id})

The tensor product on objects is:

(G,\mathsf{st}) \circ (F, \mathsf{st}) = (G \circ F, X \otimes GF(Y) \xrightarrow{\mathsf{st}}G(X \otimes F(Y)) \xrightarrow{G \mathsf{st}} GF(X \otimes Y))

For morphisms

\varphi : (F_1, \mathsf{st}) \Rightarrow (F_2, \mathsf{st}) \quad\text{and}\quad \gamma : (G_1, \mathsf{st}) \Rightarrow (G_2, \mathsf{st})

their tensor product is the usual composition of natural transformations

\gamma \circ \varphi : G_1 \circ F_1 \Rightarrow G_2 \circ F_2

Verifying the monoidal structure is routine, if fiddly, exercise in applying the definitions.

When we previously discussed strong monads, the definition was only sketched, with detailed deferred to other sources. We are now in a position to give a precise definition of what a strong monad is

A strong monad is a monoid in the category of strong endofunctors.

This is easy to remember, as it is a small variation on the internets favourite meme about monads:

A monad is a monoid in the category of endofunctors.

We just sprinkle the term strong over the slogan for monads, and we get the corresponding slogan for strong monads.

It is not hard to see that there is a strict monoidal forgetful functor to the ordinary category of endofunctors

\mathsf{Strong}(\mathcal{C}) \rightarrow [\mathcal{C}, \mathcal{C}]

so every strong monad is an ordinary monad, along with some additional strength data.

Unpacking the Definition

If we unpack the concise definition above, a strong monad is:

A strong endofunctor $(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \mathsf{st})$
A unit strong natural transformation $(\mathsf{Id}, \mathsf{id}) \Rightarrow (\mathbb{T}, \mathsf{st})$
A multiplication strong natural transformation $(\mathbb{T},\mathsf{st}) \circ (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})$

Such that the usual unit and multiplication axioms hold.

Applying the Definition

To show that this is not just an exercise in meme generation, we can apply the definition above to deduce what a distributive law of strong monad $(\mathbb{T}, \mathsf{st})$ over strong monad $(\mathbb{S}, \mathsf{st})$ should be. We require a strong natural transformation:

\lambda : (\mathbb{T}, \mathsf{st}) \circ (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{S}, \mathsf{st}) \circ (\mathbb{T}, \mathsf{st})

satisfying formally identical equations to those of an ordinary distributive law. Unpacking this, $\lambda$ must be an ordinary distributive law, also satisfying:

\mathbb{S}(\mathsf{st}) \cdot \mathsf{st} \cdot 1 \otimes \lambda = \lambda \cdot \mathbb{T}(\mathsf{st}) \cdot \mathsf{st}

This yields the same definition given in Jacobs “Semantics of Weakening and Contraction” for example.

Summary

By identifying the correct mathematical structure, we have arrived at a concise definition of strong monad paralleling one of the familiar definitions for monads.

Inquisitive readers may wonder if any of the other definitions transfer over cleanly. For example, can we define a strong monad as a monad in a different 2-category? The answer is not yet (except in a rather degenerate way)! As with most things, there is a more general definition of strength, which amongst other things allows us to move away from the restriction to endofunctors that has been conspicuous in this post. Our current level of generality will be sufficient for some forthcoming posts. We may return to this topic on a later occasion. Details can be found on the NLab for example.

Other Monad Strengths

Last time, we saw the notion of strength for a monad. These were natural transformations

$A \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$

which interact well with the monoidal and monad structure. As was mentioned last time, there are other ways we might consider commuting a functor with a monoidal structure. The obvious first choice is to consider a natural transformation of type

$\mathbb{T}(A) \otimes B \rightarrow \mathbb{T}(A \otimes B)$

again, interacting sensibly with the monoidal and monad structure (as before, we leave the details of what this means aside, to concentrate on the main ideas). Such a natural transformation is called a left-strength, denoted $\mathsf{st}'$ . The strength is often referred to as a right-strength for emphasis.

Example: If $\mathcal{V}$ is a symmetric monoidal category we can build a right-strength from a left-strength

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

as the composite:

$\mathbb{T}(A) \otimes B \xrightarrow{\sigma_{\mathbb{T}(A),B}} B \otimes \mathbb{T}(A) \xrightarrow{\mathsf{st}_{B,A}} \mathbb{T}(B \otimes A) \xrightarrow{\mathbb{T}(\sigma_{B,A})} \mathbb{T}(A \otimes B)$

Here $\sigma$ is the symmetry isomorphism from the symmetric monoidal structure. Intuitively, we just swap the inputs, use the strength and swap them back again.

As we know every $\mathsf{Set}$ monad is strong in a unique way, so it also has a unique left-strength. For example, the left-strength for the list monad acts as follows:

$([a_1,\ldots,a_n],b) \mapsto [(a_1,b),\ldots,(a_n,b)]$

Unsurprisingly, the left-strength for the powerset is very similar, visually we just swap square (list formation) brackets for curly (set formation) brackets.

$(\{a_1,\ldots,a_n\},b) \mapsto \{(a_1,b),\ldots,(a_n,b)\}$

We can consider left-strengths beyond symmetric monoidal categories, as their definition does not require the existence of a right-strength. In the cases that will be of interest to us, it will be the interplay between left and right strengths that will matter. To keep things simple, we will assume we are working in a symmetric monoidal category, so the left-strength can be derived from the right-strength (or vice-versa), as in the example above. (To move beyond this setting, we would need to assume further compatibility conditions between any choice of left and right strength, which are automatic when one is derived from the other via a monoidal symmetry.)

Once we have a right-strength $\mathsf{st}$ and a left-strength $\mathsf{st}'$ , we can build a natural transformation of type $\mathbb{T}(A) \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$ . In fact, there are two ways we can do this, either by applying the right-strength first:

$\mathsf{dst} = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}_{A,B}} \mathbb{T}(\mathbb{T}(A) \otimes B) \xrightarrow{\mathbb{T}(\mathsf{st}'_{A,B})} \mathbb{T}^2(A\otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

or applying the left-strength first:

$\mathsf{dst}' = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}'_{A,B}} \mathbb{T}(A \otimes \mathbb{T}(B)) \xrightarrow{\mathbb{T}(\mathsf{st}_{A,B})} \mathbb{T}^2(A \otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

Both these composites are referred to as double strengths. Whenever we see two composites of the same type in category theory, it is natural to consider if they are always the same.

Example: For the list monad, we have:

$\mathsf{dst}([a,b],[c,d]) = [(a,c),(b,c),(a,d),(b,d)]$

whereas

$\mathsf{dst}'([a,b],[c,d]) = [(a,c),(a,d),(b,c),(b,d)]$

notice the difference in the order of the middle two elements.

On the other hand, for the powerset monad, essentially because there is no ordering in subsets:

$\mathsf{dst}(\{a,b\},\{c,d\}) = \mathsf{dst}'(\{a,b\},\{c,d\}) = \{(a,c),(b,c),(a,d),(b,d) \}$

This is not an isolated example, for the powerset monad $\mathsf{dst} = \mathsf{dst}'$ .

The previous examples show us that in general $\mathsf{dst} \neq \mathsf{dst}'$ , but the two composites may agree for some monads. This question, and its implications are another key topic in the theory of monads. We shall begin exploring the details in the next post.

A Note on Terminology

An earlier version of this post used the term costrength for what is termed a left-strength above. This terminology does not align well with the conventional use of “co” in category theory. Thanks to @varkor on mathstodon for persuading me that I should move to the more modern terminology.

There is also a discussion about this terminology on the NLab.

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)$ .