The n-Category Café

Lawvere theories

Until 1963 the traditional way to conceptualize the general theory of algebraic structures was in terms of equational logic. In his doctoral thesis under the supervision of Samuel Eilenberg, Bill Lawvere attempted the unification of our understanding of universal algebra by using category theory. The advantage of this point of view over the previous one was that we can collect all the information about the operations themselves together with the axioms they are subject to, into a finite product preserving functor. In particular the definition was given as follows:

A Lawvere theory is a small category $L$ with finite products, together with a strict finite-product preserving identity-on-objects functor $I:\aleph_0^{op} \to L$, where $\aleph_0$ is a skeleton of the category of finite sets.

We think of the arrows of a Lawvere theory as the collection of operations in a theory, and in particular, we think the hom-sets $L(n,1)$ as the collections of the n-ary operations we can define. Lawvere theories, together with finite-product preserving commuting triangles between them, form a category $\mathit{Law}$. Moreover, $\mathit{Law}$ has coproducts given by the quotient of the disjoint union of the operations of two Lawvere theories, over their equational axioms.

Examples of algebraic structures are in this case described as models of a specific Lawvere theory $L$. That is, finite-product preserving functors $M:L \to C$, to any category $C$ with finite products, among which $\mathit{Set}$ is of primary interest. In their turn, models together with natural transformations between them form a category $\mathit{Mod}(L,C)$. We will talk more about the semantics of a Lawvere theory later on, when we will make the connection to monads. For the moment, we will restrict ourselves to describing a symmetric monoidal structure on $Law$:

Let $L$ and $L'$ be two Lawvere theories. Their tensor product $L \otimes L'$ will contain any operations $f:n \to m$ and $f': n' \to m'$ of $L$ and $L'$ respectively, subject to the following equations:

$$\begin{matrix} n\times n' & \overset{n \times f'}{\longrightarrow} & n \times m' \\ {}_{f \times n'}\downarrow && \downarrow_{f \times m'} \\m \times n' & \underset{m \times f'}{\longrightarrow} & m \times m'. \\ \end{matrix}$$

The unit of the monoidal structure is given by the so called theory of an object, i.e. the category $\aleph_0^{op}$ itself, considered as a Lawvere theory with the identity functor. An interesting aspect of the tensor product of two Lawvere theories is the behaviour of its models. One can prove that the models of the tensor product $L \otimes L'$ in any categroy $C$ with finite products are equivalent, with respect to the underlying set functor given by the evaluation at 1, to the models of $L$ in the category $\mathit{Mod}(L',C)$. The last can be applied to the Lawvere theory of a group, in order to show that its tensor product with itself is isomorphic to the Lawvere theory of an Abelian group.

Monads and their connection to Lawvere theories

The motivation for formulating universal algebra in terms of monads can be found in the well known “Categories for the Working Mathematician”. It was the observation of Eilenberg and Moore, back in 1965, of the fact that the category of algebras of the monad that arises from the free group functor, is exactly the category of groups. Three years after Lawvere’s thesis was submitted, Linton made the connection to monads as follows:

• On the one hand, for any given Lawvere theory $L$, the underlying set functor $U_L:\mathit{Mod}(L,\mathit{Set}) \to \mathit{Set}$, given by $M \mapsto M(1)$, had been proven by Lawvere to have a left adjoint. This adjunction will give rise to a monad $T_L$ on $Set$. Linton showed that the category $\mathit{Mod}(L,Set)$ of models in $Set$ is equivalent to the category of $T_L$-algebras.

• On the other hand, if we consider any monad $T$ on $Set$, one can prove that the opposite of the Kleisli category $\mathit{Kl}(T)$ becomes a Lawvere theory by restricting to the category $\aleph_0^{op}$ the finite-product preserving canonical functor $\mathit{Set}^{op} \rightarrow \mathit{Kl}(T)^{op}$.

Moreover, both of these mappings turn out to be functorial. We can observe that if we start with a Lawvere theory $L$ and consider its monad $T_L$, then the Lawvere theory $\mathit{Kl}(T_L)^{op}$ is isomorphic to $L$ in $\mathit{Law}$. By that, we can consider $\mathit{Law}$ as a full subcategory of the category of monads, whose inclusion functor has a right adjoint.

Which approach is better?

History showed that category theorists favored the one in terms of monads. However there are a few drawbacks to that approach. For instance, there is an equivalence of categories between the category of monads on $\mathit{Set}$ and the category of large Lawvere theories, i.e. locally small categories with a strict identity-on-objects product preserving functor from the opposite of a skeleton of $\mathit{Set}$. This encompasses monads without rank, which do not preserve all $\kappa$-filtered colimits for any cardinal $\kappa$. This is due do the fact that while we are able to introduce a notion of sum between Lawvere theories (given by their coproduct), as well as a notion of a tensor product, we cannot necessarily do the same for monads without rank, which means that we are moving away from the “algebraic nature” of Lawvere theories.

Thus, why did monads gain prominence over Lawvere theories in understanding unversal algebra? Here are some possible explanations:

1. While we can consider monads over a general category and then study $\mathit{Set}$ as an example of primary interest, Lawvere theories require some notion of finiteness, which does not exist in general. One could use the notion of locally finitely presentable categories but this did not exist until some years later.
2. It would be easier to visualize earlier a generalisation of Lawvere theories in terms of enriched categories, however this area of category theory was not yet widely developed. It was only after the early 80s that we could define Lawvere theories enriched in a locally finitely presentable monoidal closed category $V$ and consider its models as $V$-functors.
3. Concepts in categorical logic that appear to be closely related to Lawvere theories came to light much later.

Computational effects and universal algebra

Another significant use of monads came from computer science and specifically by Eugenio Moggi’s PhD thesis defense under the supervision of Plotkin in 1987. Moggi introduced his notions of computations and he wanted to give a general semantics of them by using mathematical theory. The actual formulation came a couple of years later, when he used monads to describe computational effects. An alternative suggestion to unify computational effects, related though to the previous one, came in 2002 by Hyland, Plotkin and Power, and it was in terms of Lawvere theories. The argument will become clearer by the use of an example:

Consider a finite set of values $\mathit{Val}$ and a finite set of locations $\mathit{Loc}$. Then the side-effects Lawvere theory $L_S$, when $S=\mathit{Val}^{\mathit{Loc}}$, is the free Lawvere theory generated by the operations $\mathit{lookup}:\mathit{Val} \to \mathit{Loc}$ and $\mathit{update}:1\to \mathit{Loc} \times \mathit{Val}$, as it was defined in Notions of Computation Determine Monads, by Plotkin and Power. Then the underlying set functor $U:\mathit{Mod}(L_S,Set) \to \mathit{Set}$, given by evaluation at $1$, will give rise to a monad, which in its turn, coincides with Moggi’s side effect monad $(S\times -)^S$. An interesting result relative to the one for the tensor product of the Lawvere theory of a group is the following: The side-effects theory for $S=\mathit{Val}^{\mathit{Loc}}$ is the $\mathit{Loc}$-fold tensor product of the side-effects theory for $S=\mathit{Val}$.

Around this time, Hyland, Plotkin and Power, motivated by observations like the above, showed that computational effects can be regarded as instance of universal algebra. However continuations are an exception to that. This is due to the fact that the continuations monad has no rank so it doesn’t really fit into the setting of Lawvere theories, for the reasons discussed above. This indicates a fruitful area for future work.