The Formal Theory of Iterated Distributive Laws

In this talk we will use the Formal Theory of Monads [4] to shed more light on the theory of Iterated Distributive Laws [2].

The standard theory of distributive laws [1] gives a way to compose two monads on the same category, or equivalently, to lift one monad to the category of algebras of the other in such a way that the algebras for the lifted monad and those for the composite monad coincide. This gives two points of view on the same composite algebraic structure. A motivating example gives two constructions of 2-categories: on the one hand we can use two monads on 2-graphs, one for vertical composition and one for horizontal composition, and on the other hand we can use the free category monad on 1-graphs, and then the free Cat-enriched category monad on Cat-graphs; the resulting structures coincide.

Street’s classic paper [4] constructs, for any 2-category $K$, a 2-category $\text{Mnd}(K)$ of monads on $K$, monad functors, and monad transformations. The paper ends with several enticing results about distributive laws, including that distributive laws are the 0-cells of $\text{Mnd}(\text{Mnd}(K))$. Furthermore, Mnd is a monad on 2-Cat, whose composition takes a distributive law and returns the composite monad.

In [2] the first author extended the theory of distributive laws to be able to compose $n$ monads with coherent distributive laws between them. In this talk we will further extend this to include iterated lifts of the monads and distributive laws between them. While this can be proved directly we find it more interesting to prove it as a corollary of a small extension of [4]. There, the existence of Eilenberg–Moore objects for monads on a given $K$ is expressed via a 2-functor $\text{Alg}:\text{Mnd}(K)⟶K$ picking out the Eilenberg–Moore object for each monad in $K$. We prove that in fact Alg exhibits such $K$ as a pseudo-algebra for Mnd regarded as a 2-monad on the 2-category 2-Cat. The associativity isomorphism “is” Beck’s standard result about algebras via distributive laws. This result is so natural that we suspect it might be considered “folklore”; however we have not seen or heard it mentioned. The proof is long but routine.

Our result about iterated distributive laws follows: given a distributive series of $n$ monads, we can lift the first $n-1$ monads to the category of algebras for the last monad (by [1]), but moreover all the distributive laws lift too, so the process can be iterated, giving an $n-1$ times iterated lift of the first monad in the series. In the case of $n$-categories, this gives a more abstract proof that the $n$-categories constructed by composing the individual monads for composition in each direction coincide with the $n$-categories constructed by iterated enrichment.

This extension of [2] gives us two main benefits that we use in our work. The first is an extension to 2 dimensions, where we look at (strict) distributive laws between 2-monads. The 2-monads and the distributive laws remain strict so the basic definitions do not have any subtlety, but we can extend the lifting theorem to the 2-categories of pseudo-algebras; this is crucial for our continued work on semi-strict $n$-categories [3].

Our further application is for a generalised Eckmann–Hilton argument on $n$-degenerate $(n+1)$-categories. Our re-framing of [2] enables us to give a satisfying abstract account of different expressions of the Eckmann–Hilton argument: via iterated internalisation, or via multiple multiplicative structures and interchange. The equivalence of those structures is usually proved by direct calculation, but we prefer the abstract argument provided by the present work.