# Lawvere Categories as Composed PROPs

Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi

► To cite this version:

Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi. Lawvere Categories as Composed PROPs. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.11-32, 10.1007/978-3-319-40370-0_3 . hal-01446031

HAL Id: hal-01446031

https://inria.hal.science/hal-01446031

Submitted on 25 Jan 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
Lawvere theories as composed PROPs

Filippo Bonchi¹, Pawel Sobocinski², and Fabio Zanasi³

¹ CNRS, École Normale Supérieure de Lyon, France

² University of Southampton, United Kingdom

³ Radboud University Nijmegen, The Netherlands

**Abstract.** PROPs and Lawvere theories are related notions adapted to the study of algebraic structures borne by an object in a category, but whereas PROPs are symmetric monoidal, Lawvere theories are cartesian. This paper formulates the connection between the two notions using Lack's technique for composing PROPs via distributive laws. We show Lawvere theories can be seen as resulting from a distributive law of two PROPs — one expressing the algebraic structure in linear form and the other expressing the ability of copying and discarding variables.

# 1 Introduction

PROPs [28] are symmetric monoidal categories with objects the natural numbers. In the last two decades, they have become increasingly popular as an environment for the study of diagrammatic formalisms from diverse branches of science in a compositional, resource sensitive fashion. Focussing on computer science, they have recently featured in algebraic approaches to Petri nets [11, 35], bigraphs [12], quantum circuits [15], and signal flow graphs [5, 7, 1, 20].

PROPs describe both the syntax and the semantics of diagrams, with the interpretation expressed as a PROP morphism [[·]]: **Syntax** → **Semantics**. Typically, **Syntax** is freely generated by a signature Σ of operations with arbitrary arity/coarity and can be composed sequentially and in parallel. Thus diagram syntax—which we refer to as Σ-terms—is inherently 2-dimensional: the term structure is that of directed acyclic graphs, rather than trees, as in the familiar case of operations with coarity 1. A crucial aspect is *linearity*: variables in Σ-terms cannot be copied nor discarded.

It is often useful to axiomatise the equivalence induced by [[·]] by means of a set of equations $E$, and then study the theory $(\Sigma, E)$. For PROPs, completeness proofs typically provide a serious challenge, involving the retrieval of a normal form for Σ-terms modulo $E$. The difficulty can be drastically reduced by exploiting certain operations on PROPs: an example of this modular methodology is provided by [5, 7], where the PROP operations of sum and composition are crucial for giving a sound and complete axiomatization of signal flow diagrams.

Sum is just the coproduct in the category of PROPs. Whenever two PROPs $T_1$ and $T_2$ can be presented by the theories $(\Sigma_1, E_1)$ and $(\Sigma_2, E_2)$, then their sum $T_1 + T_2$ is presented by the disjoint union $(\Sigma_1 \uplus \Sigma_2, E_1 \uplus E_2)$.
Composition of PROPs is more subtle, as it requires certain compatibility conditions between the structure of $\mathcal{T}_1$ and $\mathcal{T}_2$. Lack [25] describes this operation formally by means of distributive laws, seeing PROPs as monads in the 2-categorical sense of Street [36]. In a nutshell, a distributive law $\lambda: \mathcal{T}_1; \mathcal{T}_2 \to \mathcal{T}_2$; $\mathcal{T}_1$ of PROPs is a recipe for moving arrows of $\mathcal{T}_1$ past those of $\mathcal{T}_2$. The resulting PROP $\mathcal{T}_2$; $\mathcal{T}_1$ enjoys a factorisation property: every arrow in $\mathcal{T}_2$; $\mathcal{T}_1$ decomposes as one of $\mathcal{T}_2$ followed by one of $\mathcal{T}_1$. The graph of $\lambda$ can be seen as a set of directed equations $E_\lambda := (\xrightarrow{\in \mathcal{T}_1}, \xrightarrow{\mathcal{T}_2}) \approx (\xrightarrow{\mathcal{T}_2}, \xrightarrow{\mathcal{T}_1})$ and $\mathcal{T}_2$; $\mathcal{T}_1$ is presented by the theory $(\Sigma_1 \uplus \Sigma_2, E_1 \uplus E_2 \uplus E_\lambda)$.

This work uses distributive laws of PROPs to characterise Lawvere categories$^4$, a well known class of structures adapted to the study of categorical universal algebra. The essential difference with PROPs is that Lawvere categories express cartesian theories $(\Sigma, E)$, i.e. where $\Sigma$ only features operations with coarity 1 and $E$ may include non-linear equations. Our starting observation is that the Lawvere category $\mathcal{L}_\Sigma$ on a cartesian signature $\Sigma$ exhibits a factorisation property analogous to the one of composed PROPs: arrows can always be decomposed as $\xrightarrow{\in \mathcal{C}m} \xrightarrow{\in \mathcal{T}_\Sigma}$, where $\mathcal{C}m$ is the PROP of commutative comonoids, generated by a copy $1 \to 2$ and a discard $1 \to 0$ operation, and $\mathcal{T}_\Sigma$ is the PROP freely generated by $\Sigma$. This factorisation represents cartesian $\Sigma$-terms by their syntactic tree — the $\mathcal{T}_\Sigma$-part — with the possibility of explicitly indicating variable-sharing among sub-terms — the $\mathcal{C}m$-part. This simple observation leads us to the main result of the paper: for any cartesian signature $\Sigma$, there is a distributive law of PROPs $\lambda: \mathcal{T}_\Sigma$; $\mathcal{C}m \to \mathcal{C}m$; $\mathcal{T}_\Sigma$ which is presented by equations that express the naturality of copier and discarder; the resulting composed PROP $\mathcal{C}m$; $\mathcal{T}_\Sigma$ is the Lawvere category $\mathcal{L}_\Sigma$.

By a quotient construction on distributive laws, it follows immediately that the above theorem holds more generally for any cartesian theory $(\Sigma, E)$ where the set of axioms $E$ only contains linear equations. For instance the Lawvere category of commutative monoids $\mathcal{L}_{\mathcal{M}n}$ can be obtained by means of PROP composition, while the one $\mathcal{L}_{\mathcal{G}r}$ of abelian groups cannot, because of the non-linear axiom $x \times x^{-1} = 1$. Obviously, one can still formulate $\mathcal{L}_{\mathcal{G}r}$ as the quotient of the composite $\mathcal{L}_{\mathcal{M}n}$ by adding this equation, see Example 4.6 below.

As a side remark, we observe that, by taking the sum $\mathcal{C}m + \mathcal{T}_\Sigma$, rather than the composition, we are able to capture a different, well-known representation for cartesian $\Sigma$-terms, namely *term graphs*, which are acyclic graphs labeled over $\Sigma$. With respect to the standard tree representation, the benefit of term graphs is that the sharing of any common sub-term can be represented explicitly, making them particularly appealing for efficient rewriting algorithms, see e.g. [34] for a survey on the subject. As shown in [16], $\Sigma$-term graphs are in 1-1 correspondence with the arrows of the free *gs-monoidal category* generated by $\Sigma$, a concept that actually amounts to forming the sum of PROPs $\mathcal{C}m + \mathcal{T}_\Sigma$. Thus the only

<footnote n="4">⁴ Usually called Lawvere theories in the literature: i.e. finite product categories with set of objects the natural numbers, where product on objects is addition [27, 23]. In order to keep the exposition uniform, we reserve the word *theory* for presentations and refer to the presentation $(\Sigma, E)$ of a Lawvere theory as a *cartesian theory*.</footnote>
difference between term graphs and the representation of terms given by $\mathbf{Cm}$; $\mathcal{T}_\Sigma$ is in the validity of naturality of copier and discarder. Intuitively, a term where a resource is explicitly copied is not identified with the term where two copies appear separately: in short, copying is not natural.

*Related Works.* The motto “cartesian terms = linear terms + copying and discarding” inspired several papers exploiting the role of $\mathbf{Cm}$ in Lawvere categories, see e.g. [14, 26, 16]. In our work, Lawvere categories feature as a distinguished example of a construction, PROP composition, that is increasingly important in many recent research threads [6, 5, 20, 32]. The significance of this exercise is two-fold. First, it gives a deeper understanding of the nature of Lawvere categories and how they formally relate to PROPs, by showing the provenance of the natural copy-discard structure. Second, our result provides a canonical means of defining a distributive law for freely generated PROPs, showing that the result of composition is a familiar algebraic notion and enjoys a *finite* axiomatisation.

The following construction, reported by Baez in [2], is close in spirit to our work. There is pseudo-adjunction between symmetric monoidal and categories with finite products

<figure><img src="image_2.png" /></figure>

where $R$ is the evident forgetful functor and $L$ adds to any object of $\mathbb{C} \in \mathbf{SMCat}$ a natural copy-discard structure: natural diagonals and projections. Baez [2] states an equivalence between $RL(\mathbb{C})$ and $\mathbb{C} \otimes \mathbf{Cm}$, with the tensor $\otimes$ defined by $\mathbf{SMCat}[\mathbb{C}_1 \otimes \mathbb{C}_2, \mathbb{C}_3] \simeq \mathbf{SMCat}[\mathbb{C}_1, \mathbf{SMCat}[\mathbb{C}_2, \mathbb{C}_3]]$. Indeed, our main construction, as well as being a distributive law, is also an instance of a tensor or Kronecker product of symmetric monoidal theories; a concept that has been explored in some detail in the cartesian setting of Lawvere theories, see e.g. [22].

Our work restricts attention to PROPs $\mathcal{T}_\Sigma \in \mathbf{SMCat}$ freely generated by a cartesian signature $\Sigma$: in this case, it is enough to add a copy-discard structure for the object 1 and $RL(\mathcal{T}_\Sigma)$ coincides with PROP composition $\mathbf{Cm}$; $\mathcal{T}_\Sigma$. Our perspective exploiting distributive laws has the advantage of providing a *finite* presentation in terms of the naturality axioms.

It is also worth mentioning that the relationship between symmetric monoidal and cartesian structures is central in the categorical semantics of linear logic; in this perspective, the presence of $\mathbf{Cm}$ allows to interpret the structural rules of contraction and weakening — see e.g. [24, 30].

*Prerequisites and notation.* We assume familiarity with the basics of category theory (see e.g. [29, 10]), the definition of symmetric strict monoidal category [29, 33] (often abbreviated as SMC) and of bicategory [10, 3]. We write $f$; $g$: $a \to c$ for composition of $f$: $a \to b$ and $g$: $b \to c$ in a category $\mathbb{C}$, and $\mathbb{C}[a, b]$ for the hom-set of arrows $a \to b$. It will be sometimes convenient to indicate an arrow $f: a \to b$ of $\mathbb{C}$ as $x \xrightarrow{f \in \mathbb{C}} y$ or also $\xrightarrow{\in \mathbb{C}}$, if names are immaterial. For $\mathbb{C}$ an SMC, $\oplus$ is its monoidal product, with unit object $I$, and $\sigma_{a,b}: a \oplus b \to b \oplus a$ is the symmetry associated with $a, b \in \mathbb{C}$.
$$ 
\begin{array}{l}
(t_1; t_3) \oplus (t_2; t_4) = (t_1 \oplus t_2); (t_3 \oplus t_4) \\
(t_1; t_2); t_3 = t_1; (t_2; t_3) \quad \text{id}_n; c = c = c; \text{id}_m \\
(t_1 \oplus t_2) \oplus t_3 = t_1 \oplus (t_2 \oplus t_3) \quad \text{id}_0 \oplus t = t = t \oplus \text{id}_0 \\
\sigma_{1,1}; \sigma_{1,1} = \text{id}_2 \quad (t \oplus \text{id}_z); \sigma_{m,z} = \sigma_{n,z}; (\text{id}_z \oplus t)
\end{array}
$$

<caption>Fig. 1. Axioms of symmetric strict monoidal categories for a PROP $\mathcal{T}$.</caption>

## 2 PROPs

Our exposition is founded on symmetric monoidal theories: specifications for algebraic structures borne by objects in a symmetric monoidal category.

**Definition 2.1.** A (one-sorted) symmetric monoidal theory (SMT) is a pair $(\Sigma, E)$ consisting of a signature $\Sigma$ and a set of equations $E$. The signature $\Sigma$ is a set of generators $o: n \to m$ with arity $n$ and coarity $m$. The set of $\Sigma$-terms is obtained by composing generators in $\Sigma$, the unit $id: 1 \to 1$ and the symmetry $\sigma_{1,1}: 2 \to 2$ with ; and $\oplus$. This is a purely formal process: given $\Sigma$-terms $t: k \to l$, $u: l \to m$, $v: m \to n$, one constructs new $\Sigma$-terms $t$; $u: k \to m$ and $t \oplus v: k + n \to l + n$. The set $E$ of equations contains pairs $(t, t': n \to m)$ of $\Sigma$-terms with the same arity and coarity.

The categorical concept associated with symmetric monoidal theories is the notion of PROP (product and permutation category [28]).

**Definition 2.2.** A PROP is a symmetric strict monoidal category with objects the natural numbers, where $\oplus$ on objects is addition. Morphisms between PROPs are strict symmetric identity-on-objects monoidal functors: PROPs and their morphisms form the category PROP. We call a sub-PROP a sub-category of a PROP which is also a PROP; i.e. the inclusion functor is a PROP morphism.

The PROP $\mathcal{T}$ freely generated by an SMT $(\Sigma, E)$ has as its set of arrows $n \to m$ the set of $\Sigma$-terms $n \to m$ taken modulo the laws of symmetric strict monoidal categories — Fig. 1 — and the smallest congruence (with respect to ; and $\oplus$) containing the equations $t = t'$ for any $(t, t') \in E$.

There is a natural graphical representation for arrows of a PROP as string diagrams, which we now sketch, referring to [33] for the details. A $\Sigma$-term $n \to m$ is pictured as a box with $n$ ports on the left and $m$ ports on the right. Composition via $;$ and $\oplus$ are rendered graphically by horizontal and vertical juxtaposition of boxes, respectively.

$$ t; s \text{ is drawn } \boxed{t} \Box \boxed{s} \quad t \oplus s \text{ is drawn } \boxed{t} \Box \boxed{s}. \qquad (1) $$

In any SMT there are specific $\Sigma$-terms generating the underlying symmetric monoidal structure: these are $id_1: 1 \to 1$, represented as $\Box$, the symmetry $\sigma_{1,1}: 1 + 1 \to 1 + 1$, represented as $\Box\Box$, and the unit object for $\oplus$, that is,
$id_0: 0 \to 0$, whose representation is an empty diagram $\square$. Graphical representation for arbitrary identities $id_n$ and symmetries $\sigma_{n,m}$ are generated according to the pasting rules in (1).

**Example 2.3.**

(a) We write $(\Sigma_M, E_M)$ for the SMT of commutative monoids. The signature $\Sigma_M$ contains a multiplication $\otimes: 2 \to 1$ and a unit $\circ: 0 \to 1$. Equations $E_M$ assert associativity (A1), commutativity (A2) and unitality (A3).

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A1)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A2)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A3)

We call $Mn$ the PROP freely generated by the SMT $(\Sigma_M, E_M)$.

(b) We also introduce the SMT $(\Sigma_C, E_C)$ of cocommutative comonoids. The signature $\Sigma_C$ consists of a comultiplication $\otimes: 1 \to 2$ and a counit $\circ: 1 \to 0$. $E_C$ is the following set of equations.

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A4)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A5)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A6)

We call $Cm$ the PROP freely generated by $(\Sigma_C, E_C)$. Modulo the white vs. black colouring, string diagrams of $Cm$ can be seen as those of $Mn$ “reflected about the $y$-axis”. This observation yields $Cm \cong Mn^{op}$.

(c) The PROP $B$ of (commutative/cocommutative) bialgebras is generated by the theory $(\Sigma_M \uplus \Sigma_C, E_M \uplus E_C \uplus B)$, where $B$ is the following set of equations.

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A7)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A8)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A9)

$$ \begin{tikzpicture} \node[draw, shape=circle, inner sep=1.5pt] at (0,0) {}; \node[draw, shape=circle, inner sep=1.5pt] at (0,1) {}; \node at (0,0.5) {$=$}; \node at (0,1.5) {}; \end{tikzpicture} $$

(A10)

**Remark 2.4 (Models of a PROP).** The assertion that $(\Sigma_M, E_M)$ is the SMT of commutative monoids—and similarly for other SMTs appearing in our exposition—can be made precise using the notion of *model* (sometimes also called *algebra*) of a PROP. Given a strict symmetric monoidal category $\mathcal{C}$, a model of a PROP $\mathcal{T}$ in $\mathcal{C}$ is a symmetric strict monoidal functor $\mathcal{F}: \mathcal{T} \to \mathcal{C}$. Then $\text{LinMod}(\mathcal{T}, \mathcal{C})$ is the category of models of $\mathcal{T}$ in $\mathcal{C}$ and natural transformations between them.

Turning to commutative monoids, there is a category Monoid($\mathcal{C}$) whose objects are the commutative monoids in $\mathcal{C}$, i.e., objects $x \in \mathcal{C}$ equipped with arrows $x \oplus x \to x$ and $I \to x$, satisfying the usual equations. Given any model $\mathcal{F}: Mn \to \mathcal{C}$, it follows that $\mathcal{F}(1)$ is a commutative monoid in $\mathcal{C}$: this yields a functor $\text{LinMod}(Mn, \mathcal{C}) \to \text{Monoid}(\mathcal{C})$. Saying that $(\Sigma_M, E_M)$ is the SMT of commutative monoids means that this functor is an equivalence natural in $\mathcal{C}$. We shall not focus on models as they are not central in our developments and refer the reader to [19, 25] for more information.
Example 2.3 only shows PROPs freely generated from an algebraic specification. However, one can also define PROPs in a more direct manner, without relying on SMTs. Two basic examples will be useful for our exposition:

- the PROP F whose arrows $n \to m$ are functions from $\bar{n}$ to $\bar{m}$, where $\bar{n} = \{0, 1, \dots, n-1\}$.

- the PROP P whose arrows $n \to m$ exist only if $n = m$, in which case they are the permutations on $\bar{n}$.

This kind of definition is often useful as a different, more concrete perspective on PROPs that arise from symmetric monoidal theories. For instance, F is *presented* by the theory of commutative monoids, in the sense that F and Mn are isomorphic PROPs: once can consider a string diagram $t \in Mn[n, m]$ as the graph of a function of type $\{1, \dots, n\} \to \{1, \dots, m\}$. For instance, $\mathcal{D} \bullet \oplus \mathcal{D} \bullet : 2 \to 2$ describes the function $f: \{1, 2\} \to \{1, 2\}$ mapping both elements to 1. By duality, $\mathrm{Cm} \cong \mathrm{F}^{\mathrm{op}}$, that is, $\mathrm{F}^{\mathrm{op}}$ is presented by the theory of commutative comonoids.

Similarly, P provides a concrete description of the theory $(\emptyset, \emptyset)$ with empty signature and no equations. It is the initial object in the category **PROP**.

## 3 PROP composition

A basic operation on SMTs $(\Sigma, E)$ and $(\Sigma', E')$ is to take their sum $(\Sigma \uplus \Sigma', E \uplus E')$. In **PROP**, the PROP generated by $(\Sigma \uplus \Sigma', E \uplus E')$ is the coproduct $\mathcal{T} + \mathcal{S}$ of the PROP $\mathcal{T}$ generated by $(\Sigma, E)$ and $\mathcal{S}$, generated by $(\Sigma', E')$.

The sum $\mathcal{T}+\mathcal{S}$ is the least interesting way of combining theories, because there are no equations that express compatibility between the algebraic structures in $\mathcal{T}$ and $\mathcal{S}$. This is a standard pattern in algebra: e.g. a ring is given by a monoid and an abelian group, subject to equations that ensure that the former distributes over the latter. Similarly, the equations of bialgebras (Example 2.3) describe the interplay of a monoid and a comonoid. Ordinary functions, which can always be decomposed as a surjection followed by an injection, are another example.

In [25] Lack shows how these phenomena can be uniformly described as the operation of composing PROPs. The conceptual switch is to understand PROPs as monads, and their composition as a distributive law. These monads live in a certain bicategory [3], as in the classical work by Street [36]<fnref n="5" />.

**Definition 3.1.** A monad on an object $x$ of a bicategory $\mathfrak{B}$ is a 1-cell $\mathcal{F}: x \to x$ with 2-cells $\eta^{\mathcal{F}}: \mathrm{id}_x \to \mathcal{F}$ and $\mu^{\mathcal{F}}: \mathcal{F} \to \mathcal{F}$ (called the unit and the multiplication respectively) making the following diagrams—in which we suppress the associativity isomorphisms—commute.

<footnote n="5">⁵ Actually, Street worked in a 2-category, but the same theory can be developed in any bicategory with the obvious, minor modifications [25, §3.1].</footnote>
commute.

<figure><img src="image_3.png" /></figure>

A distributive law $\lambda: \mathcal{F}; \mathcal{G} \to \mathcal{G}; \mathcal{F}$ yields a monad $\mathcal{G}; \mathcal{F}$ with the following unit and multiplication:

$$ \begin{align} \eta^{\mathcal{G}; \mathcal{F}} & : \mathrm{id} \xrightarrow{\eta^{\mathcal{F}}} \mathcal{F} \xrightarrow{\eta^{\mathcal{G}; \mathcal{F}}} \mathcal{G}; \mathcal{F} \tag{7} \\ \mu^{\mathcal{G}; \mathcal{F}} & : \mathcal{G}; \mathcal{F}; \mathcal{G}; \mathcal{F} \xrightarrow{\mathcal{G}\lambda\mathcal{F}} \mathcal{G}; \mathcal{G}; \mathcal{F}; \mathcal{F} \xrightarrow{\mu^{\mathcal{G}; \mathcal{F}}\mathcal{F}} \mathcal{G}; \mathcal{F}; \mathcal{F} \xrightarrow{\mathcal{G}\mu^{\mathcal{F}}} \mathcal{G}; \mathcal{F} \end{align} $$

Let us verify how the abstract definition works for the case of categories. Pick categories $\mathcal{C}$ and $\mathcal{D}$ with the same set $Ob$ of objects, seen as monads $Ob \stackrel{\mathrm{dom}_{\mathcal{C}}}{\leftarrow}$ $Ar_{\mathcal{C}} \stackrel{\mathrm{cod}_{\mathcal{C}}}{\rightarrow}$ $Ob$ and $Ob \stackrel{\mathrm{dom}_{\mathcal{D}}}{\leftarrow}$ $Ar_{\mathcal{D}} \stackrel{\mathrm{cod}_{\mathcal{D}}}{\rightarrow}$ $Ob$ in $\mathrm{Span}(\mathcal{Set})$. A distributive law $\lambda: \mathcal{C}; \mathcal{D} \to \mathcal{D}; \mathcal{C}$ is a span morphism

<figure><img src="image_4.png" /></figure>

mapping composable pairs $a \stackrel{\in\mathcal{C}}{\rightarrow} \stackrel{\in\mathcal{D}}{\rightarrow} b$ to composable pairs $a \stackrel{\in\mathcal{D}}{\rightarrow} \stackrel{\in\mathcal{C}}{\rightarrow} b$. As described in (7), $\lambda$ allows to define a monad structure on $\mathcal{D}; \mathcal{C}$. That means, $\lambda$ yields a category $\mathcal{D}; \mathcal{C}$ whose arrows $a \to b$ are composable pairs $a \stackrel{\in\mathcal{D}}{\rightarrow} \stackrel{\in\mathcal{C}}{\rightarrow} b$ of arrows of $\mathcal{D}, \mathcal{C}$ and composition is defined as

$$ (a \xrightarrow{f \in \mathcal{D}} g \in \mathcal{C}) ; (b \xrightarrow{f' \in \mathcal{D}} g' \in \mathcal{C}) := (a \xrightarrow{f \in \mathcal{D}} \lambda(\xrightarrow{g \in \mathcal{C}} \xrightarrow{f' \in \mathcal{D}} g') \xrightarrow{g' \in \mathcal{C}} c). $$

PROPs are understood as monads in the same sense that small categories are. The difference is that one needs to refine the bicategory of interest, in order for the composition of PROPs-monads to yield another PROP-monad and not an arbitrary small category. These refinements are in two steps. First, one takes the bicategory $\mathrm{Span}(\mathrm{Mon})$ whose 1-cells are spans in the category of *monoids*, instead of sets. This accounts for the monoidal structure — in fact, monads in $\mathrm{Span}(\mathrm{Mon})$ are small strict monoidal categories. The second refinement has
the purpose of correctly accounting for the symmetry structure of PROPs: one takes the bicategory $\mathbf{Bimod}(\mathbf{Span}(\mathbf{Mon}))$ whose objects are small strict monoidal categories and 1-cells are the *bimodules* in $\mathbf{Span}(\mathbf{Mon})$. PROPs are then monads on the object P of $\mathbf{Bimod}(\mathbf{Span}(\mathbf{Mon}))$.

We shall gloss over further details about the exact formalisation of this observation, as it is out of the scope of this paper — we refer to [25] and [37, § 2.4] for the detailed definitions. The simpler setting of composition of mere categories should provide enough guidance to follow the rest of our exposition.

It is important for our purposes to remark how composition works for PROPs $\mathcal{T}_1, \mathcal{T}_2$ generated by SMTs, say $(\Sigma_1, E_1)$ and $(\Sigma_2, E_2)$. The PROP $\mathcal{T}_1; \mathcal{T}_2$ induced by a distributive law $\lambda: \mathcal{T}_2; \mathcal{T}_1 \to \mathcal{T}_1; \mathcal{T}_2$ will also enjoy a presentation by generators and equations, consisting of the sum $(\Sigma_1 \uplus \Sigma_2, E_1 \uplus E_2)$ plus the equations $E_\lambda$ arising from the distributive law. The set $E_\lambda$ is simply the graph of $\lambda$, now seen as a set of directed equations $(\varepsilon_{\mathcal{T}_2} \to \varepsilon_{\mathcal{T}_1}) \approx (\varepsilon_{\mathcal{T}_1} \to \varepsilon_{\mathcal{T}_2})$ telling how $\Sigma_2$-terms modulo $E_2$ distribute over $\Sigma_1$-terms modulo $E_1$. In fortunate cases, it is possible to present $E_\lambda$ by a simpler, or even finite, set of equations, thus giving a sensible axiomatisation of the compatibility conditions expressed by $\lambda$. This is the case for both examples considered below.

*Example 3.3.*

(a) The PROP $\mathbf{F}$ of functions can be described as the composite of PROPS for surjections and injections. Let $\mathbf{In}$ be the PROP whose arrows $n \to m$ are injective functions from $\bar{n}$ to $\bar{m}$. The PROP $\mathbf{Su}$ of surjective functions is defined analogously. There is a distributive law $\lambda: \mathbf{In}; \mathbf{Su} \to \mathbf{Su}; \mathbf{In}$ defined by epi-mono factorisation: it maps a composable pair $\xrightarrow{\varepsilon_{\mathbf{In}}} \varepsilon_{\mathbf{Su}} \xrightarrow{\varepsilon_{\mathbf{In}}} \mathbf{In}$ to a composable pair $\xrightarrow{\varepsilon_{\mathbf{Su}}} \varepsilon_{\mathbf{In}} \xrightarrow{\varepsilon_{\mathbf{In}}} \mathbf{In}$ [25]. The resulting PROP $\mathbf{Su}; \mathbf{In}$ is isomorphic to $\mathbf{F}$ because any function in $\mathbf{F}$ can be uniquely factorised (up-to permutation) as a surjection followed by an injection. In more syntactic terms, using the isomorphism $\mathbf{F} \cong \mathbf{Mn}$, this result says that $\mathbf{Mn}$ is the composite $\mathbf{Mu}; \mathbf{Un}$, where $\mathbf{Mu} \cong \mathbf{Su}$ is the PROP freely generated by the SMT $\{\boxed{\cdot}\}, \{(A1), (A2)\})$ and $\mathbf{Un} \cong \mathbf{In}$ by the SMT $\{\boxed{\cdot}, \emptyset\}$. The distributive law $\lambda: \mathbf{In}; \mathbf{Su} \to \mathbf{Su}; \mathbf{In}$ is then presented by the remaining equation (A3) of $\mathbf{Mn}$, which indeed describes how the generator $\boxed{\cdot}$ of $\mathbf{Un}$ can be moved past the one $\boxed{\cdot}$ of $\mathbf{Mu}$.

(b) The composition of $\mathbf{Cm}$ and $\mathbf{Mn}$ yields the PROP $\mathbf{B}$ of commutative bialgebras. First, because $\mathbf{Mn} \cong \mathbf{F}$ and $\mathbf{Cm} \cong \mathbf{F}^{\mathrm{op}}$, we can express a distributive law $\lambda: \mathbf{Mn}; \mathbf{Cm} \to \mathbf{Cm}; \mathbf{Mn}$ as having the type $\mathbf{F}; \mathbf{F}^{\mathrm{op}} \to \mathbf{F}^{\mathrm{op}}; \mathbf{F}$. This amounts to saying that $\lambda$ maps $\mathbf{cospans} \ n \xrightarrow{f \in \mathbf{F}} \xleftarrow{g \in \mathbf{F}} m$ to $\mathbf{spans} \ n \xleftarrow{p \in \mathbf{F}} \xrightarrow{q \in \mathbf{F}} m$. Defining this mapping via (chosen) pullback in $\mathbf{F}$ satisfies the conditions of distributive laws [25]. One can now read the equations arising by the distributive
law from pullback squares in F. For instance:

<figure><img src="image_5.png" /></figure>

where the second diagram is obtained from the pullback by applying the isomorphisms $F \cong \mathbf{Mn}$ and $F^{op} \cong \mathbf{Cm}$. In fact, Lack [25] shows that the equations presenting $\mathbf{Cm}$; $\mathbf{Mn}$ arise from (those of $\mathbf{Cm}+\mathbf{Mn}$ and) just four pullback squares, yielding equations (A7)-(A10). Therefore, $\mathbf{Cm}$; $\mathbf{Mn}$ is isomorphic to the PROP B of bialgebras encountered in Example 2.3. Furthermore, these PROPs have a “concrete” descriptions as $F^{op}$; F. In the terminology of [3], one can see $F^{op}$; F as the *classifying category* of the bicategory *Span*(*F*), obtained by identifying the isomorphic 1-cells and forgetting the 2-cells.

There is a tight relationship between distributive laws and factorisation systems. Distributive laws of small categories are in 1-1 correspondence with so-called *strict factorisation systems* [31], in which factorisations must be specified uniquely on the nose, rather than merely up-to isomorphism. Distributive laws of PROPs correspond instead to a more liberal kind of factorisation system, for which decompositions are up-to permutation. As this perspective will be useful later, we recall the following result from Lack [25].

**Proposition 3.4** ([25], **Theorem 4.6**). Let $\mathcal{S}$ be a PROP and $\mathcal{T}_1, \mathcal{T}_2$ be sub-PROPs of $\mathcal{S}$. Suppose that each arrow $n \xrightarrow{f \in \mathcal{S}} m$ can be factorised as $n \xrightarrow{g_1 \in \mathcal{T}_1} \xrightarrow{g_2 \in \mathcal{T}_2} m$ uniquely up-to permutation, that is, for any other decomposition $n \xrightarrow{h_1 \in \mathcal{T}_1} \xrightarrow{h_2 \in \mathcal{T}_2} m$ of $f$, there exists permutation $p \xrightarrow{p \in \mathcal{P}}$ such that the following diagram commutes.

<figure><img src="image_6.png" /></figure>

Then there exists a distributive law $\lambda: \mathcal{T}_2; \mathcal{T}_1 \to \mathcal{T}_1; \mathcal{T}_2$, defined by associating to a composable pair $\xrightarrow{f \in \mathcal{T}_2} \xrightarrow{g \in \mathcal{T}_1} \mathcal{T}_2$ the factorisation of $f$; $g$, yielding $\mathcal{S} \cong \mathcal{T}_1; \mathcal{T}_2$.

## Quotient of a distributive law

Definition 3.1 introduced the notion of *quotient* $\theta: \mathcal{F} \to \mathcal{G}$ of a monad $\mathcal{F}$: the idea is that the monad $\mathcal{G}$ is obtained by imposing additional equations on the algebraic theory described by $\mathcal{F}$. As one may expect, distributive laws are compatible with monad quotients, provided that the law preserves the newly added equations. This folklore result appears in various forms in the literature: [9] gives it for distributive laws of endofunctors over monads and [4, 8] for distributive laws of monads. All these references concern distributive laws in **Cat**. For our purposes, it is useful to state the result for arbitrary bicategories.
a Lawvere category is required to be a category with finite products — henceforth called a cartesian category, a PROP may carry any symmetric monoidal structure, not necessarily cartesian.

Just as PROPs, Lawvere categories can be also freely obtained by generators and equations. By analogy with symmetric monoidal theories introduced in § 2, we organise this data as a cartesian theory: it simply amounts to the notion of equational theory that one typically finds in universal algebra, see e.g. [13].

**Definition 4.1.** A (one-sorted) cartesian theory $(\Sigma, E)$ consists of a signature $\Sigma = \{o_1: n_1 \to 1, \dots, o_k: n_k \to 1\}$ and a set $E$ of equations between cartesian $\Sigma$-terms, which are defined as follows:

- for each $i \in \mathbb{N}$, the variable $x_i$ is a cartesian term;

- suppose $o: n \to 1$ is a generator in $\Sigma$ and $t_1, \dots, t_n$ are cartesian terms. Then $o(t_1, \dots, t_n)$ is a cartesian term.

The Lawvere category $\mathcal{L}_{(\Sigma,E)}$ freely generated by $(\Sigma, E)$ is the category whose objects are the natural numbers and arrows $n \to m$ are lists $\langle t_1, \dots, t_m \rangle$ of cartesian $\Sigma$-terms quotiented by $E$, such that, for each $t_i$, only variables among $x_1, \dots, x_n$ appear in $t_i$. Composition is by substitution:

$$ \left( n \xrightarrow{\langle t_1, \dots, t_m \rangle} m \right); \left( m \xrightarrow{\langle s_1, \dots, s_z \rangle} z \right) = n \xrightarrow{\langle s_1[t_i/x_i|1 \le i \le m], \dots, s_z[t_i/x_i|1 \le i \le m] \rangle} z $$

where $t[t'/x]$ denotes the cartesian term $t$ in which all occurrences of the variable $x$ have been replaced with $t'$.

$\mathcal{L}_{(\Sigma,E)}$ is equipped with a product $\times$ which is defined on objects by addition and on arrows by list concatenation and suitable renaming of variables:

$$ \left( n \xrightarrow{\langle t_1, \dots, t_m \rangle} m \right) \times \left( z \xrightarrow{\langle s_1, \dots, s_l \rangle} l \right) \\ = n + z \xrightarrow{\langle t_1, \dots, t_m, s_1[x_{i+m}/x_i|1 \le i \le l], \dots, s_l[x_{i+m}/x_i|1 \le i \le l] \rangle} m + l. $$

We use notation $\mathrm{ovar}(t)$ for the list of occurrences of variables appearing (from left to right) in $t$ and, more generally, $\mathrm{ovar}(t_1, \dots, t_m)$ for the list $\mathrm{ovar}(t_1) :: \dots :: \mathrm{ovar}(t_m)$. Also, $|l| \in \mathbb{N}$ denotes the length of a list $l$. We say that a list $\langle t_1, \dots, t_m \rangle: n \to m$ is linear if each variable among $x_1, \dots, x_n$ appears exactly once in $\mathrm{ovar}(t_1, \dots, t_m)$.

Our first observation is that Lawvere categories are PROPs.

**Proposition 4.2.** $\mathcal{L}_{(\Sigma,E)}$ is a PROP.

*Proof.* Let $\times$ act as the monoidal product, 0 as its unit and define the symmetry $n+m \to m+n$ as the list $\langle x_{n+1}, \dots, x_{n+m}, x_1, \dots, x_n \rangle$. It follows that $\mathcal{L}_{(\Sigma,E)}$ equipped with this structure satisfies the laws of symmetric strict monoidal categories, thus it is a PROP.

As a side observation, note that the unique PROP morphism $\mathbf{P} \to \mathcal{L}_{(\Sigma,E)}$ given by initiality of $\mathbf{P}$ in **PROP** sends $p: n \to n$ to $\langle x_{p^{-1}(1)}, \dots, x_{p^{-1}(n)} \rangle$.
**Remark 4.3.** In spite of Proposition 4.2, cartesian theories are not a subclass of symmetric monoidal theories: in fact, the two concepts are incomparable. On the one hand, a symmetric monoidal theory $(\Sigma, E)$ is cartesian if and only if all generators in $\Sigma$ have coarity 1 and, for all equations $t = s$ in $E$, $t$ and $s$ are $\Sigma$-terms with coarity 1. Under these conditions, there is a canonical way to interpret any $\Sigma$-term $n \to m$ as a list of $m$ cartesian $\Sigma$-terms on variables $x_1, \dots, x_n$. Below, $o$ ranges over $\Sigma$:

$$ \boxplus : 1 \to 1 \mapsto \langle x_1 \rangle $$

$$ \boxminus : 2 \to 2 \mapsto \langle x_2, x_1 \rangle $$

$$ \boxed{\mathbf{o}} : n \to 1 \mapsto \langle o(x_1, \dots, x_n) \rangle. $$

The inductive cases are defined using the operations $\boxplus$ and $\boxminus$ on lists given in Definition 4.1. Note that $\Sigma$-terms always denote (lists of) linear cartesian terms. This explains why, conversely, not all the cartesian theories are symmetric monoidal: their equations possibly involve non-linear $\Sigma$-terms, which are not expressible with (symmetric monoidal) $\Sigma$-terms. The subtlety here is that, in a sense, we can still simulate a cartesian theory on signature $\Sigma$ with a symmetric monoidal theory, which however will be based on a larger signature $\Sigma'$, recovering the possibility of copying and discarding variables by the use of additional generators. This point will become more clear below, where we will see how copier and discharger, i.e., the cartesian structure, can be mimicked with the use of the PROP Cm.

**Example 4.4.** The SMT $(\Sigma_M, E_M)$ of commutative monoids is cartesian. It generates the Lawvere category $\mathcal{L}_{\Sigma_M, E_M}$ whose arrows $n \to m$ are lists $\langle t_1, \dots, t_m \rangle$ of elements of the free commutative monoid on $\{x_1, \dots, x_n\}$.

The example of commutative monoids is particularly instructive for sketching our approach to Lawvere categories as composed PROPs. First, note that the Lawvere category $\mathcal{L}_{\Sigma_M, E_M}$ includes the PROP Mn freely generated by $(\Sigma_M, E_M)$. Indeed, any string diagram of Mn can be interpreted as a list of terms following the recipe of Remark 4.3. For instance,

$$ \text{diagram} : 4 \to 3 \text{ is interpreted as } \langle \boxed{\mathbf{o}}(x_2, \boxed{\mathbf{o}}(x_1, x_3)), x_4, \boxed{\mathbf{o}} \rangle : 4 \to 3 $$

As we observed above, string diagrams of Mn can only express linear terms. What makes $\mathcal{L}_{\Sigma_M, E_M}$ more general than Mn is the ability to copy and discard variables. Indeed, just as any monoidal category in which $\oplus$ is the cartesian product, $\mathcal{L}_{\Sigma_M, E_M}$ comes equipped with canonical choices of a “copy” and “discard” operation

$$ \text{copy}(n) := \langle x_1, \dots, x_n, x_1, \dots, x_n \rangle : n \to 2n \quad \text{dsc}(n) := \langle \rangle : n \to 0 \quad n \in \mathbb{N} $$

natural in $n$, which satisfy some expected equations: copying is commutative and associative; copying and then discarding is the same as not doing anything — see e.g. [18, 14].
How can we mimic the copy and discard structure in the language of PROPs?
First, for each $n > 1$ one can define $cpy(n)$ and $dsc(n)$ in terms of $cpy(1)$ and $dsc(1)$, which can therefore be regarded as the only fundamental operations$^7$.
Also, the equations that they satisfy can be synthesised as saying that $cpy(1)$ acts as the comultiplication and $dsc(1)$ as the counit of a commutative comonoid on 1. Therefore, they are none other than the generators of the PROP $Cm$:

$$ \text{[C]: } 1 \to 2 $$

$$ \text{[D]: } 1 \to 0. $$

Our approach suggests that a copy of $Mn$ and of $Cm$ “live” inside $\mathcal{L}_{\Sigma_M, E_M}$. We claim that these two PROPs provide a complete description of $\mathcal{L}_{\Sigma_M, E_M}$, that means, any arrow of $\mathcal{L}_{\Sigma_M, E_M}$ can be presented diagrammatically by using $Mn$ and $Cm$. For instance,

$$ \langle \text{[D]} | (x_2, \text{[D]} | (x_1, x_4)), x_1, \text{[D]} | \rangle : 4 \to 3 \text{ corresponds to } \text{[Cm]} : 4 \to 3 $$

Observe that the diagram is of the factorised form $\xrightarrow{\in Cm} \xrightarrow{\in Mn}$. Intuitively, $Cm$ is deputed to model the interplay of variables — in this case, the fact that $x_1$ is copied and $x_3$ is deleted — and $Mn$ describes the syntactic tree of the terms. Of course, to claim that this factorisation is always possible, we need additional equations to model composition of factorised diagrams. For instance:

$$ \langle \text{[D]} | (x_1, x_2), x_1 \rangle ; \langle x_1, \text{[D]} | (x_1, x_2) \rangle = \langle \text{[D]} | (x_1, x_2), \text{[D]} | (\text{[D]} | (x_1, x_2), x_1) \rangle $$

<figure><img src="image_7.png" /></figure>

<figure><img src="image_8.png" /></figure>

≡

<figure><img src="image_9.png" /></figure>

The second equality holds if we assume the equation (A8) of the SMT of bialgebra-bras. Thus the example suggests that composition by substitution in $\mathcal{L}_{\Sigma_M, E_M}$ can be mimicked at the diagrammatic level by allowing the use of bialgebra equations, which as we know from Example 3.3.(b) present the composite PROP $Cm$; $Mn$. Therefore, the conclusive conjecture of our analysis is that $\mathcal{L}_{\Sigma_M, E_M}$ must be isomorphic to $Cm$; $Mn$ and can be presented by equations (A1)-(A10).

We now generalise and make formal the above approach. Our main result is the following.

**Theorem 4.5.** Suppose that $(\Sigma, E)$ is an SMT which is also cartesian and let $T_{(\Sigma, E)}$ be its freely generated PROP. Then $\mathcal{L}_{(\Sigma, E)} \cong Cm$; $T_{(\Sigma, E)}$, where distributive law $T_{(\Sigma, E)}$; $Cm \to Cm$; $T_{(\Sigma, E)}$ yielding $\mathcal{L}_{(\Sigma, E)}$ is presented by equations

<footnote>$^7$ For $n = 0$, both operations are equal to the identity on 0.</footnote>
<figure><img src="image_10.png" /></figure>

for each $o \in \Sigma$.

Before moving to the proof of Theorem 4.5, we show its significance by revisiting some well-known theories in terms of our result.

### Example 4.6.

(a) If we instantiate Theorem 4.5 to the theory $(\Sigma_M, E_M)$ of commutative monoids (Example 2.3), then (Lw1)-(Lw2) are the bialgebra equations (A7)-(A10). The result that $B \cong \mathrm{Cm}$; $\mathrm{Mn}$ (Example 3.3.(b)) is now an immediate consequence of Theorem 4.5 and tells us that the Lawvere category of commutative monoids can be considered as the PROP of bialgebras.

(b) In the case of monoids, the resulting Lawvere category is precisely a composite PROP, because all the equations only affect the linear part of the theory, that means, the generating cartesian theory is also an SMT. As observed in Remark 4.3, this is not true in general: for instance, the cartesian theory $(\Sigma_G, E_G)$ of abelian groups extends the one $(\Sigma_M, E_M)$ of commutative monoids with an inverse operation $\llbracket \cdot \rrbracket: 1 \to 1$ and a non-linear equation $\llbracket \circ \circ \rrbracket(x, \llbracket \cdot \rrbracket(x)) = \llbracket \circ \circ \rrbracket$. In such cases, Theorem 4.5 still yields useful information about the structure of the resulting Lawvere category. For instance, it means that $\mathcal{L}_{(\Sigma_G, E_G)}$ is isomorphic to the PROP $\mathrm{Cm}$; $\mathcal{T}_{(\Sigma_G, E_M)}$ quotiented by the above non-linear equation, which is rendered in string diagrams as:

<figure><img src="image_11.png" /></figure>

Interestingly, the result of this quotient is isomorphic to the PROP of integer matrices, see e.g. [37, §3.5] and its models in a symmetric monoidal category are the *Hopf algebras* [17], with $\llbracket \cdot \rrbracket$ playing the role of the antipode.

(c) In [21] Fritz presents the category of finite sets and probabilistic maps using generators and equations. The resulting Lawvere category $\mathcal{L}_{\mathrm{Prob}}$ can be decomposed following the scheme of Theorem 4.5: there is a linear part $(\Sigma_P, E_P)$ of the theory — given by binary convex combinations $\Sigma_P = \{\llbracket \lambda \rrbracket: 2 \to 1 \mid \lambda \in [0, 1]\}$ and suitable associativity and commutativity laws in $E_P$, a commutative comonoid structure, and the two interact according to (Lw1)-(Lw2). This interaction yields a composite PROP $\mathrm{Cm}$; $\mathcal{T}_{(\Sigma_P, E_P)}$ which, quotiented by non-linear equations $\llbracket 0 \rrbracket = \llbracket \bullet \rrbracket$ and $\llbracket \lambda \rrbracket = \llbracket \cdot \rrbracket$, yields $\mathcal{L}_{\mathrm{Prob}}$.<fnref n="8" />

<footnote n="8">⁸ In fact, the Lawvere category in [21] has finite coproducts, while our $\mathcal{L}_{\mathrm{Prob}}$ is based on finite products. This is just a matter of co-/contra-variant presentation of the same data: one can switch between the two by “vertical rotation” of diagrams.</footnote>
**Remark 4.7.** It is instructive to observe how Theorem 4.5 translates to models of theories. We recalled what is a model for a PROP in Remark 2.4; there is an analogous notion for Lawvere categories. A model for a Lawvere category $\mathcal{L}_{(\Sigma,E)}$ is a cartesian category $\mathbb{C}$ together with a cartesian (i.e., finite-products preserving) functor $\mathcal{L}_{(\Sigma,E)} \to \mathbb{C}$: models of $\mathcal{L}_{(\Sigma,E)}$ in $\mathbb{C}$ and natural transformations between them form a category $\text{CartMod}(\mathcal{L}_{(\Sigma,E)}, \mathbb{C})$. Now, for $(\Sigma, E)$ and $\mathcal{T}_{(\Sigma,E)}$ as in Theorem 4.5, we have that models of $\mathcal{L}_{(\Sigma,E)}$ in $\mathbb{C}$ cartesian are the same as models of $\mathcal{T}_{(\Sigma,E)}$ in $\mathbb{C}$, now seen more abstractly as a symmetric monoidal category. That means, there is an equivalence $\text{LinMod}(\mathcal{T}_{(\Sigma,E)}, \mathbb{C}) \simeq \text{CartMod}(\mathcal{L}_{(\Sigma,E)}, \mathbb{C})$.

The rest of the section is devoted to proving Theorem 4.5. First we observe that, by the following lemma, it actually suffices to check our statement for SMTs with no equations. This reduction has just the purpose of making computations in $\mathcal{L}_{(\Sigma,E)}$ easier, by working with terms instead of equivalence classes.

**Lemma 4.8.** If the statement of Theorem 4.5 holds in the case $E = \emptyset$, then it holds for any cartesian SMT $(\Sigma, E)$.

*Proof.* Let $(\Sigma, E)$ be a cartesian SMT and $\mathcal{T}_{\Sigma}$, $\mathcal{T}_{(\Sigma,E)}$ be the PROPs freely generated, respectively, by $(\Sigma, \emptyset)$ and $(\Sigma, E)$. By assumption, Theorem 4.5 holds for $(\Sigma, \emptyset)$, yielding a distributive law $\lambda: \mathcal{T}_{\Sigma}$; $\text{Cm} \to \text{Cm}$; $\mathcal{T}_{\Sigma}$. A routine check shows that $\lambda$ preserves the equations of $E$, whence Proposition 3.6 gives a distributive law $\lambda'$: $\mathcal{T}_{(\Sigma,E)}$; $\text{Cm} \to \text{Cm}$; $\mathcal{T}_{(\Sigma,E)}$ with the required properties.

In the sequel, let us abbreviate $\mathcal{L}_{\Sigma, \emptyset}$ as $\mathcal{L}_{\Sigma}$. By virtue of Lemma 4.8, we shall prove Theorem 4.5 for $\mathcal{L}_{\Sigma}$ and by letting $\mathcal{T}_{\Sigma}$ be the PROP freely generated by $(\Sigma, \emptyset)$. We shall obtain the distributive law $\mathcal{T}_{\Sigma}$; $\text{Cm} \to \text{Cm}$; $\mathcal{T}_{\Sigma}$ from the recipe of Proposition 3.4, by showing that any arrow of $\mathcal{L}_{\Sigma}$ decomposes as $\xrightarrow{\in\text{Cm}} \xrightarrow{\in\mathcal{T}_{\Sigma}}$.

We now give some preliminary lemmas that are instrumental for the definition of the factorisation and the proof of the main result. We begin by showing how string diagrams of $\text{Cm}$ and $\mathcal{T}_{\Sigma}$ are formally interpreted as arrows of $\mathcal{L}_{\Sigma}$.

**Lemma 4.9.**

- $\text{Cm}$ is the sub-PROP of $\mathcal{L}_{\Sigma}$ whose arrows are lists of variables. The inclusion of $\text{Cm}$ in $\mathcal{L}_{\Sigma}$ is the morphism $\Phi: \text{Cm} \to \mathcal{L}_{\Sigma}$ defined on generators of $\text{Cm}$ by

$$ \bullet \quad \mapsto \langle x_1, x_1 \rangle: 1 \to 2 \qquad \bullet \quad \mapsto \langle \rangle: 0 \to 1. $$

- $\mathcal{T}_{\Sigma}$ is the sub-PROP of $\mathcal{L}_{\Sigma}$ whose arrows are linear terms. The inclusion of $\mathcal{T}_{\Sigma}$ in $\mathcal{L}_{\Sigma}$ is the morphism $\Psi: \mathcal{T}_{\Sigma} \to \mathcal{L}_{\Sigma}$ defined on generators of $\mathcal{T}_{\Sigma}$ by

$$ \bullet \quad \mapsto \langle o(x_1, \dots, x_n) \rangle: n \to 1 \qquad (o: n \to 1) \in \Sigma. $$

*Proof.* First, it is immediate to verify that lists of variables are closed under composition, monoidal product and include all the symmetries of $\mathcal{L}_{\Sigma}$: therefore, they form a sub-PROP. The same holds for linear terms.
We now consider the first statement of the lemma. There is a 1-1 correspondence between arrows $n \xrightarrow{f \in \mathcal{L}_{\Sigma}} m$ that are lists of variables and functions $\overline{m} \to \overline{n}$: the function for $f$ maps $k$, for $1 \le k \le m$, to the index $l$ of the variable $x_l$ appearing in position $k$ in $f$. This correspondence yields an isomorphism between the sub-PROP of $\mathcal{L}_{\Sigma}$ whose arrows are lists of variables and $F^{op}$. Composing this isomorphism with $\mathrm{Cm} \stackrel{\sim}{\to} F^{op}$ yields $\Phi$ as in the statement of the lemma.

For the second statement, faithfulness is immediate by the fact that arrows of $\mathcal{T}_{\Sigma}$ are $\Sigma$-terms modulo the laws of SMCs, with no additional equations. One can easily verify that $\Psi: \mathcal{T}_{\Sigma} \to \mathcal{L}_{\Sigma}$ identifies the linear terms in $\mathcal{L}_{\Sigma}$ following the observations in Remark 4.3.

Henceforth, for the sake of readability we shall not distinguish between $\mathrm{Cm}$ and the isomorphic sub-PROP of $\mathcal{L}_{\Sigma}$ identified by the image of $\Phi$, and similarly for $\mathcal{T}_{\Sigma}$ and $\Psi$. Lemma 4.9 allows us to use $\mathcal{L}_{\Sigma}$ as an environment where $\mathrm{Cm}$ and $\mathcal{T}_{\Sigma}$ interact. The following statement guarantees the soundness of the interaction described by (Lw1)-(Lw2).

**Lemma 4.10.** Equations (Lw1) and (Lw2) are sound in $\mathcal{L}_{\Sigma}$.

*Proof.* We first focus on (Lw1). Following the isomorphisms of Lemma 4.9, $\overline{[O]} \in \mathcal{T}_{\Sigma}[n, 1]$ is interpreted as the arrow $\langle o(x_1, \dots, x_n) \rangle \in \mathcal{L}_{\Sigma}[n, 1]$ and $\overline{\bullet} \in \mathrm{Cm}[0, 1]$ as $\langle \rangle \in \mathcal{L}_{\Sigma}[1, 0]$. The left-hand side of (Lw1) is then the composite $\langle o(x_1, \dots, x_n) \rangle$; $\langle \rangle \in \mathcal{L}_{\Sigma}[n, 0]$. Therefore, the left- and right-hand side of (Lw1) are the same arrow of $\mathcal{L}_{\Sigma}$.

It remains to show soundness of (Lw2). Following Lemma 4.9, the left-hand side $\overline{[O]}$; $\overline{\bullet}$ is interpreted in $\mathcal{L}_{\Sigma}$ as $\langle o(x_1, \dots, x_n) \rangle; \langle x_1, x_1 \rangle$ and the right-hand side as $\langle x_1, \dots, x_n, x_1, \dots, x_n \rangle; \langle o(x_1, \dots, x_n), o(x_{n+1}, \dots, x_{n+n}) \rangle$. By definition, both composites are equal to $\langle o(x_1, \dots, x_n), o(x_1, \dots, x_n) \rangle$ in $\mathcal{L}_{\Sigma}$. Therefore, (Lw2) is also sound in $\mathcal{L}_{\Sigma}$.

It is useful to observe that (Lw1)-(Lw2) allows us to copy and discard not only the generators but arbitrary string diagrams of $\mathcal{T}_{\Sigma}$.

**Lemma 4.11.** Suppose $\overline{[d]}$ is a string diagram of $\mathcal{T}_{\Sigma}$. Then the following holds in $\mathcal{T}_{\Sigma} + \mathrm{Cm}$ quotiented by (Lw1)-(Lw2).

$$ \text{diagram} = \text{diagram} \quad (\text{Lw3}) $$

$$ \text{diagram} = \text{diagram} \quad (\text{Lw4}) $$

*Proof.* The proof is by induction on $\overline{[d]}$. For (Lw3), the base cases of $\Box$ and $\Box\Box$ follow by the laws of SMCs (Figure 1). The base case of $\overline{[O]}$, for $o$ a generator in $\Sigma$, is given by (Lw2). The inductive cases of composition by $+$ and $\oplus$ immediately follow by induction hypothesis. The proof of (Lw4) is analogous.

We can now show the factorisation lemma.
**Lemma 4.12.** Any arrow $n \xrightarrow{f \in \mathcal{L}_{\Sigma}} m$ has a factorisation $n \xrightarrow{\hat{c} \in \mathbf{Cm}} \xrightarrow{\hat{d} \in \mathcal{T}_{\Sigma}} m$ which is unique up-to permutation.

*Proof.* Since the cartesian theory generating $\mathcal{L}_{\Sigma}$ has no equations, $n \xrightarrow{f} m$ is just a list of cartesian $\Sigma$-terms $\langle t_1, \dots, t_m \rangle$. The factorisation consists in replacing all variables appearing in $\langle t_1, \dots, t_m \rangle$ with fresh ones $x_1, \dots, x_z$, so that no repetition occurs: this gives us the second component of the decomposition as a list of linear terms $z \xrightarrow{\hat{d} \in \mathcal{T}_{\Sigma}} m$. The first component $\hat{c}$ will be the list $n \xrightarrow{\mathrm{ovar}(t_1, \dots, t_m) \in \mathbf{Cm}} z$ of variables originally occurring in $f$, so that post-composition with $\hat{d}$ yields $\langle t_1, \dots, t_m \rangle$. It is simple to verify uniqueness up-to permutation of this factorisation.

We now have all the ingredients to conclude the proof of our main statement.

*Proof* (Theorem 4.5). Using the conclusion of Lemma 4.12, Proposition 3.4 gives us a distributive law $\lambda: \mathcal{T}_{\Sigma}; \mathbf{Cm} \to \mathbf{Cm}; \mathcal{T}_{\Sigma}$ such that $\mathcal{L}_{\Sigma} \cong \mathbf{Cm}; \mathcal{T}_{\Sigma}$. It remains to show that (Lw1)-(Lw2) allow to prove all the equations arising from $\lambda$. By Proposition 3.4, $\lambda$ maps a composable pair $n \xrightarrow{d \in \mathcal{T}_{\Sigma}} \xrightarrow{c \in \mathbf{Cm}} m$ to the factorisation $n \xrightarrow{c' \in \mathbf{Cm}} \xrightarrow{d' \in \mathcal{T}_{\Sigma}} m$ of $d$; $c$ in $\mathcal{L}_{\Sigma}$, calculated according to Lemma 4.12. The corresponding equation generated by $\lambda$ is $d$; $c = c'$; $d'$, with $d, c, c'$, $d'$ now seen as string diagrams of $\mathcal{T}_{\Sigma} + \mathbf{Cm}$. The equational theory of $\mathcal{L}_{\Sigma} \cong \mathbf{Cm}; \mathcal{T}_{\Sigma}$ consists of all the equations arising in this way plus those of $\mathcal{T}_{\Sigma} + \mathbf{Cm}$. What we need to show is that

the string diagrams $d$; $c$ and $c'$; $d'$ are equal modulo the equations of $\mathcal{T}_{\Sigma} + \mathbf{Cm}$ and (Lw1)-(Lw2).

Since our factorisation is unique up-to permutation, it actually suffices to show a weaker statement, namely that

there exists a factorisation $n \xrightarrow{c'' \in \mathbf{Cm}} \xrightarrow{d'' \in \mathcal{T}_{\Sigma}} m$ of $d$; $c$ in $\mathcal{L}_{\Sigma}$ such that the string diagrams $d$; $c$ and $c''$; $d''$ are equal modulo the equations of $\mathcal{T}_{\Sigma} + \mathbf{Cm}$ and (Lw1)-(Lw2).

Statement (‡) implies (†) because, by uniqueness of the factorisation $c'$; $d'$ up-to permutation, there exists $p \in \mathbf{P}$ such that $d' = p$; $d''$ and $c'' = c'$; $p$ in $\mathcal{L}_{\Sigma}$. Since $p$ is an arrow of both sub-PROPs $\mathcal{T}_{\Sigma}$ and $\mathbf{Cm}$, the first equality also holds in $\mathcal{T}_{\Sigma}$ and the second in $\mathbf{Cm}$. So $c'$; $d' = c'$; $p$; $d'' = c''$; $d''$ in $\mathcal{T}_{\Sigma} + \mathbf{Cm}$.

Therefore, we turn to a proof of (‡). We describe a procedure to transform the string diagram $\xrightarrow{d \in \mathcal{T}_{\Sigma}} \xrightarrow{c \in \mathbf{Cm}}$ into the form $\xrightarrow{c'' \in \mathbf{Cm}} \xrightarrow{d'' \in \mathcal{T}_{\Sigma}}$ by only using the equations in $\mathcal{T}_{\Sigma} + \mathbf{Cm}$ plus (Lw1)-(Lw2). Lemmas 4.9 and 4.10 guarantee that $d$; $c = c''$; $d''$ as arrows of $\mathcal{L}_{\Sigma}$.

1. First, there is a preparatory step in which we move all symmetries to the outmost part of the string diagram $d$; $c$, to ease the application of (Lw1)-(Lw2). By definition, $d$ only contains components of the kind $\overline{[O]}$: $k \to 1$,
for $o \in \Sigma$, $\text{[D]}: 2 \to 2$ and $\text{[C]}: 1 \to 1$. Using naturality (Fig. 1), we can
move all symmetries $\text{[D]}$ to the left of components $\text{[O]}$.

<figure><img src="image_12.png" /></figure>

The result is a string diagram $p$; $\bar{d}$; $c'$, where $p$ only contains components $\text{[D]}$ and $\text{[C]}$ — i.e., it is a string diagram of $\mathcal{P}$ — and $\bar{d}$ is a string diagram of $\mathcal{T}_{\Sigma}$ where $\text{[D]}$ does not appear.

<figure><img src="image_13.png" /></figure>

We then perform a symmetric transformation on the string diagram $c$. By definition, $c$ contains components $\text{[C]}: 1 \to 2$, $\text{[C]}: 0 \to 1$, $\text{[D]}: 2 \to 2$ and $\text{[C]}: 1 \to 1$. By naturality, we can move all symmetries $\text{[D]}$ to the right of any component $\text{[C]}$ and $\text{[C]}$.

<figure><img src="image_14.png" /></figure>

<figure><img src="image_15.png" /></figure>

The result is a string diagram $p$; $\bar{d}$; $\bar{c}$; $p'$, where $\bar{c}$ is a string diagram of $\text{Cm}$ in which $\text{[D]}$ does not appear and $p'$ is a string diagram of $\mathcal{P}$.

<figure><img src="image_16.png" /></figure>

2. We now make $\bar{d}$ and $\bar{c}$ interact. First note that, since $\bar{d}$ does not contain $\text{[D]}$ and all generators $o \in \Sigma$ have coarity 1, $\bar{d}$ must the $\oplus$-product $\bar{d}_1 \oplus \dots \oplus \bar{d}_z$ of string diagrams $\bar{d}_i: k_i \to 1$ of $\mathcal{T}_\Sigma$.

<figure><img src="image_17.png" /></figure>

For analogous reasons, $\bar{c}$ is also a $\oplus$-product $\bar{c}_1 \oplus \dots \oplus \bar{c}_z$ where, for $1 \le i \le z$,

$$ \text{[D]}_{i} = \text{[D]}_{i}^{\prime} \quad \text{or} \quad \text{[C]}_{i} = \text{[C]}_{i}^{\prime}. \qquad (9) $$

We thus can present $\bar{c}$ as follows:

<figure><img src="image_18.png" /></figure>
We are now in position to distribute each $\bar{d}_i$ over the corresponding $\bar{c}_i$. Suppose first $\bar{c}_i$ satisfies the left-hand equality in (9). By assumption, all the equations of $\mathcal{T}_\Sigma + \text{Cm}$, (Lw1) and (Lw2) hold. Thus, by Lemma 4.11, also (Lw3) holds. Starting from $\bar{d}_i; \bar{c}_i$, we can iteratively apply (Lw3) to obtain a string diagram of shape $\xrightarrow{\in Cm} \xrightarrow{\in \mathcal{T}_\Sigma}$:

<figure><img src="image_19.png" /></figure>

In the remaining case, $\bar{c}_i$ satisfies the right-hand equality in (9). Then, one application of (Lw1) also gives us a string diagram of shape $\xrightarrow{\in Cm} \xrightarrow{\in \mathcal{T}_\Sigma}$.

$$ \xrightarrow{\phantom{\in Cm}} \left[ \bar{d}_i \right] \bullet \xrightarrow{\phantom{\in Cm}} $$

Applying the above transformations for each $\bar{d}_i; \bar{c}_i$ yields a string diagram of the desired shape $\xrightarrow{c'' \in Cm} \xrightarrow{d'' \in \mathcal{T}_\Sigma}$.

<figure><img src="image_20.png" /></figure>

Observe that all the transformations that we described only used equations in $\mathcal{T}_\Sigma + \text{Cm}$, (Lw1) and (Lw2). This concludes the proof of (‡) and thus of the main theorem.

*Acknowledgements* The first author acknowledge support by project ANR 12IS02001 PACE. The third author acknowledges support from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement n° 320571.
References

[1] Baez, J.C., Erbele, J.: Categories in control. CoRR abs/1405.6881 (2014)

[2] Baez, J.C.: Universal algebra and diagrammatic reasoning. Lecture (2006), http://math.ucr.edu/home/baez/universal/universal_hyper.pdf

[3] Bénabou, J.: Introduction to bicategories. In: Reports of the Midwest Category Seminar, Lecture Notes in Mathematics, vol. 47, pp. 1–77. Springer Berlin Heidelberg (1967)

[4] Bonchi, F., Milius, S., Silva, A., Zanasi, F.: Killing epsilons with a dagger — a coalgebraic study of systems with algebraic label structure. Theoretical Computer Science 604, 102–126 (2015)

[5] Bonchi, F., Sobocinski, P., Zanasi, F.: A categorical semantics of signal flow graphs. In: CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014. Proceedings. pp. 435–450 (2014)

[6] Bonchi, F., Sobocinski, P., Zanasi, F.: Interacting bialgebras are Frobenius. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. pp. 351–365 (2014)

[7] Bonchi, F., Sobocinski, P., Zanasi, F.: Full abstraction for signal flow graphs. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. pp. 515–526 (2015)

[8] Bonchi, F., Zanasi, F.: Bialgebraic semantics for logic programming. Logical Methods in Computer Science 11(1:14) (2015)

[9] Bonsangue, M.M., Hansen, H.H., Kurz, A., Rot, J.: Presenting distributive laws. In: Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013. Proceedings. pp. 95–109 (2013)

[10] Borceux, F.: Handbook of Categorical Algebra 1 – Basic Category Theory. Cambridge Univ. Press (1994)

[11] Bruni, R., Melgratti, H.C., Montanari, U.: A connector algebra for P/T nets interactions. In: CONCUR '11. pp. 312–326. Springer (2011)

[12] Bruni, R., Montanari, U., Plotkin, G.D., Terreni, D.: On hierarchical graphs: Reconciling bigraphs, gs-monoidal theories and gs-graphs. Fundam. Inform. 134(3-4), 287–317 (2014)

[13] Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer (1981)

[14] Burroni, A.: Higher dimensional word problems with applications to equational logic. Theor Comput Sci 115, 43–62 (1993)

[15] Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics 13(4), 043016 (2011)

[16] Corradini, A., Gadducci, F.: An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures 7(4), 299–331 (1999)

[17] Dascalescu, S., Nastasescu, C., Raianu, S.: Hopf Algebras, Pure and Applied Mathematics, vol. 235. Marcel Dekker, Inc., New York, Basel (2001), an Introduction

[18] Eilenberg, S., Kelly, G.M.: Closed categories. In: Proceedings of the Conference on Categorical Algebra. pp. 421–562. Springer (1966)

[19] Fiore, M.P., Campos, M.D.: The algebra of directed acyclic graphs. In: Abramsky Festschrift. LNCS, vol. 7860 (2013)

[20] Fong, B., Rapisarda, P., Sobociński, P.: A categorical approach to open & interconnected dynamical systems. CoRR/1510.05076 (2015)
[21] Fritz, T.: A presentation of the category of stochastic matrices. CoRR abs/0902.2554 (2009), http://arxiv.org/abs/0902.2554

[22] Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor Comput Sci 357(1-3), 70-99 (2006)

[23] Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science 172, 437-458 (2007)

[24] Jacobs, B.: Semantics of weakening and contraction. Annals of Pure and Applied Logic 69(1), 73-106 (1994)

[25] Lack, S.: Composing PROPs. Theor App Categories 13(9), 147-163 (2004)

[26] Lafont, Y.: Equational reasoning with 2-dimensional diagrams. In: Comon, H., Jounnaud, J.P. (eds.) Term Rewriting, Lecture Notes in Computer Science, vol. 909, pp. 170-195. Springer Berlin Heidelberg (1995)

[27] Lawvere, W.F.: Functorial Semantics of Algebraic Theories. Ph.D. thesis (2004)

[28] Mac Lane, S.: Categorical algebra. B Am Math Soc 71, 40-106 (1965)

[29] Mac Lane, S.: Categories for the Working Mathematician. Springer (1998)

[30] Melliès, P.A.: Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27, Société Mathématique de France 1196 (2009)

[31] Rosebrugh, R., Wood, R.: Distributive laws and factorization. Journal of Pure and Applied Algebra 175(13), 327-353 (2002), special Volume celebrating the 70th birthday of Professor Max Kelly

[32] Ross Duncan, K.D.: Interacting Frobenius algebras are Hopf. CoRR abs/1601.04964 (2016), http://arxiv.org/abs/1601.04964

[33] Selinger, P.: A survey of graphical languages for monoidal categories. Springer Lecture Notes in Physics 13(813), 289-355 (2011)

[34] Sleep, M.R., Plasmeijer, M.J., van Eekelen, M.C.J.D. (eds.): Term Graph Rewriting: Theory and Practice. John Wiley and Sons Ltd., Chichester, UK (1993)

[35] Sobociński, P., Stephens, O.: A programming language for spatial distribution of net systems. In: Petri Nets '14 (2014)

[36] Street, R.: The formal theory of monads. J Pure Appl Algebra 2(1), 243-265 (2002)

[37] Zanasi, F.: Interacting Hopf Algebras: the theory of linear systems. Ph.D. thesis, Ecole Normale Supérieure de Lyon (2015)