The graphical theory of monads

Abstract

The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theory.

Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning.

This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.

1 Introduction

Street’s formal theory of monads (Street, 1972) shows that a large part of the theory of monads is independent of the specifics of categories, functors, and natural transformations and can be developed in the abstract. This insight both clarifies the nature of the original theory and allows the transfer of results to other settings, such as enriched category theory. Unfortunately, much of the original work is phrased in terms of various 2-categorical constructions, in particular, 2-adjunctions, and the use of this machinery can make the material inaccessible to many.

In this paper, we show that the formal theory of monads can be developed in much more elementary terms, by systematic calculation using equational reasoning, not with ordinary mathematical symbols, but with diagrams. Our aims are twofold. First, we aim to illustrate the power of the graphical language of string diagrams, by explicitly proving non-trivial results in formal monad theory as our running example. Second, we hope to present formal monad theory in a more elementary light, opening the insights of Street’s vision to a broader audience.

We assume some basic knowledge of category theory, but otherwise provide a self-contained account of the required material. We begin with background on string diagrams and 2-categories, and the mathematical structures of interest in Sections 2 and 3. This material is adapted from that in Hinze and Marsden (2023), although the account we present here is specialized to the needs of later calculations. The subsequent sections present entirely new material that has not appeared in print before. In Section 4, we introduce the key abstraction of an Eilenberg–Moore object. Section 5 develops what is probably the fundamental result of formal monad theory, that Eilenberg–Moore objects imply that every monad arises from an adjunction, and Section 6 then shows that this adjunction is a canonical choice. Sections 7 and 9 present results about lifting arrows and monads, and require significantly more involved calculations which provide serious illustrations of string-diagrammatic techniques. The intervening Section 8 shows how duality can be exploited to recover results about Kleisli constructions and comonads for free and relates these dualities to the symmetries of our diagrams.

1.1 Contributions

The contributions of the paper are as follows:

• • We provide the first string-diagrammatic account of axiomatic monad theory in a 2-categorical setting. Our work presents an elementary, graphical formulation of Streets formal theory of monads, obviating the need for complex machinery such as 2-adjunctions or constructions involving auxiliary 2-categories. We cover several fundamental aspects, beginning with an explicit diagrammatic definition of Eilenberg–Moore objects and their universal property. This is followed by explicit proofs that:

  • – Every monad arises from an adjunction.

  • – The Eilenberg–Moore adjunction is terminal among such resolutions.

  • – There is a one-to-one correspondence between so called Eilenberg–Moore laws and liftings of arrows.

  • – There is a one-to-one correspondence between Beck distributive laws and monad liftings to Eilenberg–Moore objects.

• • We emphasize geometric intuition for calculational moves such as “dragging”, “bending”, and “splitting” wires and “sliding beads” along wires. Our approach highlights the need for good notational choices, particularly in this graphical setting where there is great freedom to express ideas. We include illustrations of good versus bad diagrammatic choices to develop the intuition of readers new to these techniques — Section 2.5 gives a foretaste.

• • We introduce some diagrammatic notational innovations:

  • – A graphical technique to focus on regions of interest in diagrams where proof steps will occur.

  • – A simple systematic approach to Eilenberg–Moore objects, emphasizing the connection to the base category.

  • – The elementary, but crucial, use of explicit identity transforms to both consistently maintain type information and to isolate the role of equations between arrows in our proofs.

1.2 Related work

Book length expositions of string diagrams, in the style of the present work, can be found in Hinze and Marsden (2023), and its forthcoming sequel (Hinze and Marsden, 2025). Hinze and Marsden (2016) develop the theory of distributive laws using string diagrams for categories, functors, and natural transformations — the calculations transfer directly to the more abstract setting of the current paper. Other topics dealt with using similar techniques can be found in Piróg and Wu (2016) and Hinze and Marsden (2016). Earlier accounts of string diagrams for categorical calculations, with some stylistic differences, can be found in Curien (2008) and Marsden (2014). Historically, string diagrams were already being interpreted in 2-categories by the Australian School of Category Theory in the 1980’s (Aitchison, 1987), and began appearing in formal publications soon after (Street, 1995, 1996). Theoretically, the calculus is a “colourful” variation of the monochrome diagrams used for (planar) monoidal categories (Joyal and Street, 1988, 1991).

String diagrams are used in a variety of settings, with probably the most common being various types of monoidal categories. These methods have been applied in many areas, including quantum theory (Coecke and Kissinger, 2017; Coecke and Gogioso, 2022; Heunen and Vicary, 2019), natural language semantics (Coecke et al., 2010), signal flow graphs (Bonchi et al., 2015), control theory (Baez and Erbele, 2015), economic game theory (Ghani et al., 2018) and (Ghani et al., 2018), Markov processes (Baez et al., 2016), analogue (Baez and Fong, 2015) and digital (Ghica and Jung, 2016) electronics and hardware architecture (Brown and Hutton, 1994), machine learning (Fong et al., 2019), linear algebra (Sobocinski, 2019), and logic (Clingman et al., 2021; Bonchi et al., 2024). General background on these different graphical calculi can be found in Selinger (2011). Although each of these diagrammatic languages has its own distinctive “feel”, they have much in common, and the present work could serve as an introduction to the general methods.

2 Background: String diagrams

We begin our introduction to string diagrams in terms of conventional category theory. That is, we consider categories, functors, and natural transformations. Once we have introduced the required notation, we move to the more abstract setting of 2-categories, of which ${\mathbf{Cat}}$ , the 2-category of categories, functors, and natural transformations, is the paradigmatic example. A systematic account of this style of graphical reasoning for elementary category theory can be found in Hinze and Marsden (2023).

We first recall the traditional notation most commonly used in category theory.

Categories are drawn as points or vertices, zero-dimensional objects, typically depicted as letters ${\mathcal{C}}$ , ${\mathcal{D}}$ , and so on. A functor is drawn as a one-dimensional object, in the form of an arrow between two categories. Finally, natural transformations appear as two-dimensional objects, as double arrows intuitively filling the region between a parallel pair of functor arrows. Given its appearance, the notation for a natural transformation is sometimes referred to as an eye diagram.

String diagrams invert these notational conventions, considering their Poincaré dual.

Now categories are two-dimensional objects, depicted as coloured regions, functors remain one-dimensional, with the slight tweak that they are now drawn vertically, as lines, which we will also refer to as edges or wires, separating the coloured regions of their domain to the right and codomain to the left. Functors can only exit the diagram at the top or bottom boundary, where their wire is labelled with their name. Natural transformations are now the focus of attention, drawn as zero-dimensional vertices, appearing on the wires denoting their domain above and codomain below. This change of emphasis better reflects the significance of the concepts. As described in Mac Lane (1998):

“Category” has been defined in order to be able to define “functor” and “functor” has been defined in order to be able to define “natural transformation.”

With the string diagram notation, natural transformations are the focus of attention, with categories and functors auxiliary concepts that provide vital type information about how they can be combined. In what follows, the names ${\mathcal{C}}$ , ${\mathcal{D}}$ , $\ldots$ will range over categories, ${\mathsf{F}}$ , ${\mathsf{G}}$ , $\ldots$ over functors, and ${\alpha }$ , ${\beta }$ , … over natural transformations.

2.1 Composition

Of course, these concepts do not live in isolation, we build more complicated functors and natural transformations by composition, and this is reflected in our diagrams. Given functors ${\mathsf{G}\mathrel{:} \mathcal{E}\leftarrow \mathcal{D}}$ and ${\mathsf{F}\mathrel{:} \mathcal{D}\leftarrow \mathcal{C}}$ , in pictures,

their composite ${\mathsf{G}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{:} \mathcal{E}\leftarrow \mathcal{C}}$ is drawn as follows:

Notice that symbolically, we write the composite as ${\mathsf{G}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{:} \mathcal{E}\leftarrow \mathcal{C}}$ , with the type information going from right to left. This way, both the type information and order of composition align between the symbolic notation and the diagrams. As a special case, we draw the identity functor on ${\mathcal{C}}$ as an empty region:

As will be discussed later, it is occasionally useful to break this convention, and explicitly draw dashed identity wires for clarity.

Using these conventions, both the unitality equations ${\mathsf{Id}_{\mathcal{D}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{=}\mathsf{F}\mathrel{=}\mathsf{F}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{Id}_{\mathcal{C}}}$ and the associativity equation ${(\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{G})\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{=}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}(\mathsf{G}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F})}$ are built into the notation.

Given natural transformations,

we depict their vertical composite ${\beta \mathrel{\cdot}\alpha \mathrel{:} \mathsf{F}\mathbin{\dot{\to}}\mathsf{H}}$ as the following diagram:

As a special case, an identity natural transformation is represented by the edge for the corresponding functor:

As with identity functors, it will be useful to break the convention for identity natural transformations on occasion, and explicitly draw them as white circles. This will be discussed in detail later.

Again, using these conventions the unitality equations ${id_{\mathsf{G}}\mathrel{\cdot}\alpha \mathrel{=}\alpha \mathrel{=}\alpha \mathrel{\cdot}id_{\mathsf{F}}}$ and the associativity equation ${(\gamma \mathrel{\cdot}\beta )\mathrel{\cdot}\alpha \mathrel{=}\gamma \mathrel{\cdot}(\beta \mathrel{\cdot}\alpha )}$ are built into the notation.

There is a second notion of composition. For natural transformations

we denote their horizontal composite ${\beta \mathord{\mspace{1mu}\circ\mspace{1mu}}\alpha \mathrel{:} \mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathbin{\dot{\to}}\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{G}}$ via horizontal diagrammatic composition:

Vertical and horizontal composition satisfy two coherence conditions, which ensure that they interact without friction. Horizontal composition preserves vertical identities,

\begin{equation*} {id_{\mathsf{G}}\mathord{\mspace{1mu}\circ\mspace{1mu}}id_{\mathsf{F}}\mathrel{=}id_{\mathsf{G}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}}} {}\end{equation*}

and vertical composition:

(2.1) \begin{equation} {(\delta \mathrel{\cdot}\gamma )\mathord{\mspace{1mu}\circ\mspace{1mu}}(\beta \mathrel{\cdot}\alpha )\mathrel{=}(\delta \mathord{\mspace{1mu}\circ\mspace{1mu}}\beta )\mathrel{\cdot}(\gamma \mathord{\mspace{1mu}\circ\mspace{1mu}}\alpha )} {}\end{equation}

The latter property is also known as the interchange law. Again, both properties are built into the notation. The interchange law expresses that the two visual ways of forming a $2\times 2$ matrix of natural transformations are equivalent:

Although unitality and associativity can be built into conventional linear notation by leaving out identities and brackets around composition, the interchange law is an intrinsically two-dimensional notion.

As a corollary of the notational convention for identities, we obtain what Dubuc and Szyld (2013) suggestively call the elevator equations. Intuitively, we can slide vertices up and down wires, which is a very useful manoeuvre to be able to perform during proofs.

(2.2)

2.2 Natural transformations between composite functors

So far, all our natural transformations have been “one-in one-out”. To perform useful calculations, we need to look in more detail at natural transformations between composite functors. For example, we could draw the natural transformation ${\psi \mathrel{:} \mathsf{F}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{G}\mathbin{\dot{\to}}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{J}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{L}}$ as:

but this is probably not the best choice as it mixes symbolic and graphical notation. Instead, we draw separate wires for each element of the composite:

This explicitly exposes the composite wires as multiple threads, which makes it possible to access them directly in our calculations.

2.3 Identity natural transformations

A related topic is the handling of equations between functors. For example, if we have an equation such as ${\mathsf{T}\mathrel{=}\mathsf{U}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}}$ , we can exploit this in our diagrams using explicit identity vertices, depicted by special white circles, in our diagrams:

These explicit identity vertices allow us to “expand” and “collapse” composite wires, as is convenient during our proofs. We will occasionally draw the diagram for an identity vertex to indicate that the corresponding equality holds.

Identity vertices satisfy obvious cancellation identities:

(2.3a)

(2.3b)

We can also fuse identities with other vertices, for example for ${\eta \mathrel{:} \mathsf{Id}\mathbin{\dot{\to}}\mathsf{T}}$ , with ${\mathsf{T}\mathrel{=}\mathsf{U}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}}$ as before:

This use of explicit identities extends in the obvious way to more complex equations, such as ${\mathsf{G}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{=}\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{H}}$ which has composite functors on both sides of the equation, and will be witnessed by vertices of the form:

The notion of an Eilenberg–Moore object introduced in Section 4 introduces equations such as these, and so it is important to have a diagrammatic technique to handle them smoothly.

2.4 Focusing

During calculations, it can sometimes be hard even for experts to identify exactly how a diagram has been changed during a proof step. To address this, we introduce a visual cue to focus on a particular part of a diagram, by highlighting the region of interest. For example, in the following two diagrams,

an equality has been applied to the rectangular regions that appear to be in the spotlight, whilst the regions in shadow remain passive. This graphical trick is a purely cosmetic visual aid, and is not a formal part of the string diagram notation. We indicate the introduction or moving of these highlights in proofs with the hint “focus”, and their removal to reveal a full diagram with “unfocus”.

2.5 Diagram evolution

On one level of abstraction a string diagram is simply a planar graph: vertices are connected by lines, partitioning the plane into regions. (Lines are implicitly oriented from top to bottom, so they must not have a horizontal tangent.) Two-dimensional notation provides considerable artistic freedom. It is quite rare that one gets a drawing “right” the first time — a diagram typically goes through a series of evolutionary steps. To illustrate, we have recorded the genesis of an important property in the paper, Equation (7.4). For the following discussion, it is not important to understand the significance of this equation.

The ugly. Drawing string diagrams is to some extent a matter of personal taste: some authors simply connect the vertices by straight lines, others prefer curvy diagrams. Our initial attempt at Equation (7.4) is shown on the right below.

The two equations are semantically equivalent, even though they look quite different. (In general, string diagrams that are equivalent up to planar isotopy denote the same natural transformation (Joyal and Street, 1991). A planar isotopy is a continuous deformation of a plane diagram that preserves cusps, crossings, and the property of having no horizontal tangents.)

The bad. We made some progress when we drew the path that connects the two occurrences of ${\overline{\mathsf{H}}}$ as a continuous, straight vertical line. In the equation on the left below, the vertical line can be seen as a border. The rendering of the equation suggests a calculational manoeuvre: stuff on the left of the border transmogrifies into stuff on the right, or vice versa. However, the diagram on the right-hand side is still a little unwieldy.

Attempting to extract some geometric intuition for the equation, we pushed the vertical line idea further, replacing the vertex ${\epsilon }$ and the wire left of it by ${\chi^{\mathsf{S}}}$ , folding its definition. This tweak was enlightening as the resulting equation provides a clear geometric intuition: when applied from left to right, the vertex ${\chi^{\mathsf{T}}}$ , transforming to ${\chi^{\mathsf{S}}}$ as it enters the yellow region, and the three wires attached to it are dragged across the border. When a wire crosses another wire, it “creates” a vertex, which is why the diagram on the right has three additional vertices. Sections 7 and 9 detail the significance of these vertices.

The good. The introduction of ${\chi^{\mathsf{S}}}$ was a clarifying idea, but not the final step.

Eschewing the dragging intuition, simplicity won the day and we were drawn to a more neutral formulation. This reflects how we use the equation in practice, applying it from right to left to abstract the more complex formulation to a simpler form.

As is commonplace in graphical reasoning, more than one depiction can prove fruitful. If we switch our attention to the left hand side of the equation and adjust our use of identity vertices, we are lead to the “conical” depiction below.

We will pick up this conical depiction again in Section 9 where particularly the left-most diagram provides just the right emphasis in calculations. If we use a conical depiction for both sides of the equation, we recover a geometrical intuition of sliding the vertical ${\mathsf{H}}$ edge from right to left.

It is amazing how many and how wildly different renderings an equation admits, and the scope for expression that provides.

2.6 2-Categories

So far, we have talked of categories and composing functors and natural transformations. A 2-category is an abstraction of the composition of these entities, in the same way we can think of categories as an abstraction of how functions between sets compose. Instead of categories, functors, and natural transformations, we now talk of objects, arrows, and transforms, respectively. There are two sorts of composition, horizontal and vertical, and these satisfy all the equations previously introduced. The string diagrammatic notation transfers seamlessly to this abstract setting.

There are several reasons to move to this level of abstraction. Results can be proved at a greater level of generality, exploiting the fact that many other categories “look similar” to ${\mathbf{Cat}}$ , the 2-category of categories, functors, and natural transformations. It is also clarifying to understand which results depend on the specifics of ordinary category theory, and which only depend on higher-level structure. Mathematicians study group theory by abstracting away from concrete groups for the same reason.

The relationship between the abstract 2-categorical terminology, the concrete example of ${\mathbf{Cat}}$ , and the string diagrammatic notation is summarized below:

3 Background: key mathematical structures

Now that we have fixed our setting and notational conventions, it is time to introduce the key mathematical structures of interest. This will also serve as an introduction to applying the string diagrammatic notation introduced in Section 2.

3.1 Monads

Our fundamental object of study is that of a monad. A monad on base object ${\mathcal{C}}$ consists of an arrow ${\mathsf{T}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}}$ , and unit and multiplication transforms:

The unit ${\eta \mathrel{:} \mathsf{Id}\mathbin{\dot{\to}}\mathsf{T}}$ looks a tad like a lollipop, the multiplication ${\mu \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{T}\mathbin{\dot{\to}}\mathsf{T}}$ resembles a tuning fork. The unit and multiplication are required to satisfy unitality and associativity equations:

(3.1a)

(3.1b)

As usual in category theory, having introduced a new class of objects, morally we should specify appropriate arrows between monads. There are a few possibilities, so we defer this responsibility to Section 7.

As a trivial but useful example of a monad, we note that the identity ${\mathsf{Id}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}}$ carries the structure of a monad:

Verifying all the axioms boils down to confirming equations of the form:

3.2 Adjunctions

An adjunction between a pair of arrows ${\mathsf{L}\mathrel{:} \mathcal{C}\leftarrow \mathcal{D}}$ and ${\mathsf{R}\mathrel{:} \mathcal{D}\leftarrow \mathcal{C}}$ consists of a pair of counit and unit transforms:

The counit ${\epsilon \mathrel{:} \mathsf{L}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{R}\mathbin{\dot{\to}}\mathsf{Id}}$ resembles a curved cup, the unit ${\eta \mathrel{:} \mathsf{Id}\mathbin{\dot{\to}}\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{L}}$ a cap. They are required to satisfy the following snake equations, which intuitively allow us to straighten out bends in our string diagrams, by pulling a wire straight.

(3.2a)

(3.2b)

In the case of categories, functors, and natural transformations, this definition is equivalent to the many other formulations of adjunctions (Fokkinga and Meertens 1994), but is particularly convenient for graphical reasoning.

An adjoint situation with left adjoint ${\mathsf{L}\mathrel{:} \mathcal{C}\leftarrow \mathcal{D}}$ and right adjoint ${\mathsf{R}\mathrel{:} \mathcal{D}\leftarrow \mathcal{C}}$ is often denoted ${\mathsf{L}\dashv \mathsf{R}\mathrel{:} \mathcal{D}\leftharpoonup \mathcal{C}}$ , with the understanding that the units are given implicitly.

3.3 Maps of adjunctions

As we have introduced adjunctions, we are beholden to consider arrows between these structures. For adjunctions ${\mathsf{L}\dashv \mathsf{R}\mathrel{:} \mathcal{D}\leftharpoonup \mathcal{C}}$ and ${\mathsf{L}'\dashv \mathsf{R}'\mathrel{:} \mathcal{D}'\leftharpoonup \mathcal{C}'}$ , and arrows ${\mathsf{H}\mathrel{:} \mathcal{D}'\leftarrow \mathcal{D}}$ and ${\mathsf{K}\mathrel{:} \mathcal{C}'\leftarrow \mathcal{C}}$ as in the diagram below:

we say that the pair ${\mathsf{H}}$ , ${\mathsf{K}}$ is a map of adjunctions if the following conditions hold:

(3.3)

The conditions relating the units and counits have a nice visual representation exploiting identity transforms:

which we shall refer to as the sliding equations for obvious reasons. In fact, each of the sliding equations implies the other. To show unit sliding implies counit sliding, we calculate:

The other direction is symmetrical.

Now is probably a good time to say a few words about reasoning with string diagrams. First and foremost, in terms of manoeuvres, there is no difference between standard equational reasoning based on one-dimensional notation and equational reasoning using the two-dimensional language of string diagrams. We chain equations, we unfold and fold definitions, and we replace equals with equals. In particular, we use the same popular proof format, attributed to Wim Feijen (Gasteren, van, 1988, p. 107), where each step of the calculation is justified by a hint, enclosed in curly braces. The hints should allow the reader to easily verify that the calculation constitutes a valid proof.

The main advantage of diagrammatic notation is that it silently deals with distracting bookkeeping steps, such as unitality, associativity, and the interchange law, leaving us free to concentrate on the essentials. This is an important aspect of any choice of notation, as advocated by Backhouse (1989). Furthermore, with good diagrammatic choices, we can often exploit topological intuition to identify suitable steps in our reasoning.

3.4 Huber’s construction

Given a monad ${\mathsf{T}}$ and an adjunction ${\mathsf{L}\dashv \mathsf{R}}$ , we can build a new monad with underlying arrow ${\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{L}}$ using Huber’s construction (Huber, 1961). The unit and multiplication of the resulting monad are graphically given by “wrapping up” the monad ${\mathsf{T}}$ using the adjunction:

(3.4a)

(3.4b)

The special case we are particularly interested in is when the monad ${\mathsf{T}}$ is the identity monad. The resulting composites,

show that every adjunction induces a monad. The proofs of the unitality and associativity axioms, (3.1a) and (3.1b), are left as instructive exercises to the reader. The solutions can be found in Hinze and Marsden (2023), and a significant hint is provided in Section 3.5.

3.5 Monad actions and transforms of actions

Adjunctions and monads are central concepts of category theory. The third key structure we require is the less well-known notion of a left monad action. Intuitively, a left action can be thought of as a generalization of the possibly more familiar idea of an Eilenberg–Moore algebra, see also Appendix 1.

Given a monad ${(\mathsf{T}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ , a left action of ${\mathsf{T}}$ , or left ${\mathsf{T}}$ -action, consists of an object ${\mathcal{D}}$ , an arrow ${\mathsf{A}\mathrel{:} \mathcal{C}\leftarrow \mathcal{D}}$ , and a transform ${\alpha \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{A}\mathbin{\dot{\to}}\mathsf{A}}$ , graphically:

We occasionally say ${\alpha }$ is a left ${\mathsf{T}}$ -action on ${\mathsf{A}}$ with source ${\mathcal{D}}$ for emphasis. By abuse of language, we refer to ${\mathsf{A}}$ as the carrier of ${\alpha }$ . The transform ${\alpha }$ must respect the unit and multiplication of the monad ${\mathsf{T}}$ , in that the following unit and multiplication axioms hold.

(3.5a)

(3.5b)

For conciseness, we often refer to an action using the diagram for its transform (pars pro toto), as this implicitly defines all the other data.

Given a pair of ${\mathsf{T}}$ -actions with the same source, a transform of actions or action transform,

is a transform ${{h}\mathrel{:} \mathsf{A}\mathbin{\dot{\to}}\mathsf{B}}$ such that the right-turn axiom holds:

(3.6)

As a first example of an action, we note that the monad axioms (3.1a) and (3.1b) imply that the monad multiplication

is a left ${\mathsf{T}}$ -action.

Adjunctions are also a source of actions: If ${\mathsf{L}\dashv \mathsf{R}\mathrel{:} \mathcal{D}\leftharpoonup \mathcal{C}}$ generates ${\mathsf{T}\mathrel{:} \mathcal{D}\leftarrow \mathcal{D}}$ , then ${\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon }$ is a ${\mathsf{T}}$ -action on ${\mathsf{R}}$ .

We refer to this as the canonical action induced by the adjunction and introduce the shorthand ${\chi \mathbin{:=}\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon }$ , graphically:

The proof of the unit axiom (3.5a) is an easy exercise in applying the snake equation (ignore the dashed wires for the moment):

For the multiplication axiom (3.5b) there is nothing to do:

The left-hand side is simply a redraw of the right-hand side. We can make an interesting observation: If we replace the dashed lines, the identity wires, by the left adjoint ${\mathsf{L}}$ , then we obtain proofs that Huber’s composites, (3.4a) and (3.4b), satisfy the left unital axiom (3.1a) and the multiplication axiom (3.1b).

Furthermore, given any left action ${\alpha \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{A}\mathbin{\dot{\to}}\mathsf{A}}$ and arrow ${\mathsf{B}\mathrel{:} \mathcal{D}\leftarrow \mathcal{E}}$ , we can form a new action by “outlining” on the right-hand side, as follows:

(3.7)

In fact, for a fixed left ${\mathsf{T}}$ -action ${\alpha \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{A}\mathbin{\dot{\to}}\mathsf{A}}$ the outlining operation is functorial. If we have an arbitrary transform ${{h}\mathrel{:} \mathsf{B}\mathbin{\dot{\to}}\mathsf{C}}$ , then the composite

(3.8)

is a ${\mathsf{T}}$ -action transform, as by the elevator equations (2.2):

(3.9)

Associativity and preservation of identities is trivial to see diagrammatically. (We have seen that ${\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon }$ is a left action, and therefore we have a second proof that the multiplication ${\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{L}}$ is a left action.) Outlining will be a key feature of the universal property presented in Section 4.

With these observations in place, we note that the multiplication axiom (3.5b) is equivalent to saying a left ${\mathsf{T}}$ -action ${\alpha \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{A}\mathbin{\dot{\to}}\mathsf{A}}$ is simultaneously an action transform of type:

(3.10)

We make use of this idea in Section 5.

As with all string diagrams, it is worth considering different ways of depicting left actions. These can allow us to highlight the intuitions for manipulations performed in proofs, or simply be more convenient in certain situations. For example, we will often use the compact, less symmetrical rendering

which emphasizes the idea of ${\mathsf{T}}$ acting on the left of ${\mathsf{A}}$ . It is also sometimes useful to adjust the orientation, so that the ${\mathsf{A}}$ wire lies in a more passive horizontal direction:

As soon as you have gained some experience with diagrams, you start to relax the rules a little. For example, we allow edges to enter or exit the sides of diagrams, as was done above. As edges must not have zero gradient, they can be extended unambiguously to a diagram in which all edges enter from the top and exit from the bottom of the diagram. To illustrate, the diagram above can be extended to

but ween gain little clarity at the cost of significant horizontal space.

Another perhaps surprisingly useful depiction we will encounter in Section 9.3 is

When reasoning with string diagrams, for example the proofs in this paper, we would encourage readers to play with alternative diagrammatic renderings to help clarify their understanding of the proof moves involved.

4 From Eilenberg–Moore categories to Eilenberg–Moore objects

Using the definition of monad, a reasonable amount of monad theory can be developed within a 2-category. For example, the graphical arguments about composing monads using distributive laws and the Yang-Baxter equation presented in Hinze and Marsden (2016), building upon the original work of Beck (1969) and Cheng (2011), transfer smoothly to the 2-categorical setting.

However, for many of the more interesting results, we need a bit more. In ordinary category theory, there are two categories associated with a monad ${\mathsf{T}}$ , the Eilenberg–Moore category (Eilenberg and Moore, 1965), commonly denoted ${\mathcal{C}^{\mathsf{T}}}$ , and the Kleisli category (Kleisli, 1965), often denoted ${\mathcal{C}_{\mathsf{T}}}$ . These constructions cannot be directly transferred to the 2-categorical setting, as they involve the explicit construction of new categories in terms of objects and arrows of the base category, and the structures of the monads involved. This presents a challenge for developing more serious aspects of monad theory at this level of abstraction.

Street (1972) resolved this problem by identifying the correct abstraction of the Eilenberg–Moore construction in the 2-categorical setting. In this section, we introduce this machinery in diagrammatic terms, laying the foundations for the proofs in subsequent sections. Further background in more traditional notation can be found in Lack and Street (2002), Kelly and Street (2006), and Lack (2009).

Given a monad ${(\mathsf{T}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ , a left ${\mathsf{T}}$ -action

is universal if it satisfies the following two properties.

First, for every left ${\mathsf{T}}$ -action

there exists a unique comparison arrow

such that ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{K}\mathrel{=}\mathsf{A}}$ and ${\chi^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{K}\mathrel{=}\alpha }$ , graphically:

(4.1)

Second, given two left actions, ${\alpha }$ and ${\alpha '}$ , with induced comparison arrows, ${\mathsf{K}}$ and ${\mathsf{K}'}$ , and a ${\mathsf{T}}$ -action transform between them,

there exists a unique comparison transform

such that ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}{k}\mathrel{=}{h}}$ , graphically:

(4.2)

Note Conditions (4.1) and (4.2) depict two variants of the same equation, by making different choices about where to insert identity vertices to ensure consistent labelling at the boundaries. Essentially, this is a choice between exposing multiple wires or abstracting to a single composite at the boundary of our diagrams. We shall prefer the latter choice as it proves more convenient in the calculations we shall encounter.

An object carrying the structure of a universal left action is referred to as an Eilenberg–Moore object for ${\mathsf{T}}$ , denoted ${\mathcal{C}^{\mathsf{T}}}$ . In the graphical representation, an Eilenberg–Moore object ${\mathcal{C}^{\mathsf{T}}}$ is represented by a “dotted” region, reusing the colour of ${\mathcal{C}}$ . As one might expect, in the case of categories, functors, and natural transformations, the Eilenberg–Moore object of a monad is the same thing as its Eilenberg–Moore category (Eilenberg and Moore, 1965), see Appendix 1.

How is the universal property used in calculations? The typical pattern in later sections is that by carefully choosing suitable left ${\mathsf{T}}$ -actions and ${\mathsf{T}}$ -action transforms, the universal property yields new arrows and transforms, and in each case these satisfy equations that we can exploit in our calculations. We shall see many examples of this technique in what follows.

At the risk of dwelling on the obvious, a universal action establishes a one-to-one correspondence between left ${\mathsf{T}}$ -actions on ${\mathsf{A}}$ and arrows ${\mathsf{F}}$ with ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{=}\mathsf{A}}$ . In one direction, given an action ${\alpha \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{A}\mathbin{\dot{\to}}\mathsf{A}}$ , the desired arrow ${\mathsf{F}}$ is simply the unique comparison arrow. In the other direction, given ${\mathsf{F}}$ with ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}\mathrel{=}\mathsf{A}}$ we can construct an actiony outlining the universal action, placing the identity cells above and below:

The uniqueness property guarantees that the correspondence is one-to-one.

The following consequence of the universal property provides us with a jolly useful proof principle. Given a transform ${{h}\mathrel{:} \mathsf{A}\mathbin{\dot{\to}}\mathsf{B}}$ with ${\mathsf{A},\mathsf{B}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{D}}$ , the composite

is an action transform due to the functoriality of “outlining” (3.8). Consequently, for transforms

the uniqueness part of the universal property immediately yields that

We will exploit this property by saying ${\mathsf{U}^{\mathsf{T}}}$ is left-cancellative.

5 Every monad with an Eilenberg–Moore object is induced by an adjunction

We begin our exploration of how the universal property of Eilenberg–Moore objects can be applied to establish results in monad theory. Our aim is to show that every monad with an Eilenberg–Moore object is induced by an adjunction. One could describe this as the fundamental result of formal monad theory, as every subsequent result hinges on the existence of this adjunction. To establish the result we proceed in three steps: first, we construct the “raw data”, the adjoints and the units; second, we show that this data gives the original monad, via Huber’s construction; third, we prove the snake equations.

5.1 Adjoints and units

Let ${(\mathsf{T}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ be a monad. The Eilenberg–Moore object immediately gives us an arrow ${\mathsf{U}^{\mathsf{T}}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}^{\mathsf{T}}}$ , which we anticipate serves as the right adjoint. As a first step toward establishing an adjunction, we would like to find a candidate left adjoint of type ${\mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{C}}$ . To this end, we recall that the monad multiplication is simultaneously left monad action. Therefore, by the universal property there exists a unique comparison arrow ${\mathsf{F}^{\mathsf{T}}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{C}}$ such that

(5.1)

Since ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}^{\mathsf{T}}\mathrel{=}\mathsf{T}}$ , an obvious choice for the unit of our adjunction is the unit of the monad ${\mathsf{T}}$ .

(5.2)

Finally, the counit ${\epsilon \mathrel{:} \mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}\mathbin{\dot{\to}}\mathsf{Id}}$ is constructed using a suitable comparison transform. To this end, we need to find an action transform between actions whose comparison arrows are ${\mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ and ${\mathsf{Id}}$ , respectively. We do not have to look far:

• The comparison arrow of the source action has to be ${\mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ . Since ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}(\mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}})\mathrel{=}\mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ , the “outlined” multiplication, see also (3.7), is of the right type:

• The comparison arrow of the target action has to be ${\mathsf{Id}}$ . The universal ${\chi^{\mathsf{T}}}$ itself is an action with carrier ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{Id}}$ :

Now recall from Section 3.5 that an action is simultaneously an action transform (3.10). In our case, the universal action ${\chi^{\mathsf{T}}}$ itself is an arrow of the desired type:

Consequently, the universal property gives a comparison transform:

satisfying the following instance of (4.2):

(5.3)

Observe that the universal and the canonical action coincide, provided, of course, that we succeed in establishing the adjunction ${\mathsf{F}^{\mathsf{T}}\dashv \mathsf{U}^{\mathsf{T}}}$ .

5.2 Huber’s construction yields the original monad

We now have arrows ${\mathsf{F}^{\mathsf{T}}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{C}}$ and ${\mathsf{U}^{\mathsf{T}}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}^{\mathsf{T}}}$ , and transforms ${\eta \mathrel{:} \mathsf{Id}\mathbin{\dot{\to}}\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}^{\mathsf{T}}}$ and ${\epsilon \mathrel{:} \mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}\mathbin{\dot{\to}}\mathsf{Id}}$ . We wish to confirm that this data induces the original monad, via Huber’s construction. We have already seen that ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}^{\mathsf{T}}\mathrel{=}\mathsf{T}}$ , and the unit of the adjunction is the unit of the monad by construction. It remains to confirm that the induced monad has the same multiplication. This follows straightforwardly from equations we have already established:

(5.4)

We replace the left chamber of the heart, the canonical action we focus on, by the universal action (5.3), and then plug in the definition of the multiplication (5.1).

5.3 Every Eilenberg–Moore object induces an adjunction

It remains to confirm that ${\eta }$ and ${\mu }$ satisfy the snake equations, establishing the adjunction ${\mathsf{F}^{\mathsf{T}}\dashv \mathsf{U}^{\mathsf{T}}}$ . For the first snake equation (3.2a), we reason as follows:

Firstly, we introduce an identity vertex to combine two wires into a ${\mathsf{T}}$ wire. We then replace the canonical with the universal action as indicated by the focus, and simplify with the action unit axiom.

The second snake equation (3.2b) is more subtle to prove. Trying to establish the equation directly, we quickly discover there is no obvious calculation step we can apply. The plan therefore is to exploit the fact that ${\mathsf{U}^{\mathsf{T}}}$ is left-cancellative, and first prove an equality for a more complex diagram, which allows us to get the proof off the ground.

We calculate:

Consider the first diagram. We have placed a ${\mathsf{U}^{\mathsf{T}}}$ wire to the left of the snake and added suitable identity vertices, ${\mathsf{T}\mathrel{=}\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}^{\mathsf{T}}}$ . This turns the snake into the heart-like shape we have seen before. We then extract an identity from the unit, apply Huber’s construction of the monad multiplication, and tidy up using the monad unit axiom. Applying that ${\mathsf{U}^{\mathsf{T}}}$ is left-cancellative then completes the proof. We will subsequently refer to ${\mathsf{U}^{\mathsf{T}}}$ and ${\mathsf{F}^{\mathsf{T}}}$ , respectively, as the underlying and free arrows of ${\mathcal{C}^{\mathsf{T}}}$ .

6 Eilenberg–Moore comparison and the terminal resolution

Given a monad ${(\mathsf{T}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ , an adjunction ${\mathsf{L}\dashv \mathsf{R}\mathrel{:} \mathcal{C}\leftharpoonup \mathcal{D}}$ is called a resolution of ${\mathsf{T}}$ , if the adjunction induces the monad via Huber’s construction. This implies, in particular, that we can express the multiplication using the canonical action:

(6.1)

We wish to compare two resolutions of the same monad. To do so, for resolutions

it is natural to consider maps of adjunctions between them, as introduced in Section 3.3. As the monad and its base object are fixed, we restrict to maps of adjunctions with one component the identity, as in the following diagram:

We typically refer to such a map using the arrow ${\mathsf{K}}$ (pars pro toto).

In Section 5 we saw that if a monad ${\mathsf{T}}$ has an Eilenberg–Moore object, then this induces an adjunction ${\mathsf{F}^{\mathsf{T}}\dashv \mathsf{U}^{\mathsf{T}}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftharpoonup \mathcal{C}}$ , which is a resolution of ${\mathsf{T}}$ . Observe that (5.1) is an instance of (6.1). Our aim is to show this adjunction is a canonical choice, it is the terminal resolution: For every resolution ${\mathsf{L}\dashv \mathsf{R}\mathrel{:} \mathcal{C}\leftharpoonup \mathcal{D}}$ of ${\mathsf{T}}$ , there is a unique comparison map from ${\mathsf{L}\dashv \mathsf{R}}$ to ${\mathsf{F}^{\mathsf{T}}\dashv \mathsf{U}^{\mathsf{T}}}$ .

Quite pleasingly, we can use the defining properties of the comparison map

(6.2a)

(6.2b)

(6.2c)

(6.2d)

to derive the definition of ${\mathsf{K}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{D}}$ . Here we write ${\eta ^{\mathsf{T}}}$ and ${\epsilon ^{\mathsf{T}}}$ for the unit and counit of the adjunction ${\mathsf{F}^{\mathsf{T}}\dashv \mathsf{U}^{\mathsf{T}}}$ for clarity. Our principal tool is the universal property of Eilenberg–Moore objects, so we need to determine a suitable carrier and a suitable action. The second axiom (6.2b) identifies the carrier as ${\mathsf{R}}$ . The third axiom (6.2c), the counit sliding equation, fixes the action itself:

We use the second axiom (6.2b) to eliminate the occurrence of ${\mathsf{K}}$ on the left-hand side. The resulting transform is the canonical action ${\chi }$ , the outlined counit ${\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon }$ , which a left ${\mathsf{T}}$ -action on ${\mathsf{R}}$ . Therefore, we can invoke the universal property to conclude that there is a unique ${\mathsf{K}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{E}}$ such that ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{K}\mathrel{=}\mathsf{R}}$ and ${\chi^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{K}\mathrel{=}\mathsf{R}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon \mathrel{=}\chi }$ , graphically:

(6.3)

For reasons of hygiene, we have added explicit identity vertices so that the bordering wires and regions agree. We were less fastidious in the previous proof to avoid unhelpful diagrammatic clutter. The reader is encouraged to add suitable identity vertices to ensure everything is in order.

It remains to verify that the data actually constitutes a map of adjunctions. For the first axiom (6.2a), we appeal to uniqueness. As we already know that the left adjoint ${\mathsf{F}^{\mathsf{T}}}$ is induced by the multiplication of the monad, it suffices to show that ${\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{L}}$ is also induced by ${\mu \mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{T}\mathbin{\dot{\to}}\mathsf{T}}$ .

We fold the definition of ${\chi }$ (6.3) and then use the fact that ${\mathsf{L}\dashv \mathsf{R}}$ generates the monad ${\mathsf{T}}$ (6.1).

The second and the third axiom, (6.2a) and (6.2c), hold by construction. Finally, the fourth axiom (6.2d) holds trivially as the unit of the monad and the units of the adjunctions coincide. This completes the proof that there is a unique map of adjunctions from every resolution to the Eilenberg–Moore resolution.

7 Eilenberg–Moore laws classify liftings

If we have an arrow ${\mathsf{H}\mathrel{:} \mathcal{D}\leftarrow \mathcal{C}}$ and monads ${\mathsf{S}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}}$ and ${\mathsf{T}\mathrel{:} \mathcal{D}\leftarrow \mathcal{D}}$ , it is natural to ask when this induces an arrow ${\overline{\mathsf{H}}\mathrel{:} \mathcal{D}^{\mathsf{T}}\leftarrow \mathcal{C}^{\mathsf{S}}}$ between the corresponding Eilenberg–Moore objects. It turns out that there is a one-to-one correspondence between certain well-behaved arrows ${\overline{\mathsf{H}}}$ , so-called liftings, and transforms known as Eilenberg–Moore laws. Establishing this relationship is the aim of this section.

7.1 Liftings and Eilenberg–Moore laws

For monads ${\mathsf{S}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}}$ and ${\mathsf{T}\mathrel{:} \mathcal{D}\leftarrow \mathcal{D}}$ and arrow ${\mathsf{H}\mathrel{:} \mathcal{D}\leftarrow \mathcal{C}}$ , we say that ${\overline{\mathsf{H}}\mathrel{:} \mathcal{D}^{\mathsf{T}}\leftarrow \mathcal{C}^{\mathsf{S}}}$ is a lifting of ${\mathsf{H}}$ , if and only if they commute with underlying arrows: ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{H}}\mathrel{=}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{S}}}$ . Graphically, this equality is captured by identity vertices:

Furthermore, we say that

is an Eilenberg–Moore law if it satisfies the following two coherence conditions with respect to the monad structure:

(7.1a)

(7.1b)

We draw these diagrams in this way to emphasize the intuition that the Eilenberg–Moore law allows us to “drag” the monad structure across the ${\mathsf{H}}$ wire.

EM-laws generalize left actions of a monad: a left action is an EM-law to the identity monad. If we “erase” the lower halves, the yellow regions, of the coherence conditions above, (7.1a) and (7.1b), we obtain the axioms of left actions, (3.5a) and (3.5b).

Picking up a loose thread, in Section 3.1 we postponed introducing a suitable class of arrows between monads. We now fulfill this obligation, and form monads and EM-laws into a category suitable for later developments.

The identity EM-law on the monad ${\mathsf{T}}$ is given by ${{id}\mathrel{:} \mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{Id}\mathbin{\dot{\to}}\mathsf{Id}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{T}}$ :

The identity trivially satisfies the coherence conditions, (7.1a) and (7.1b).

The composition of two EM-laws is formed by adjoining the laws vertically:

where ${\kappa / \lambda }$ is symbolic notation for the composite law. The unit axiom (7.1a) for this composite then follows from the equalities:

We drag the unit ${\eta }$ twice, first across the functor ${\mathsf{H}}$ and then a second time across the functor ${\mathsf{K}}$ . We proceed in an analogous fashion to establish the multiplication axiom (7.1b), dragging the fork twice:

It remains to show that the composition is unital and associative, with the identity as its neutral element. This is, however, visually evident as we stack the laws vertically.

7.2 A one-to-one correspondence between Eilenberg–Moore laws and left actions

Let ${\mathsf{S}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C}}$ and ${\mathsf{T}\mathrel{:} \mathcal{D}\leftarrow \mathcal{D}}$ be monads with Eilenberg–Moore objects. Our first goal is to establish a one-to-one correspondence between

1. 1. Eilenberg–Moore laws of type ${\mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{H}\mathbin{\dot{\to}}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{S}}$ and

2. 2. left ${\mathsf{T}}$ -actions on ${\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{S}}}$ .

Using the results of Section 5, there is an adjunction ${\mathsf{F}^{\mathsf{S}}\dashv \mathsf{U}^{\mathsf{S}}\mathrel{:} \mathcal{C}\leftharpoonup \mathcal{C}^{\mathsf{S}}}$ inducing ${\mathsf{S}}$ via Huber’s construction. Using this adjunction, we show that every Eilenberg–Moore law yields a left ${\mathsf{T}}$ -action via the mapping:

(7.2)

We split the ${\mathsf{S}}$ wire of the EM-law and then “bend the right leg up”. Equivalently, we can place the universal action below the law — recall that the canonical and the universal action coincide, ${\mathsf{U}^{\mathsf{S}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\epsilon \mathrel{=}\chi^{\mathsf{S}}}$ (5.3). Of course, we need to show that the resulting transform is a left action but this is immediate as we compose two EM-laws, the given one and the universal action.

In the other direction, given a left ${\mathsf{T}}$ -action we can form an Eilenberg–Moore law by “bending the right arm down”:

(7.3)

The resulting transform looks a tad like a humanoid robot. In order to maintain the parallel alignment of our wires, we have drawn the vertex as a larger blob with greater space to connect them. Notice that the robot’s right hip uses the unit of the adjunction ${\mathsf{F}^{\mathsf{S}}\dashv \mathsf{U}^{\mathsf{S}}}$ to bend the wire down, whereas the left hip is merely a sudden change in direction of a downward wire. Of course, we must verify this composite satisfies the two axioms of an Eilenberg–Moore law. For the unit axiom (7.1a), we calculate:

This is a one-step proof simply applying the left action unit axiom (3.5a), which removes the blob.

The multiplication proof (7.1b) is no more complicated.

We apply the multiplication axiom (3.5b), turning one blob into two blobs. The second step is more interesting. We deliberately complicate the diagram by the insertion of an extra “kink” in a wire via the snake equation (3.2b), introducing Huber’s multiplication at the bottom of the diagram.

Finally, it is not hard to see that the mappings, (7.2) and (7.3), establish a one-to-one correspondence between Eilenberg–Moore laws of type ${\mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{H}\mathbin{\dot{\to}}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{S}}$ and left ${\mathsf{T}}$ -actions on ${\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{S}}}$ — the snake equations do the trick.

7.3 A one-to-one correspondence between left actions and liftings

Driving the proof home, the universal property of Eilenberg–Moore objects immediately gives a one-to-one correspondence between

1. 1. Left ${\mathsf{T}}$ -actions on ${\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{S}}}$ and

2. 2. liftings ${\overline{\mathsf{H}}\mathrel{:} \mathcal{D}^{\mathsf{T}}\leftarrow \mathcal{C}^{\mathsf{S}}}$ such that ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{H}}\mathrel{=}\mathsf{H}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{S}}}$ .

We use the notation for the lifted arrow induced by an Eilenberg–Moore law . From the discussion above, by the universal property and the characterization of the counit (5.3), this will satisfy:

(7.4)

We consider liftings in more detail in Section 9.

8 Kleisli objects and duality

When doing mathematics, or anything else for that matter, it is always nice to get things for free. In the case of the monad theory we have been developing, it pays us to consider if we can exploit some of the symmetries of our diagrams. For example, what happens if we mirror our diagrams about a vertical or horizontal axis? By pursuing this idea, we recover a lots of additional results in the theory of both monads and comonads.

We begin by considering reflection about a vertical axis. If we examine the key notion of a monad, reflecting all the diagrams in this way results in exactly the same structure.

Fortunately, things get more interesting when we consider monad actions. Given a monad ${(\mathsf{M}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ , a left action of ${\mathsf{T}}$ on ${\mathsf{A}\mathrel{:} \mathcal{C}\leftarrow \mathcal{E}}$ was defined to be a

such that Equations (3.5a) and (3.5b) hold. By mirroring about the vertical axis, that is, taking the horizontal reflection, we discover the notion of a right ${\mathsf{T}}$ -action as an

satisfying the equations

(8.1a)

(8.1b)

Similarly, a transform of right actions is required to satisfy the vertical mirror image of Equation (3.6).

Taking this mirroring idea further, we can dualize the notion of Eilenberg–Moore object. We will do this in full detail, so that interested readers can contrast with Section 4 to see the impact of dualizing the definitions given there.

For a monad ${\mathsf{T}}$ , we say that a right action

is universal if it satisfies the following two properties. First, for every right ${\mathsf{T}}$ -action

there exists a unique comparison arrow

such that ${\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}_{\mathsf{T}}\mathrel{=}\mathsf{A}}$ and ${\mathsf{K}\mathord{\mspace{1mu}\circ\mspace{1mu}}\chi_{\mathsf{T}}\mathrel{=}\alpha }$ , graphically:

(8.2)

Second, given two right actions ${\alpha }$ and ${\alpha '}$ , with induced comparison arrows ${\mathsf{K}}$ and ${\mathsf{K}'}$ , and a right ${\mathsf{T}}$ -action transform

(8.3)

there exists a unique comparison transform

such that ${{k}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}_{\mathsf{T}}\mathrel{=}{h}}$ , graphically:

The object ${\mathcal{C}_{\mathsf{T}}}$ carrying the structure of a universal right action is referred to as a Kleisli object for ${\mathsf{T}}$ . Using a similar convention to that for Eilenberg–Moore objects, graphically, a Kleisli object ${\mathcal{C}_{\mathsf{T}}}$ is represented by a distinctive stippled region, reusing the colour of ${\mathcal{C}}$ . Again, the terminology relates to the fact that the Kleisli object for a monad in ${\mathbf{Cat}}$ is its Kleisli category (Kleisli, 1965). Observant readers will notice that as well as taking the horizontal reflection of our diagrams, we have adjusted some of the names. This is a cosmetic change to ensure we follow standard naming conventions, and we shall continue to do so in what follows.

By mirroring the arguments in Section 5 and 6, we get new results for free. Every monad ${\mathsf{T}}$ with a Kleisli object arises from an adjunction ${\mathsf{F}_{\mathsf{T}}\dashv \mathsf{U}_{\mathsf{T}}\mathrel{:} \mathcal{C}\leftharpoonup \mathcal{C}_{\mathsf{T}}}$ via Huber’s construction, and furthermore this adjunction is the initial resolution.

Similarly, if we reflect Equations (7.1a) and (7.1b) about their vertical axis, we get the following equations, for ${\mathsf{H}}$ of appropriate type:

(8.4a)

(8.4b)

These are the axioms of what is known as a Kleisli law. Again, via an entirely formal process of mirroring the proofs of Section 7, we can derive new results. Specifically, there is a one-to-one correspondence between Kleisli laws for ${\mathsf{H}\mathrel{:} \mathcal{C}\leftarrow \mathcal{D}}$ and liftings ${\overline{\mathsf{H}}\mathrel{:} \mathcal{D}_{\mathsf{T}}\leftarrow \mathcal{C}_{\mathsf{S}}}$ such that ${\overline{\mathsf{H}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{F}^{\mathsf{T}}\mathrel{=}\mathsf{F}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{H}}$ .

Givenhe additional results, we have found simply by reflecting diagrams about the vertical axis, it is natural to ask what happens if we take the vertical reflection, reflecting about the horizontal axis instead. If we reflect the diagrams for the key notion of monad on ${\mathcal{C}}$ , we are lead to a triple

satisfying the equations

(8.5a)

(8.5b)

Such a triple ${(\mathsf{N}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\epsilon \mathrel{:} \mathsf{N}\mathbin{\dot{\to}}\mathsf{Id},\delta \mathrel{:} \mathsf{N}\mathbin{\dot{\to}}\mathsf{N}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{N})}$ , satisfying Equations (8.5a) and (8.5b), in the setting of categories, functors, and natural transformations is precisely the usual definition of a comonad. The general case is the abstraction of comonads to the 2-categorical setting. Therefore, by reflecting all the diagrams in the previous sections about the horizontal axis, we derive further results showing every comonad arises via a canonical adjunction, and lifting results for comonads.

In total, by combining vertical and horizontal reflections, every definition or proof we introduce yields three further mirror images. This is a powerful principle, as without doing further work each time we get four concepts and sets of results for the price of one. In more mathematical language, we are applying dualities of 2-categories:

1. 1. Each 2-category has a dual given by reversing all of the arrows. Taking the horizontal reflection of our diagrams precisely corresponds to considering definitions and proofs in this dual 2-category.

2. 2. Each 2-category has another dual, given by reversing all of the transforms. Taking the vertical reflection of our diagrams then corresponds to considering structures in this second dual 2-category.

3. 3. The two dualities can be combined and diagrammatically this relates to mirroring about both axes.

The string diagrammatic notation plays particularly well with these 2-categorical dualities, as it is easy to visualize their impact on definitions, axioms, and equational proofs.

9 Beck’s distributive laws classify monad liftings

In Section 7, we established tight conditions under which we could lift an arrow to the level of Eilenberg–Moore objects. In this section, we continue this line of thought, considering when we can lift one monad to the Eilenberg–Moore object of another.

9.1 Beck distributive laws

A Beck distributive law or simply Beck law of type ${\mathsf{T}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{S}\mathbin{\dot{\to}}\mathsf{S}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{T}}$ is a transform that is both a Kleisli law and an Eilenberg–Moore law. Graphically,

satisfies the following equations:

(9.1a)

(9.1b)

(9.1c)

(9.1d)

9.2 Monad liftings

We say that a monad ${(\overline{\mathsf{S}}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{C}^{\mathsf{T}},\overline{\eta },\overline{\mu })}$ is a lifting of the monad ${(\mathsf{S}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ if and only if its components commute with the underlying functor:

(9.2)

As usual, the diagrammatic rendering of these properties is instructive: we have

and exploiting these identity vertices, the units and multiplications satisfy the equations:

(9.3a)

(9.3b)

In other words, the identity transform ${{id}\mathrel{:} \mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{S}}\mathbin{\dot{\to}}\mathsf{S}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ is a Kleisli law! This is equivalent to requiring that the following dual equations hold:

(9.4a)

(9.4b)

In other words, the opposite identity transform ${{id}\mathrel{:} \mathsf{S}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}\mathbin{\dot{\to}}\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{S}}}$ is an Eilenberg–Moore law! (This holds in general: an isomorphism is an Eilenberg–Moore law if and only if its inverse is a Kleisli law.) That we have two equivalent pairs of equations for liftings, Equations (9.3a) and (9.3b), and Equations (9.4a) and (9.4b), can be seen as witnessing a certain bias in their diagrammatic rendering. Both capture the single pair of symbolic equations, ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\eta }\mathrel{=}\eta \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ and ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mu }\mathrel{=}\mu \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ . That the symbolic notation is unbiased in this respect comes at the cost of omitting type information that is explicit at the boundaries of our diagrams.

9.3 Lifting the monad arrow

Given a Beck law , we can lift the arrow ${\mathsf{S}}$ to . Building on the one-to-one correspondence between liftings and left actions, the Beck law satisfies the following instance of (7.4):

(9.5)

Observe that ${\chi^{\mathsf{T}}}$ is drawn creatively: the ${\mathsf{U}^{\mathsf{T}}}$ wires point to the right, in order to make the subsequent calculations more visually appealing.

Our goal is now to show that the additional axioms of a Beck distributive law mean that the unit and multiplication also lift to give a monad on ${\mathcal{C}^{\mathsf{T}}}$ .

9.4 Lifting the unit

We begin by aiming to find a candidate unit for the lifted monad. To this end let us briefly pause to explain a general recipe for constructing transforms. Say, we need one of type

The idea is, of course, to appeal to the universal property of the Eilenberg–Moore object, which gives a suitable transform, provided there is an action transform of type:

Then ${\phi }$ is given as the unique comparison transform, satisfying

There are two proof obligations: we need to show (1) that ${\alpha }$ and ${\beta }$ are actions and (2) that ${{h}}$ is an action transform between them. Fortunately, these obligations are often easy to discharge if we use general constructions such as “outlining”. To illustrate, let us apply the recipe to the problem at hand.

Since we aim to construct a lifted unit,

we need to find an action transform of type

(9.6)

The actions are constructed by outlining the universal action (the only action around): once with the source of ${\overline{\eta }}$ , the identity arrow ${\overline{\mathsf{Id}}}$ , and a second time with ${\overline{\mathsf{S}}}$ , the target of ${\overline{\eta }}$ . The universal property induces a unique ${\overline{\eta }}$ such that

Theondition required of the unit of a lifted monad (9.4a) suggests defining

so that the requirement holds by definition.

All that remains to be done is to discharge the proof obligations: (1) ${\chi^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{Id}}}$ and ${\chi^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{S}}}$ are actions via “outlining”; (2) to show that ${\eta \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ is an action transform between them, we first consider an alternative rendering of (9.6) that is more suitable for our graphical calculations:

(9.7)

The arrow ${\mathsf{U}^{\mathsf{T}}}$ is consistently drawn as a cone on the right, in line with the style of (9.5). For the proof of the right-turn axiom (3.6), we need to vertically paste the diagrams: for the left-hand side, we place the transform below the source action, and for the right-hand side above. To establish the axiom, we reason:

(9.8)

We simply drag the unit across the ${\mathsf{U}^{\mathsf{T}}}$ wires using the fact that the identity is a Kleisli law (9.3a) and an Eilenberg–Moore law (9.4a).

9.5 Lifting the multiplication

To find a candidate multiplication for the lifted monad, we follow the same steps as in the previous section. In particular, we use the condition ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mu }\mathrel{=}\mu \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ required of the multiplication of a lifted monad, (9.3b) and (9.4b), to fix the action transform. We obtain the following counterpart of (9.7):

We verify the right-turn axiom (3.6) as follows:

(9.9)

Here we drag the multiplication across the ${\mathsf{U}^{\mathsf{T}}}$ wires using the two multiplication axioms, (9.3b) and (9.4b).

9.6 Lifting the monad

It remains to establish that ${\overline{\eta }}$ and ${\overline{\mu }}$ satisfy the three monad axioms. The pattern in each case is the same. We exploit that ${{id}}$ is an EM-law, repeatedly applying the lifting equations, (9.4a) and (9.4b), to “slide away the veil”, revealing a construction in terms of the original monad. We can then apply the axioms of that monad to further our proof.

For the left unit axiom (3.1a):

and for the right unit axiom (3.1a):

Finally, for the associativity axiom (3.1b):

Therefore, as ${\mathsf{U}^{\mathsf{T}}}$ is left-cancellative, we have established that the required equations hold.

These proofs illustrate a general phenomenon: base transformations pass their properties on to their lifted counterparts — like transformations we can also lift equations.

9.7 A lifting induces a distributive law

We would now like to show that every lifting of ${(\mathsf{S}\mathrel{:} \mathcal{C}\leftarrow \mathcal{C},\eta ,\mu )}$ arises in this way. To do so, we assume a lifting ${(\overline{\mathsf{S}}\mathrel{:} \mathcal{C}^{\mathsf{T}}\leftarrow \mathcal{C}^{\mathsf{T}},\overline{\eta },\overline{\mu })}$ . As ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\mathsf{S}}\mathrel{=}\mathsf{S}\mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}}$ , the lifted arrow ${\overline{\mathsf{S}}}$ is induced by the left ${\mathsf{T}}$ -action:

Calculations (9.8) and (9.9) have established the intuitive equations:

(9.10a)

and

(9.10b)

As we have seen earlier, a left action induces an Eilenberg–Moore law by “bending a wire down”:

To show that this composite is a Beck distributive law, we must confirm that it also satisfies the axioms of a Kleisli law. For the unit axiom, we first observe that

(9.11)

which is the snake equation (3.2a) in disguise.

Combining this handy identity with Equation (9.10a), we establish the Kleisli unit axiom (9.1a):

We proceed in a similar way to establish the multiplication axiom. First, we redraw Equation (5.3), introducing an explicit identity vertex on the left arm of the universal action.

(9.12)

For the proof of the Kleisli multiplication axiom (9.1b), we argue:

It is best to read the proof backwards. The goal is clear: we need to “merge” the two copies of the candidate law into one. To this end, we first replace the lower universal action by the counit (9.12), creating a snake between the two vertical paths. Alas, we cannot immediately pull the wire straight, as this would transmogrify the extremities of the identity vertices attached to the snake, turning an arm into a leg and vice versa. To enable the snake equation, we first need to raise the right identity vertex above the level of the left one, as indicated by the focus. Here, we make essential use of the elevator equations (2.2). The rest is routine: we pull the string straight and then drag the multiplication upwards across the ${\mathsf{U}^{\mathsf{T}}}$ wires (9.10b).

All that remains to be done is to show that the distributive law induced by a lifted monad induces the original monad. But this is straightforward, as the unit and multiplication of a lifted monad are uniquely defined. Assume that we have two lifted units, then ${\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\eta }\mathrel{=}\eta \mathord{\mspace{1mu}\circ\mspace{1mu}}\mathsf{U}^{\mathsf{T}}\mathrel{=}\mathsf{U}^{\mathsf{T}}\mathord{\mspace{1mu}\circ\mspace{1mu}}\overline{\eta' }}$ and consequently ${\overline{\eta }\mathrel{=}\overline{\eta' }}$ as ${\mathsf{U}^{\mathsf{T}}}$ is left-cancellative. An analogous argument shows that lifted multiplications are unique.

10 Conclusion

A great deal more monad theory can be developed graphically in the style of this paper. For example, the convenient notation for Kan extensions (Kan, 1958) presented in Hinze (2012) transfers to the 2-categorical setting. The techniques of that paper enable a diagrammatic account of the theory of codensity monads (Kock, 1966). A graphical formulation of Kan extensions and codensity monads in a graphical style more consistent with the present work will appear in Hinze and Marsden (2025).

If we allow ourselves to move beyond the 2-categorical setting, diagrammatic reasoning can be pushed even further. One shortcoming of working in a 2-category is that there is no convenient abstraction of hom-sets, and this can place some categorical ideas out of reach. Moving to the setting of double categories (Ehresmann, 1963), or even more abstractly to virtual equipments (Cruttwell and Shulman, 2009) can address this problem by providing a connection with profunctors. Myers (2016) presents a graphical language suitable for these settings, very similar to that used in the present work, and this notation was exploited by Arkor and McDermott (2023) to give graphical arguments about relative monads (Altenkirch et al., 2015), which require this additional flexibility. We leave the exploration of these more advanced techniques to further work.