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

HAL
open science

# Coherent Presentations of Monoidal Categories

Pierre-Louis Curien, Samuel Mimram

► To cite this version:

Pierre-Louis Curien, Samuel Mimram. Coherent Presentations of Monoidal Categories. Logical Methods in Computer Science, 2017, 13 (3), pp.1-38. 10.23638/LMCS-13(3:31)2017. hal-01662524

HAL Id: hal-01662524

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

Submitted on 13 Dec 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# COHERENT PRESENTATIONS OF MONOIDAL CATEGORIES

PIERRE-LOUIS CURIEN<sup>a</sup> AND SAMUEL MIMRAM<sup>b</sup>

<sup>a</sup> Université Paris Diderot

e-mail address: curien@pps.univ-paris-diderot.fr

<sup>b</sup> École Polytechnique

e-mail address: samuel.mimram@lix.polytechnique.fr

**ABSTRACT.** Presentations of categories are a well-known algebraic tool to provide descriptions of categories by means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation, which is described by equational generators. When those form a convergent (abstract) rewriting system on objects, there are three very natural constructions that can be used to define the category which is described by the presentation: one consists in turning equational generators into identities (i.e. considering a quotient category), one consists in formally adding inverses to equational generators (i.e. localizing the category), and one consists in restricting to objects which are normal forms. We show that, under suitable coherence conditions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups, and we extend those conditions to presentations of monoidal categories.

## CONTENTS

<table><tr><td>1. Introduction</td><td>2</td></tr><tr><td>2. Presentations of categories modulo a rewriting system</td><td>4</td></tr><tr><td>2.1. Presentations of categories</td><td>4</td></tr><tr><td>2.2. Presentations modulo</td><td>5</td></tr><tr><td>2.3. Quotient and localization of a presentation modulo</td><td>6</td></tr><tr><td>3. Confluence properties</td><td>10</td></tr><tr><td>3.1. Residuation</td><td>10</td></tr><tr><td>3.2. The cylinder property</td><td>15</td></tr><tr><td>4. Comparing presented categories</td><td>17</td></tr><tr><td>4.1. The category of normal forms</td><td>17</td></tr><tr><td>4.2. Equivalence with the localization</td><td>18</td></tr><tr><td>4.3. Embedding into the localization</td><td>19</td></tr><tr><td>5. Coherent presentations of monoidal categories</td><td>20</td></tr><tr><td>5.1. Presentations of monoidal categories</td><td>20</td></tr><tr><td>5.2. Residuation in monoidal presentations</td><td>25</td></tr></table>

Key words and phrases: presentation of a category, quotient category, localization, residuation.

<figure><img src="image_3.png" /></figure>
5.3. The cylinder property 29

5.4. The coherence theorem 33

5.5. A variant of the cylinder property 34

6. Conclusion 37

References 37

# 1. INTRODUCTION

Motivated by the generalization of rewriting techniques to the setting of higher-dimensional categories, we introduce a notion of presentation of a monoidal category modulo a rewriting system, in order to be able to present a monoidal category as generated by objects and morphisms, quotiented by relations on both morphisms and objects. This work can somehow be seen as an extension of traditional techniques of rewriting modulo a theory [1]: the quotient on objects is described by a rewriting system, whose rules are called here *equational*, and we want to consider objects up to those rules. In order to handle this situation, there are mainly two possible approaches: either implicit (work on the equivalence classes modulo equational rules) or explicit (consider equational rules as invertible operations). We provide conditions on both the original rewriting system and the equational one, so that that the two approaches coincide. Namely, we show that they imply some form of *coherence* for the equational rewriting system, i.e. that there is essentially one way of transforming an object into another using the equational rules, thus implying that the quotient and the localization are equivalent. An important methodological point has to be stressed here: our aim is not to provide the most general conditions for this to hold, but sufficient conditions, which are applicable to a wide range of examples and can efficiently be checked on the presentation of a (monoidal or 2-) category.

Let us further expose our motivations, which come from higher-dimensional rewriting theory [17]. A *string rewriting system* $P$ consists in an alphabet $P_1$ and a set $P_2 \subseteq P_1^* \times P_1^*$ of rules. Such a system induces a monoid $\|P\| = P_1^*/\stackrel{*}{\Leftrightarrow}$ obtained by quotienting the free monoid $P_1^*$ on $P_1$ by the smallest congruence $\stackrel{*}{\Leftrightarrow}$ containing the rules in $P_2$; when the rewriting system is convergent, i.e. both confluent and terminating, normal forms provide canonical representatives of equivalence classes. Given a monoid $M$, we say that $P$ is a *presentation* of $M$ when $M$ is isomorphic to $\|P\|$; in this case, the elements of $P_1$ can be seen as *generators* for $M$, and the elements of $P_2$ as a complete set of *relations* for $M$. For instance, the additive monoid $\mathbb{N} \times \mathbb{N}$ admits the presentation $P$ with $P_1 = \{a, b\}$ and $P_2 = \{ba \Rightarrow ab\}$: namely, the string rewriting system is convergent, and its normal forms are words of the form $a^p b^q$, with $(p, q) \in \mathbb{N} \times \mathbb{N}$, from which it is easy to build the required isomorphism.

The notion of presentation is easy to generalize from monoids to categories (a monoid being the particular case of a category with one object): a presentation of category consists in generators for objects and morphisms, together with rules relating morphisms in the free category generated by the generators. Starting from this observation, the notion of presentation was generalized in order to present $n$-categories (computads [21, 19] or polygraphs [5]), thus providing us with a notion of *higher-dimensional rewriting system*. However for dimensions $n \ge 2$, this notion of presentation has important limitations. In particular, not every $n$-category admits a presentation. We shall illustrate this on a simple
example of a monoidal category (which is the particular case of a 2-category with only one 0-cell).

Consider the simplicial category $\Delta$ whose objects are natural numbers $p \in \mathbb{N}$ and morphisms $f : p \to q$ are monotone functions $f : [p] \to [q]$ where $[p]$ is the set $\{0, \dots, p-1\}$ considered as a finite poset with $0 < \dots < p-1$. This category is monoidal, with tensor product being given by addition on objects ($p \otimes q = p + q$) and by "juxtaposition" on morphisms, and it is well known that it admits the following presentation as a monoidal category [16, 14]: its objects are generated by one object $a$, its morphisms are generated by $m : a \otimes a \to a$ and $e : 0 \to a$, and the relations are

$$ \alpha : m \circ (m \otimes \mathrm{id}_a) = m \circ (\mathrm{id}_a \otimes m) \qquad \lambda : m \circ (e \otimes \mathrm{id}_a) = \mathrm{id}_a \qquad \rho : m \circ (\mathrm{id}_a \otimes e) = \mathrm{id}_a $$

This means that every morphism of $\Delta$ can be obtained as a composite of $e$ and $m$, and that two such formal composites represent the same morphism precisely when they can be related by the congruence generated by the above relations. As we can see on this example, a presentation $P$ of a monoidal category consists in generators for objects (here $P_1 = \{a\}$), generators for morphisms ($P_2 = \{e, m\}$) together with their source and target, and relations between composites of morphisms ($P_3 = \{\alpha, \lambda, \rho\}$) together with their source and target. Notice that such a presentation *does not allow for relations between objects*, and thus is restricted to presenting monoidal categories whose underlying monoid of objects is free.

This limitation can be better understood by trying to present the monoidal category $\Delta \times \Delta$ with tensor product extending componentwise the one of $\Delta$: the underlying monoid of objects is $\mathbb{N} \times \mathbb{N}$, which is not free. If we try to construct a presentation for this monoidal category, we are led to consider a presentation containing "two copies" of the previous presentation: we consider a presentation $P$ with $P_1 = \{a, b\}$ as object generators (where $a$ and $b$ respectively correspond to the objects $(1, 0)$ and $(0, 1)$), with $P_2 = \{m_a, e_a, m_b, e_b\}$ as morphism generators with

$$ m_a : a \otimes a \to a \qquad e_a : 0 \to a \qquad m_b : b \otimes b \to b \qquad e_b : 0 \to b $$

and with $P_3 = \{\alpha_a, \lambda_a, \rho_a, \alpha_b, \lambda_b, \rho_b\}$ as relations. If we stop here adding relations, the presented category has $\{a, b\}^*$ as underlying monoid of objects, i.e. the free product of $\mathbb{N}$ with itself, which is not right: recalling the above presentation for $\mathbb{N} \times \mathbb{N}$, we should moreover add a relation $g : ba = ab$. However, such a relation between objects is not allowed in the usual notion of presentation (where only relations between morphisms are considered). In order to provide a meaning to it, three constructions are available:

- restrict $P$ to some canonical representatives of objects modulo the equivalence generated by $g$ (typically the words of the form $a^p b^q$ with $(p, q) \in \mathbb{N} \times \mathbb{N}$),

- quotient by $g$ the monoidal category $\|P\|$ presented by $P$, or

- formally invert the morphism $g$ in $\|P\|$.

We show that under reasonable assumptions on the presentation, all three constructions coincide, thus providing a notion of *coherent presentation modulo*. In the article, we begin by studying the case of presentations modulo of categories and then generalize it to monoidal categories.

This article is based on the conference article [6], extending it on two major points. First, the assumptions on the opposite presentations turned out to be unnecessary (see the new proof of Theorem 4.5), making our conditions more natural, simpler to check and applicable to a wider range of presentations. Second, the extension to the case of presentations of monoidal categories is new.
We begin by recalling the notion of presentation of a category (Section 2.1), then we extend it to work modulo a relation on objects (Section 2.2), and consider the quotient and localization wrt to the relation (Section 2.3). In order to compare those constructions, we consider equational rewriting systems equipped with a notion of residuation (Section 3.1) and satisfying a particular “cylinder” property (Section 3.2). We then show that, under suitable coherence conditions, the category of normal forms is isomorphic to the quotient (Section 4.1) and equivalent with the localization (Section 4.2). The notion of presentation modulo is then generalized to monoidal categories (Section 5.1), as well as the residuation techniques (Section 5.2) and cylinder properties (Section 5.3), which finally allows us to generalize our coherence theorem to monoidal categories (Section 5.4).

This work was partially supported by CATHRE French ANR project ANR-13-BS02-0005-02. We would like to thank Florence Clerc for her contributions to the preliminary version of this work [6], as well as the anonymous referees for their insightful remarks leading to improvements of this article.

## 2. PRESENTATIONS OF CATEGORIES MODULO A REWRITING SYSTEM

**2.1. Presentations of categories.** Recall that a graph $(P_0, s_0, t_0, P_1)$ consists of two sets $P_0$ and $P_1$, of vertices and edges respectively, together with two functions $s_0, t_0 : P_1 \to P_0$ associating to an edge its source and target respectively:

$$P_0 \underset{t_0}{\overset{s_0}{\rightleftharpoons}} P_1$$

Such a graph generates a category with $P_0$ as objects and the set $P_1^*$ of (directed) paths as morphisms. If we denote by $i_1 : P_1 \to P_1^*$ the coercion of edges to paths of length 1, and $s_0^*, t_0^* : P_1^* \to P_0$ the functions associating to a path its source and target respectively, we thus obtain a diagram as on the left below:

$$\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    & P_1 & \\
    \mathcal{P}_0 \arrow[r, "s_0", "\searrow"] & \mathcal{P}_0 \arrow[r, "t_0", "\searrow"] \arrow[d, "i_1"] & P_1^* \\
    \mathcal{P}_0 \arrow[r, "t_0^*", "\swarrow"] & P_1^* \arrow[d, "i_1"] & \\
    & P_1 & \\
\end{tikzcd} \qquad (2.1)$$

in **Set** which is commuting, in the sense that $s_0^* \circ i_1 = s_0$ and $t_0^* \circ i_1 = t_0$.

**Definition 2.1.** A *presentation*

$$P = (P_0, s_0, t_0, P_1, s_1, t_1, P_2)$$

as pictured on the right of (2.1), consists in a graph $(P_0, s_0, t_0, P_1)$ as above, the elements of $P_0$ (resp. $P_1$) being called *object* (resp. *morphism*) *generators*, together with a set $P_2$ of *relations* (or *2-generators*) and two functions $s_1, t_1 : P_2 \to P_1^*$ satisfying the globular identities

$$s_0^* \circ s_1 = s_0^* \circ t_1 \qquad t_0^* \circ s_1 = t_0^* \circ t_1$$

The category $\|P\|$ presented by $P$ is the category obtained from the category generated by the graph $(P_0, s_0, t_0, P_1)$ by quotienting morphisms by the smallest congruence wrt composition identifying any two morphisms $f$ and $g$ such that there exists $\alpha \in P_2$ satisfying $s_1(\alpha) = f$ and $t_1(\alpha) = g$.
In the following, we often simply write $(P_0, P_1, P_2)$ for a presentation as above, leaving the source and target maps implicit. We write $f : x \to y$ for an edge $f \in P_1$ with $s_0(f) = x$ and $t_0(f) = y$, and $\alpha : f \Rightarrow g$ for a relation with $f$ as source and $g$ as target; the globular identities impose that $f$ and $g$ have the same source (resp. target). We sometimes write $\alpha : f \Leftrightarrow g$ to indicate that $\alpha : f \Rightarrow g$ or $\alpha : g \Rightarrow f$ is an element of $P_2$, and we denote by $\Leftrightarrow^*$ the smallest congruence such that $f \Leftrightarrow^* g$ whenever there exists $\alpha : f \Rightarrow g$ in $P_2$.

**Example 2.2.** The monoid $\mathbb{N}/2\mathbb{N}$ (seen as a category with only one object) admits the presentation $P$ with

$$P_0 = \{x\} \qquad P_1 = \{f : x \to x\} \qquad P_2 = \{\varepsilon : f \circ f \Rightarrow \mathrm{id}_x\}$$

Instead of considering $\Leftrightarrow^*$ simply as a relation, it is often useful to consider “witnesses” for this relation. From a categorical perspective, this can be formalized as follows. A presentation $P$ generates a 2-category with invertible 2-cells (also called a (2,1)-category), whose underlying category is the free category generated by the underlying graph of $P$, and whose set of 2-cells is generated by $P_2$ and denoted $P_2^*$. The category presented by $P$ can be obtained from this 2-category by identifying 1-cells where there is a 2-cell in between [5, 14]. We write $\alpha : f \Leftrightarrow^* g$ for such a 2-cell, which provides an explicit witness of the fact that $f$ and $g$ are identified in the presented category.

It is easily seen that any category admits a presentation:

**Lemma 2.3.** Any category $\mathcal{C}$ admits a presentation $P^\mathcal{C}$, called its standard presentation, with $P_0^\mathcal{C}$ being the set of objects of $\mathcal{C}$, $P_1^\mathcal{C}$ being the set of morphisms of $\mathcal{C}$ and $P_2^\mathcal{C}$ being the set of pairs $(f_2 \circ f_1, g) \in P_1^\mathcal{C} \times P_1^\mathcal{C}$ with $f_1, f_2, g \in P_1$ such that $s_0(f_1) = s_0(g)$, $t_0(f_2) = t_0(g)$ and $f_2 \circ f_1 = g$ in $\mathcal{C}$ (with projections as source and target functions).

In general, a category actually admits many presentations. It can be shown that two finite presentations present the same category if and only if they are related by a sequence of Tietze transformations: those transformations generate all the operations one can do on a presentation without modifying the presented category [22, 11]. For instance, Knuth-Bendix completions are a particular case of those [12].

**Definition 2.4.** Given a presentation $P$, a *Tietze transformation* consists in

- adding (resp. removing) a generator $f \in P_1$ and a 2-generator $\alpha : f \Rightarrow g \in P_2$ with $g \in (P_1 \setminus \{f\})^*$,

- adding (resp. removing) a 2-generator $\alpha : f \Rightarrow g \in P_2$ such that $f$ and $g$ are equivalent wrt the congruence generated by the relations in $P_2 \setminus \{\alpha\}$.

**2.2. Presentations modulo.** In a presentation $P$ of a category, the elements of $P_2$ generate relations, and the presented category is obtained by quotienting the morphisms of the free category on the underlying graph by all these relations. We now extend this notion in order to also allow the quotienting of objects in the process of constructing the presented category.

**Definition 2.5.** A *presentation modulo* $(P, \tilde{P}_1)$ consists of a presentation $P = (P_0, P_1, P_2)$ together with a set $\tilde{P}_1 \subseteq P_1$, whose elements are called *equational generators*.

The morphisms of $P^*$ generated by the equational generators are called *equational morphisms*. Intuitively, the category presented by a presentation modulo should be the “quotient category” $\|P\|/\tilde{P}_1$, as explained in the next section, where objects equivalent under $\tilde{P}_1$ (i.e. related by
equational morphisms) are identified. We believe that the reason why presentations modulo of categories were not introduced before is that they are actually unnecessary, in the sense that we can always convert a presentation modulo into a regular presentation, see Lemma 2.9 below. However, the techniques developed here extend in the case of monoidal categories where it is not the case anymore, see Section 5, and moreover our framework already enables one to obtain interesting results on presented categories (such as the equivalence between quotient and localization, see [6] for details). In this article, we will focus more on the case of presentations of monoidal categories.

**Definition 2.6.** Given a presentation modulo $(P, \tilde{P}_1)$, we define the *quotient presentation* $P/\tilde{P}_1$ as the (non-modulo) presentation $(P'_0, P'_1, P'_2)$ where

- $P'_0 = P_0/\cong_1$ where $\cong_1$ is the smallest equivalence relation on $P_0$ such that $x \cong_1 y$ whenever there exists a generator $f : x \to y$ in $\tilde{P}_1$, and we denote by $[x]$ the equivalence class of $x \in P_0$,

- the elements of $P'_1$ are $f : [x] \to [y]$ for $f : x \to y$ in $P_1$,

- the elements of $P'_2$ are of the form $\alpha : f \Rightarrow g$ for $\alpha : f \Rightarrow g$ in $P_2$, or $\alpha_f : f \Rightarrow \mathrm{id}_{[x]}$ for $f : x \Rightarrow y$ in $\tilde{P}_1$.

We will sometimes consider presentations modulo with “arrows reversed”:

**Definition 2.7.** Given a presentation modulo $(P, \tilde{P}_1)$, the *opposite presentation modulo* $(P^{\mathrm{op}}, \tilde{P}_1^{\mathrm{op}})$ is given by $P^{\mathrm{op}} = (P_0, P_1^{\mathrm{op}}, P_2^{\mathrm{op}})$, where $P_1^{\mathrm{op}} = \{f^{\mathrm{op}} : y \to x \mid f : x \to y \in P_1\}$ and where $P_2^{\mathrm{op}} = \{\alpha^{\mathrm{op}} : f^{\mathrm{op}} \Rightarrow g^{\mathrm{op}} \mid \alpha : f \Rightarrow g\}$ with $f^{\mathrm{op}} = f_1^{\mathrm{op}} \circ \dots \circ f_k^{\mathrm{op}}$ for $f = f_k \circ \dots \circ f_1$, and where $\tilde{P}_1^{\mathrm{op}}$ is the subset of $P_1^{\mathrm{op}}$ corresponding to $\tilde{P}_1$.

**2.3. Quotient and localization of a presentation modulo.** As explained above, we want to quotient our presentations modulo by equational morphisms, in order for the equational morphisms to induce equalities in the presented category. Given a category $\mathcal{C}$ and a set $\Sigma$ of morphisms, there are essentially two canonical ways to “get rid” of the morphisms of $\Sigma$ in $\mathcal{C}$: we can either force them to be identities, or to be isomorphisms, giving rise to the following two notions of quotient and localization of a category. These are standard constructions in category theory and we recall them below.

**Definition 2.8.** The *quotient* of a category $\mathcal{C}$ by a set $\Sigma$ of morphisms of $\mathcal{C}$ is a category $\mathcal{C}/\Sigma$ together with a *quotient functor* $Q : \mathcal{C} \to \mathcal{C}/\Sigma$ sending the elements of $\Sigma$ to identities, such that for every functor $F : \mathcal{C} \to \mathcal{D}$ sending the elements of $\Sigma$ to identities, there exists a unique functor $\tilde{F}$ such that $\tilde{F} \circ Q = F$.

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

Such a quotient category always exists for general reasons [2] and is unique up to isomorphism. Given a presentation modulo $(P, \tilde{P}_1)$, the category presented by the associated (non-modulo) presentation $P/\tilde{P}_1$ described in Definition 2.6, corresponds to considering the category presented by the (non-modulo) presentation $P$ and quotient it by $\tilde{P}_1$.
**Lemma 2.9.** For every presentation modulo $(P, \tilde{P}_1)$, the categories $\|P\|/\tilde{P}_1$ and $\|P/\tilde{P}_1\|$ are isomorphic.

*Proof.* It is enough to show that $\|P/\tilde{P}_1\|$ is a quotient of $\|P\|$ by $\tilde{P}_1$. We define a quotient functor $Q: \|P\| \to \|P/\tilde{P}_1\|$ on generators by $Q(x) = [x]$ for $x \in P_0$ and $Q(f) = f$ for $f \in P_1$: this extends to a functor since for every 2-generator $\alpha \in P_2$ there is a corresponding 2-generator in $P/\tilde{P}_1$. For every generator $f \in \tilde{P}_1$, we immediately have $Q(f) = \text{id}$. Suppose given a functor $F: \|P\| \to \mathcal{C}$ sending equational morphisms to identities. We define a functor $\tilde{F}: \|P/\tilde{P}_1\| \to \mathcal{C}$ sending an object $[x]$ of $\|P/\tilde{P}_1\|$ to $\tilde{F}[x] = Fx$. This does not depend on the choice of the representative of the class: given two representatives $y, y' \in [x]$, there exists a zig-zag of equational morphisms from $y$ to $y'$, all of which are sent by $F$ to identities, i.e. $Fy = Fy'$. Given a morphism $f = f_k \circ \dots \circ f_1$ in $\|P/\tilde{P}_1\|$ with $f_i \in P_1$, we define $\tilde{F}f = Ff_k \circ \dots \circ Ff_1$. For similar reasons, this is also well-defined. The functor $\tilde{F}$ satisfies $F = \tilde{F} \circ Q$, and it is the only such functor: given an object $[x]$ of $\|P/\tilde{P}_1\|$, one has necessarily $\tilde{F}[x] = \tilde{F} \circ Q(x) = Fx$ and similarly, given a generating morphism $f$ in $\|P/\tilde{P}_1\|$, one has necessarily $\tilde{F}f = \tilde{F} \circ Q(f) = Ff$. $\square$

A second, slightly different construction, consists in turning elements of $\Sigma$ into isomorphisms (instead of identities):

**Definition 2.10.** The localization of a category $\mathcal{C}$ by a set $\Sigma$ of morphisms is a category $\mathcal{C}[\Sigma^{-1}]$ together with a localization functor $L: \mathcal{C} \to \mathcal{C}[\Sigma^{-1}]$ sending the elements of $\Sigma$ to isomorphisms, such that for every functor $F: \mathcal{C} \to \mathcal{D}$ sending the elements of $\Sigma$ to isomorphisms, there exists a unique functor $\tilde{F}$ such that $\tilde{F} \circ L = F$.

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

**Remark 2.11.** Note that there is a canonical functor

$$ \tilde{Q} : \mathcal{C}[\Sigma^{-1}] \to \mathcal{C}/\Sigma $$

between the localization and the quotient, induced by the universal property of the localization applied to the quotient functor.

In the case where the category is presented, its localization admits the following presentation.

**Lemma 2.12.** Given a presentation $P = (P_0, P_1, P_2)$ and a subset $\Sigma$ of $P_1$, the category presented by $P' = (P_0, P'_1, P'_2)$ where

$$ P'_1 = P_1 \uplus \{\bar{f} : y \to x \mid f : x \to y \in \Sigma\} $$

and

$$ P'_2 = P_2 \uplus \{\bar{f} \circ f \Rightarrow \text{id}, f \circ \bar{f} \Rightarrow \text{id} \mid f \in \Sigma\} $$

is a localization of the category $\|P\|$ by $\Sigma$.

*Proof.* The localization functor $L$ is defined by $Lx = x$ for $x \in P_0$, and $Lf = f$ for $f \in P_1^*$. This functor is well-defined since for any 2-generator $\alpha: f \Rightarrow g$ in $P_2$, we have that $Lf = f$ and $Lg = g$, and there is a 2-generator $f \Rightarrow g$ in $P_2'$ by definition. Besides, for any $f$ in $\Sigma$, $Lf = f$ is an isomorphism since $\bar{f}$ is an inverse for $f$. Suppose given $F: \|P\| \to \mathcal{C}$ sending the elements of $\Sigma$ to isomorphisms. We define a functor $\tilde{F}: \|P'\| \to \mathcal{C}$ on the
generators by $\tilde{F}x = Fx$ for $x \in P_0$, $\tilde{F}f = Ff$ for $f \in P_1$ and $\tilde{F}\bar{f} = (Ff)^{-1}$. This functor is well-defined, since for any 2-generator $\alpha : f \Rightarrow g$ in $P_2 \subset P'_2$, we have $\tilde{F}f = Ff = Fg = \tilde{F}g$ and $\tilde{F}(f \circ \bar{f}) = Ff \circ \bar{F}f = Ff \circ (Ff)^{-1} = \text{id}$ and similarly $\tilde{F}(\bar{f} \circ f) = \text{id}$. This functor satisfies $\tilde{F} \circ L = F$ and is the unique such functor. $\square$

**Example 2.13.** Let us consider the category

$$ \mathcal{C} = \xrightarrow{f} \xleftarrow{g} y $$

with two objects and two non-trivial morphisms. Its localization by $\Sigma = \{f, g\}$ is equivalent to the category with one object and $\mathbb{Z}$ as set of morphisms (with addition as composition), whereas its quotient by $\Sigma$ is the category with one object and only the identity as morphism. Notice that they are not equivalent.

The description of the localization of a category provided by the universal property is often difficult to work with. When the set $\Sigma$ has nice properties, the localization admits a much more tractable description [10, 4].

**Definition 2.14.** A set $\Sigma$ of morphisms of a category $\mathcal{C}$ is a left calculus of fractions when

(1) the set $\Sigma$ is closed under composition : for $f$ and $g$ composable morphisms in $\Sigma$, $g \circ f$ is in $\Sigma$.

(2) $\Sigma$ contains the identities $\text{id}_x$ for $x$ in $P_0$.

(3) for every pair of coinital morphisms $u : x \to y$ in $\Sigma$ and $f : x \to z$ in $\mathcal{C}$, there exists a pair of cofinal morphisms $v : z \to t$ in $\Sigma$ and $g : y \to t$ in $\mathcal{C}$ such that $v \circ f = g \circ u$.

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

(4) for every morphism $u : x \to y$ in $\Sigma$ and pair of parallel morphisms $f, g : y \to z$ such that $f \circ u = g \circ u$ there exists a morphism $v : z \to t$ in $\Sigma$ such that $v \circ f = v \circ g$.

$$ x \xrightarrow{u} y \xrightarrow{f} z \xrightarrow{v} t $$

**Remark 2.15.** Note that the last condition is always satisfied when every morphism $u \in \Sigma$ is epi, since in this case we can take $v$ to be the identity.

**Theorem 2.16** ([10, 4]). When $\Sigma$ is a left calculus of fractions for a category $\mathcal{C}$, the localization $\mathcal{C}[\Sigma^{-1}]$ can be described as the category of fractions, whose objects are the objects of $\mathcal{C}$ and morphisms from $x$ to $y$ are equivalence classes of pairs of cofinal morphisms $(f, u)$ with $f : x \to i \in \mathcal{C}$ and $u : y \to i \in \Sigma$ under the equivalence relation identifying two such pairs $(f_1, u_1)$ and $(f_2, u_2)$ when there exists two morphisms $w_1, w_2 \in \Sigma$ such that $w_1 \circ u_1 = w_2 \circ u_2$ and $w_1 \circ f_1 = w_2 \circ f_2$, as shown on the left below:

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

<figure><img src="image_8.png" /></figure>
The identity on an object $x$ is the equivalence class of $(\mathrm{id}_x, \mathrm{id}_x)$ and the composition of two morphisms $(f, u) : x \to y$ and $(g, v) : y \to z$ is the equivalence class of $(h \circ f, w \circ v) : x \to z$ where the morphisms $h$ and $w$ are provided by property 1 of Definition 2.14, as shown on the right above. The localization functor $L : \mathcal{C} \to \mathcal{C}[\Sigma^{-1}]$ is the identity on objects and sends an morphism $f : x \to y$ to $(f, \mathrm{id}_y)$.

**Example 2.17.** This construction draws its name from the following example. Consider the category $\mathcal{Z}$ with one object $*$, whose morphisms are integers $n \in \mathbb{Z}$, composition is given by multiplication and identity is 1. The set $\Sigma = \mathbb{Z} \setminus \{0\}$ of all morphisms excepting 0 is a left calculus of fractions since (1) it is closed under multiplication, (2) it contains 1, (3) every pair of non-zero integers admits a non-zero common multiple, and it satisfies (4) by Remark 2.15 since every element can be canceled. The associated localization $\mathcal{Z}[\Sigma^{-1}]$ is the category with one object $*$, morphisms being rational numbers in $\mathbb{Q}$, with multiplication as composition: a morphism $(f, u)$ in the localization corresponds to the fraction $f/u$ and the quotient to the usual one, identifying $(fw)/(uw)$ with $f/u$.

Given a presentation modulo, when the (abstract) rewriting system on objects given by the equational generators is convergent, normal forms for objects provide canonical representatives of objects modulo equational generators, and therefore we are actually provided with three possible and equally reasonable constructions for the category presented by a presentation modulo $(P, \tilde{P}_1)$:

(1) the full subcategory $\|P\|_{\downarrow \tilde{P}_1}$ of $\|P\|$ whose objects are normal forms wrt $\tilde{P}_1$,

(2) the quotient category $\|P\|/\tilde{P}_1$,

(3) the localization $\|P\|_{[\tilde{P}_1^{-1}]}$.

The aim of the following two sections is to provide reasonable assumptions on the presentation modulo ensuring that the first two categories are isomorphic (normal forms provide a concrete description of the quotient), and equivalent to the third one (which captures the coherence of equational morphisms). We introduce these assumptions gradually in the next section. We first give some examples illustrating the fact that those constructions are not the same in general.

**Example 2.18.** Consider the category $\mathcal{C}$ with two objects and two non-identity morphisms depicted on the left:

$$ \mathcal{C} = x \underset{g}{\overset{f}{\rightleftarrows}} y \qquad \mathcal{T} = y \underset{\mathrm{id}}{\overset{\circ}{\rightleftarrows}} \mathcal{N} = y \underset{0,1,2,...}{\overset{\circ}{\rightleftarrows}} \mathcal{Z} = y \underset{...,-1,0,1,...}{\overset{\circ}{\rightleftarrows}} $$

It admits a presentation $P$ with $P_0 = \{x, y\}$, $P_1 = \{f : x \to y, g : x \to y\}$ and $P_2 = \emptyset$. We also write $\mathcal{T}$ for the terminal category (with one object and one identity morphism) and $\mathcal{N}$ (resp. $\mathcal{Z}$) for the category with one object and the additive monoid $\mathbb{N}$ (resp. $\mathbb{Z}$) as monoid of endomorphisms. Taking $\tilde{P}_1 = \{f, g\}$, we have (see also Example 2.13)

$$ \|P\|_{\downarrow \tilde{P}_1} = \|P\|/\tilde{P}_1 = \mathcal{T} \qquad \mathcal{C}[\Sigma^{-1}] \cong \mathcal{Z} $$

Taking $\tilde{P}_1 = \{f\}$, we have

$$ \|P\|_{\downarrow \tilde{P}_1} = \mathcal{T} \qquad \mathcal{C}[\Sigma^{-1}] \cong \|P\|/\tilde{P}_1 = \mathcal{N} $$

Thus the three constructions are not equivalent in general. Note that in both cases, $\tilde{P}_1$ (or its closure under composition and identities) is not a left calculus of fractions, because condition (3) of Definition 2.14 is not satisfied.
(2) there is no infinite path with generators in $\tilde{P}_1$.

These assumptions ensure in particular that the (abstract) rewriting system on vertices with $\tilde{P}_1$ as set of rules is convergent. Given a vertex $x \in P_0$, we write $\hat{x}$ for the associated normal form, i.e. the unique object $\hat{x}$ such that there is a morphism $f : x \to \hat{x}$ in $\tilde{P}_1^*$ and there is no generator of the form $f : \hat{x} \to x'$ in $\tilde{P}_1$. The classical Newman's lemma [18] holds in our framework:

**Lemma 3.2.** For any pair of coinitial morphisms $f : x \to y_1$ in $\tilde{P}_1^*$ and $g : x \to y_2$ in $P_1^*$, there exist a pair of cofinal morphisms $g' : y_1 \to z$ in $P_1^*$ and $f' : y_2 \to z$ in $\tilde{P}_1^*$ and a 2-cell $\alpha : g' \circ f \Leftrightarrow f' \circ g$ in $P_2^*$.

For every pair of distinct morphisms $(f, g)$ as in the Assumption 1, we suppose fixed an arbitrary choice of a particular triple $(g', \alpha, f')$ associated to it, and write $g/f$ for $g'$, $f/g$ for $f'$ and $\rho_{f,g}$ for $\alpha$:

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

The morphism $g/f$ (resp. $f/g$) is called the *residual* of $g$ after $f$ (resp. $f$ after $g$): intuitively, $g/f$ corresponds to what remains of $g$ once $f$ has been performed. It is natural to extend this definition to paths as follows:

**Definition 3.3.** Given two coinitial paths $f : x \to y$ and $g : x \to z$ and $P_1^*$ such that either $f$ or $g$ is in $\tilde{P}_1^*$, we define the *residual* $g/f$ of $g$ after $f$ as above when $f$ and $g$ are distinct generators, and by means of the following rules:

$$ \begin{array}{lclcl} f/f = \mathrm{id}_y & g/\mathrm{id}_x = g & \mathrm{id}_x/f = \mathrm{id}_y & (g_2 \circ g_1)/f = (g_2/(f/g_1)) \circ (g_1/f) & g/(f_2 \circ f_1) = (g/f_1)/f_2 \end{array} $$

(by convention the residual $g/f$ is not defined when neither $f$ nor $g$ belongs to $\tilde{P}_1^*$). Graphically,

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

The above rules, when applied from left to right, provide a non-deterministic algorithm for computing residuals of paths along paths. We will show in Lemma 3.11 that, under an additional assumption, this algorithm terminates and that the result does not depend on the order in which the above rules are applied. Moreover, it can be checked that residuation is compatible with associativity and identity laws, so that altogether the notion of residuation is well-defined on paths.

**Remark 3.4.** In condition (1) of Assumption 3.1, in order for Newman's lemma (and in fact also all subsequent properties) to hold, it would be enough to suppose that we have $g' \circ f \Leftrightarrow f' \circ g$ instead of requiring that there is exactly one 2-generator $\alpha$ mediating the two
morphisms. However, this would makes some formulations more involved, without bringing more generality in practice.

**Remark 3.5.** It might seem at first that Assumption 3.1 is sufficient to ensure that quotienting by $\tilde{P}_1$ or localizing wrt $\tilde{P}_1$ give rise to equivalent categories, but Example 2.19 shows that this is not the case and more assumptions are needed. In particular termination, which is introduced below.

To ensure that the definition of residuation is well-founded, and thus always defined, we will make the following additional assumption. We first recall that a poset $(N, \leq)$ is noetherian if there is no infinite descending chain $n_0 > n_1 > n_2 > \dots$ of elements of $N$; the typical example of such a poset is $(\mathbb{N}, \leq)$. A noetherian monoid $(N, +, 0, \leq)$ is a (non-necessarily commutative) monoid $(N, +, 0)$ together with a structure of noetherian poset $(N, \leq)$, such that for every $x, y, y', z \in N$,

$$y > y' \quad \text{implies} \quad x + y + z > x + y' + z$$

and 0 is the minimum element. Again, a typical example of such a monoid is $(\mathbb{N}, +, 0, \leq)$.

**Assumption 3.6.** There is a weight function $\omega_1: P_1 \to N$, where $(N, +, 0, \leq)$ is a noetherian monoid, such that for every generator $g \in P_1$ and $f \in \tilde{P}_1$, we have $\omega_1(g/f) < \omega_1(g)$, where we extend $\omega_1$ on elements of $P_1^*$ by $\omega_1(g \circ f) = \omega_1(g) + \omega_1(f)$ and $\omega_1(\text{id}) = 0$.

**Remark 3.7.** Note in particular that, with the previous assumption, we always have

$$\omega_1(g) < \omega_1(h) + \omega_1(g) + \omega_1(f) = \omega_1(h \circ g \circ f)$$

for composable morphisms $f, g$ and $h$.

In order to study confluence of the rewriting system provided by equational morphisms, through the use of residuals, we first introduce the following category, which allows us to consider, at the same time, both residuals $g/f$ and $f/g$ of two coin initial morphisms $f$ and $g$.

**Definition 3.8.** The zig-zag presentation associated to the presentation modulo $(P, \tilde{P}_1)$ is the presentation $Z = (Z_0, Z_1, Z_2)$ with $Z_0 = P_0$, $Z_1 = P_1 \uplus \tilde{P}_1$ (generators in $\tilde{P}_1$ are of the form $\bar{f}: B \to A$ for any generator $f: A \to B$ in $\tilde{P}_1$) and relations in $Z_2$ are of the form $g \circ \bar{f} \Rightarrow (\overline{f/g}) \circ (g/f)$

$$\begin{array}{ccc}
 & \xrightarrow{g/f} & z \\
\bar{f} & \Rightarrow & \overline{f/g} \\
x & \xrightarrow{g} & y_2
\end{array}$$

or $f \circ \bar{f} \Rightarrow \text{id}_y$ for any pair of distinct coin initial generators $f: x \to y \in \tilde{P}_1$ and $g: x \to z \in P_1$.

**Lemma 3.9.** The rewriting system on morphisms in $Z_1^*$ with $Z_2$ as rules is convergent. Given two coin initial morphisms $f: x \to y$ in $\tilde{P}_1^*$ and $g: x \to z$ in $P_1^*$, the normal form of $g \circ \bar{f}$ is $(\overline{f/g}) \circ (g/f)$.

*Proof.* We extend the weight function of Assumption 3.6 to morphisms in $Z_1^*$ by setting $\omega_1(\bar{f}) = 0$ for $\bar{f}$ in $\tilde{P}_1$. This ensures that the rewriting system on morphisms in $Z_1^*$ with $Z_2$ as rules is terminating. Moreover, because the left members of rules are of the form $g \circ \bar{f}$ with $g \in P_1$ and $\bar{f} \in \tilde{P}_1$, there are no critical pairs (a morphism of the form $g \circ \bar{f}$ cannot
non-trivially overlap with a morphism of the form $g' \circ \bar{f}'$), which implies that the rewriting
system is confluent. Given two coinitial morphisms $f: x \to y$ in $\tilde{P}_1^*$ and $g: x \to z$ in $P_1^*$, we
prove by well-founded induction on $\omega_1(g \circ \bar{f})$ that the normal form of $g \circ \bar{f}$ is $(f/g) \circ (g/f)$.
If either $f$ or $g$ is an identity, this is direct. Otherwise, $f = f_2 \circ f_1$ and $g = g_2 \circ g_1$ where $f_1$,
$f_2$, $g_1$ and $g_2$ are non-identity morphisms.

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

By induction, we have

$$
g_1 \circ \bar{f}_1 \stackrel{*}{\Rightarrow} (\overline{f_1/g_1}) \circ (g_1/f_1) \quad \text{and} \quad (g_1/f_1) \circ \bar{f}_2 \stackrel{*}{\Rightarrow} (\overline{f_2/(g_1/f_1)}) \circ ((g_1/f_1)/f_2)
$$

because

$$
\omega_1(g_1 \circ \bar{f}_1) < \omega_1(g_2 \circ g_1 \circ \bar{f}_1 \circ \bar{f}_2) = \omega_1(g \circ \bar{f})
$$

and

$$
\omega_1((g_1/f_1) \circ \bar{f}_2) < \omega_1(g_2 \circ (\overline{f_1/g_1}) \circ (g_1/f_1) \circ \bar{f}_2) < \omega_1(g \circ \bar{f})
$$

Therefore,

$$
\begin{align*}
g \circ \bar{f} & \stackrel{*}{\Rightarrow} g_2 \circ \overline{(f_1/g_1)} \circ (g_1/f_1) \circ \bar{f}_2 \\
& \stackrel{*}{\Rightarrow} g_2 \circ \overline{(f_1/g_1)} \circ \overline{(f_2/(g_1/f_1))} \circ ((g_1/f_1)/f_2) \\
& = g_2 \circ \overline{(f/g_1)} \circ (g_1/f)
\end{align*}
$$

Similarly,

$$
\omega_1(g_2 \circ (\overline{f/g_1}) \circ (\overline{f_2/(g_1/f_1)})) < \omega_1(g \circ \bar{f})
$$

therefore

$$
g_2 \circ \overline{(f/g_1)} \circ \overline{(f_2/(g_1/f_1))} \stackrel{*}{\Rightarrow} \overline{((f/g_1)/g_2)} \circ (g_2/(f/g_1))
$$

and we have

$$
\begin{align*}
g \circ \bar{f} & \stackrel{*}{\Rightarrow} g_2 \circ \overline{(f/g_1)} \circ (g_1/f) \\
& \stackrel{*}{\Rightarrow} \overline{((f/g_1)/g_2)} \circ (g_2/(f/g_1)) \circ (g_1/f) \\
& = \overline{(f/g)} \circ (g/f)
\end{align*}
$$

from which we conclude.

□
**Remark 3.10.** The termination Assumption 3.6 is not the only possible one. For instance, an abstract rewriting system is called strongly confluent when $x \to y_1$ and $x \to y_2$ implies that there exists $z$ such that $y_1 \to z$ (or $y_1 = z$) and $y_2 \underset{z}{\stackrel{*}{\to}} z$. Such an abstract rewriting system is always confluent [13]. This translates to our setting: if, in every residuation relation of the form (3.1), we have that $f/g$ (resp. $g/f$) is always a generator or an identity, then the rewriting system on $Z_1^*$ with $Z_2$ as rules is confluent and $g \circ \bar{f}$ rewrites to $(\overline{f/g}) \circ (g/f)$.

As a direct corollary of the convergence of the rewriting system, one can show that Definition 3.3 makes sense:

**Lemma 3.11.** *The residuation operation does not depend on the order in which equalities of Definition 3.3 are applied.*

Moreover, a “global” version of the residuation property (Assumption 3.1) holds:

**Proposition 3.12.** *Given two coinitial morphisms $f : x \to y$ in $\tilde{P}_1^*$ and $g : x \to z$ in $P_1^*$, there exists a 2-cell $\alpha : (g/f) \circ f \stackrel{*}{\Leftrightarrow} (f/g) \circ g$.*

*Proof.* By Lemma 3.9, there exists a rewriting path $\beta : g \circ \bar{f} \Rightarrow \overline{(f/g)} \circ (g/f)$ in $Z_2^*$. By induction on its length, we can construct a 2-cell $\alpha : (g/f) \circ f \stackrel{*}{\Leftrightarrow} (f/g) \circ g$ in the following way. The case where $\beta$ is empty is immediate, otherwise we have $f = f_2 \circ f_1$ and $g = g_2 \circ g_1$ where $f_2$ is in $\tilde{P}_1^*$ (resp. $g_2$ in $P_1^*$) and $f_1$ is a generator in $\tilde{P}_1$ (resp. $g_1$ in $P_1$). We distinguish two cases depending on the form of the first rule of $\beta$:

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

If $f_1 = g_1$, i.e. if the first step of $\beta$ corresponds to rewriting $g_2 \circ g_1 \circ \bar{f}_1 \circ \bar{f}_2$ to $g_2 \circ \bar{f}_2$ by applying the rewriting rule $f_1 \circ \bar{f}_1 \Rightarrow \text{id}$ of $Z_2$ (we necessarily have $f_1 = g_1$), then by induction hypothesis, there exists a 2-cell

$$ \alpha' : (g_2/f_2) \circ f_2 \stackrel{*}{\Leftrightarrow} (f_2/g_2) \circ g_2 $$

Since $f_2/g_2 = f/g$ and $g_2/f_2 = g/f$, this means that there exists a 2-cell

$$ (g/f) \circ f \stackrel{*}{\Leftrightarrow} (f/g) \circ g $$

Otherwise $f_1 \neq g_1$, and $g_2 \circ g_1 \circ \bar{f}_1 \circ \bar{f}_2$ rewrites to $g_2 \circ (\overline{f_1/g_1}) \circ (g_1/f_1) \circ \bar{f}_2$ by applying the rewriting rule $g_1 \circ \bar{f}_1 \Rightarrow (\overline{f_1/g_1}) \circ (g_1/f_1)$ of $Z_2$. By definition of the 2-generators in $Z_2$, there exists a 2-generator

$$ (g_1/f_1) \circ f_1 \Leftrightarrow (f_1/g_1) \circ g_1 $$

in $P_2$. Moreover, by Lemma 3.9, the morphism $g_2 \circ (\overline{f_1/g_1})$ in $Z_1^*$ rewrites to $(\overline{f_1/g}) \circ (g_2/(f_1/g_1))$, and therefore by induction hypothesis, there exists a 2-cell

$$ (g_2/(f_1/g_1)) \circ (f_1/g_1) \stackrel{*}{\Leftrightarrow} ((f_1/g_1)/g_2) \circ g_2 $$
*Proof.* Suppose given $f: x \to y$ in $\tilde{P}_1^*$, and $g_1, g_2: y \to z$ in $P_1^*$ such that $g_1 \circ f \stackrel{*}{\Leftrightarrow} g_2 \circ f$. By Proposition 3.14, we have

$$g_1 = (g_1 \circ f)/f \stackrel{*}{\Leftrightarrow} (g_2 \circ f)/f = g_2$$

from which we conclude. □

Our axiomatization can also be used to show the following proposition, which will not be used in the rest of the article:

**Proposition 3.20** ([6]). In the category $\|P\|$, every morphism $g$ admits a pushout along a coinital equational morphism $f$ given by $g/f$.

**Remark 3.21.** The careful reader will have noticed that, so far, we have only used the cylinder property in the case where the “vertical morphism” $f$ is equational. The case where both $g_1$ and $g_2$ are equational will be used in the proof of Theorem 4.2.

## 4. COMPARING PRESENTED CATEGORIES

**4.1. The category of normal forms.** We first show that with our hypotheses on the rewriting system, the quotient category $\|P\|/\tilde{P}_1$ can be recovered as the following subcategory of $\|P\|$, whose objects are those which are in normal form for $\tilde{P}_1$.

**Definition 4.1.** The category of normal forms $\|P\|\downarrow\tilde{P}_1$ is the full subcategory of $\|P\|$ whose objects are the normal forms of elements of $P_0$ wrt rules in $\tilde{P}_1$. We write $I: \|P\|\downarrow\tilde{P}_1 \to \|P\|$ for the inclusion functor.

For every object $x$ of $\|P\|$, we shall denote the associated normal form by $\hat{x}$, and for every such object $x$ we shall fix a choice of an equational morphism $u_x$ from $x$ to its normal form. Note that, by Newman’s Lemma 3.2, if $u_x': x \to \hat{x}$ is another choice of such a morphism then there is a 2-cell $u_x \stackrel{*}{\Leftrightarrow} u_x'$. Also, we always have $u_{\hat{x}} = \mathrm{id}_{\hat{x}}$.

**Theorem 4.2.** The category $\|P\|\downarrow\tilde{P}_1$ is isomorphic to the quotient category $\|P\|/\tilde{P}_1$.

*Proof.* We show that the category $\|P\|\downarrow\tilde{P}_1$ is a quotient of $P$ by $\tilde{P}_1$. We define a functor $N: \|P\| \to \|P\|\downarrow\tilde{P}_1$ as the functor associating to each object $x$ its normal form $\hat{x}$ under $\tilde{P}_1$, and to each morphism $f: x \to y$, the morphism $\hat{f}: \hat{x} \to \hat{y}$ where $\hat{f} = u_{y'} \circ (f/u_x)$ with $y'$ being the target of $f/u_x$:

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

Notice that, a priori, this definition depends on a choice of a representative in $P_1^*$ for $f$, and in $\tilde{P}_1^*$ for $u_x$ and $u_{y'}$, in the equivalence classes of morphisms modulo the relations in $P_2$. The global cylinder property shown in Proposition 3.14 ensures that the definition is
independent of the choice of such representatives (in particular, for $u_x$ we use the consequence of Newman's lemma mentioned above and the cylinder property in the case where the basis is equational). Given two composable morphisms $f: x \to y$ and $g: y \to z$ we have

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

The image of an equational morphism $u: x \to y$ under the functor $N$ is an identity. Namely, we have $Nu = \hat{u} = u_{y'} \circ (u/u_x)$, with $u/u_x: \hat{x} \to y'$: since $u/u_x$ is an equational morphism (as the residual of an equational morphism) whose source is a normal form, necessarily $u/u_x = \mathrm{id}_{\hat{x}}$, $y' = \hat{x}$ and $u_{y'} = \mathrm{id}_{\hat{x}}$. In particular, $N$ preserves identities.

Suppose given a functor $F: \|P\| \to \mathcal{C}$ sending the equational morphisms to identities. We have to show that there exists a unique functor $G: \|P\|_{\downarrow \tilde{P}_1} \to \mathcal{C}$ such that $G \circ N = F$. Writing $I: \|P\|_{\downarrow \tilde{P}_1} \to \|P\|$ for the inclusion functor, it is easy to show $I$ is a section of $N$, i.e. $N \circ I = \mathrm{Id}_{\|P\|_{\downarrow \tilde{P}_1}}$, and we define $G = F \circ I$.

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

Since $F$ sends equational morphisms to identities, it is easy to check that $G \circ N = F$: given an object $x$, we have

$$G \circ N(x) = G(\hat{x}) = F \circ I(\hat{x}) = F(\hat{x}) = F(x)$$

the last equality, being due to the fact that $F(u_x) = \mathrm{id}_{F(\hat{x})} = \mathrm{id}_{F(x)}$, and similarly for morphisms. Finally, we check the uniqueness of the functor $G$. Suppose given another functor $G': \|P\|_{\downarrow \tilde{P}_1} \to \mathcal{C}$ such that $G' \circ N = F = G \circ N$. We have $G' = G' \circ N \circ I = G \circ N \circ I = G$. $\square$

**4.2. Equivalence with the localization.** We now show that the two previous constructions (quotient and normal forms) also coincide with the third possible construction which consists in formally adding inverses for equational morphisms.

**Definition 4.3.** A presentation modulo $(P, \tilde{P}_1)$ is called *coherent* when the canonical functor $\|P\|_{[\tilde{P}_1^{-1}]} \to \|P\|_{\tilde{P}_1}$ is an equivalence of categories.

First, notice that we can use the description of the localization $\|P\|_{[\tilde{P}_1^{-1}]}$ as a category of fractions given in Theorem 2.16:

**Lemma 4.4.** The set $\tilde{P}_1^*/P_2$ of equational morphisms of $\|P\|$ is a left calculus of fractions.
*Proof.* We have to show that the set of equational morphisms satisfies the four conditions of Definition 2.14: the first two (closure under composition and identities) are immediate, the third one follows from Proposition 3.12, and the last one is ensured by the fact that all equational morphisms are epi by Proposition 3.19, see Remark 2.15. □

**Theorem 4.5.** A presentation modulo $(P, \tilde{P}_2)$ which satisfies assumptions 3.1 to 3.16 is coherent.

*Proof.* By Theorem 4.2, the statement can be rephrased as the claim that $\|P\|_{\downarrow \tilde{P}_1}$ and $\|P\|_{[\tilde{P}_1^{-1}]}$ are equivalent categories.

Suppose given a morphism $(f, u)$ from $x$ to $\hat{y}$ in the category of fractions $\|P\|_{[\tilde{P}_1^{-1}]}$, where $\hat{y}$ is a normal form under $\tilde{P}_1$, as on the left below

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

Since $u$ is equational and $\hat{y}$ is a normal form, one necessarily has $i = \hat{y}$ and $u = \text{id}_{\hat{y}}$. Similarly, given two equivalent morphisms $(f_1, u_1)$ and $(f_2, u_2)$ whose targets are both a normal form $\hat{y}$, as on the right above, one has $i_1 = i_2 = \hat{y}$ and $u_1 = u_2 = w_1 = w_2 = \text{id}_{\hat{y}}$, and therefore $f_1 = f_2$. Now, consider the functor $F : \|P\|_{\downarrow \tilde{P}_1} \to \|P\|_{[\tilde{P}_1^{-1}]}$ defined as the composite of the inclusion functor $I : \|P\|_{\downarrow \tilde{P}_1} \to \|P\|$, see Definition 4.1, with the localization functor $L : \|P\| \to \|P\|_{[\tilde{P}_1^{-1}]}$, see Definition 2.10:

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

The functor $F$ sends a morphism $f : \hat{x} \to \hat{y}$ in the category of normal forms to the morphism $(f, \text{id}_{\hat{y}})$ in the category of fractions. The preceding remarks imply immediately that the functor $F$ is full and faithful. Finally, given an object $y \in \|P\|_{[\tilde{P}_1^{-1}]}$, there is a morphism $u : y \to \hat{y}$ in $\tilde{P}_1^*$ to its normal form which induces an isomorphism $y \cong \hat{y}$ in $\|P\|_{[\tilde{P}_1^{-1}]}$. The functor $F$ thus provides a weak inverse to the canonical functor $\|P\|_{[\tilde{P}_1^{-1}]} \to \|P\|_{\tilde{P}_1}$, which is therefore an equivalence of categories. □

An illustration of this theorem is provided in [6], on the presentation of a “dihedral category” (note that the assumptions on the opposite presentation $P^{\text{op}}$ mentioned there were superfluous, as shown by the new proof of the above theorem). Here, in Section 5, we will provide a detailed example, in the refined setting of a presentation of a monoidal category.

**4.3. Embedding into the localization.** In this section, we show another direct application of our techniques. It is sometimes useful to show that a category embeds into its localization. When the category is equipped with a calculus of fractions, this can be shown using the following proposition [4, Exercise 5.9.2]:
**Proposition 4.6.** Given a left calculus of fractions $\Sigma$ for a category $\mathcal{C}$, all the morphisms of $\Sigma$ are mono if and only if the inclusion functor $L : \mathcal{C} \to \mathcal{C}[\Sigma^{-1}]$ is faithful.

*Proof.* Suppose that the elements of $\Sigma$ are monos. Given two morphisms $f_1, f_2 : x \to y$ in $\mathcal{C}$ such that $Lf_1 = Lf_2$, we have a diagram as on the left of (2.2) with $u_1 = u_2 = \mathrm{id}_y$, and therefore $w_1 = w_2$. Commutation of the left part of the diagram gives $w_1 \circ f_1 = w_2 \circ f_2$ and therefore $f_1 = f_2$ since $w_1 = w_2$ is mono. The functor $L$ is faithful.

Conversely, suppose that $L$ is faithful. Given morphisms $w, f_1$ and $f_2$ such that $w \in \Sigma$ and $w \circ f_1 = w \circ f_2$, one has $Lf_1 = Lf_2$ and therefore $f_1 = f_2$. The morphism $w$ is thus mono. $\square$

Showing that the elements of $\Sigma$ are monos can however be difficult. In the case where $\mathcal{C} = \|P\|$ and $\Sigma = P_1^*$, for some presentation modulo $(P, \tilde{P}_1)$, it can be proved as follows.

**Lemma 4.7.** Suppose given a presentation modulo $(P, \tilde{P}_1)$ such that the opposite presentation modulo $(P^{\mathrm{op}}, \tilde{P}^{\mathrm{op}})$ satisfies Assumptions 3.1, 3.6, 3.13 and 3.16. Then the localization functor $\|P\| \to \|P\|[[\tilde{P}_1^{-1}]]$ is faithful.

*Proof.* By the dual of Proposition 3.19, all equational morphisms are mono, and we apply Proposition 4.6. $\square$

Again, an example of application is provided in [6].

**Remark 4.8.** The result in the previous proposition is close to Dehornoy's theorem, see [8] and [9, Section II.4], stating that a monoid with a presentation satisfying suitable conditions (our assumptions are variants of those) embeds into the enveloping groupoid. Dehornoy's setting is more restricted, since taking the enveloping groupoid corresponds to localizing wrt every morphism, while we consider localization with respect to a class of morphisms. However, we also need stronger conditions: in Assumption 3.1, we require the equational rewriting system to be terminating, which is never the case for presentations of monoids since they have only one object when seen as categories. Dehornoy's conditions also impose termination properties (called there *Noetherianity*), but only “locally”. A detailed comparison, together with conditions unifying the two approaches, is left for future work.

# 5. COHERENT PRESENTATIONS OF MONOIDAL CATEGORIES

## 5.1. Presentations of monoidal categories.
We now turn our attention to presentations of monoidal categories and describe how the previous developments can be adapted to this setting. Only strict and small such categories will be considered in this article. We start from premonoidal categories [20], which will be of some use later on. In fact, all the developments performed in this section could have been carried out in the slightly more general setting of 2-categories. However, we feel that the shift in dimension would have obscured the comparison with the previous sections.

**Definition 5.1.** A (strict) premonoidal category $(\mathcal{C}, \otimes, I)$ consists of a category $\mathcal{C}$ together with

(1) for every object $x \in \mathcal{C}$, a functor $x \otimes - : \mathcal{C} \to \mathcal{C}$ called *left action*,

(2) for every object $x \in \mathcal{C}$, a functor $- \otimes x : \mathcal{C} \to \mathcal{C}$ called *right action*,

(3) an object $I \in \mathcal{C}$, called *unit object*,
such that

- the left and right actions coincide on objects: for every objects $x, y \in \mathcal{C}$, $x \otimes y$ is the same whether the $\otimes$ operation is the left or the right action, thus justifying the use of the same notation,

- the set of objects of $\mathcal{C}$ is a monoid when equipped with $\otimes$ as multiplication and $I$ as neutral element: for every objects $x, y, z \in \mathcal{C}$,

$$ (x \otimes y) \otimes z = x \otimes (y \otimes z) \qquad I \otimes x = x = x \otimes I $$

- the left action is a monoid action: for every objects $x, y \in \mathcal{C}$ and morphism $f$,

$$ x \otimes (y \otimes f) = (x \otimes y) \otimes f \qquad I \otimes f = f $$

- the right action is a monoid action: for every objects $x, y \in \mathcal{C}$ and morphism $f$,

$$ (f \otimes x) \otimes y = f \otimes (x \otimes y) \qquad f \otimes I = f $$

- the left and right actions are compatible: for every objects $x, y \in \mathcal{C}$ and morphism $f$,

$$ (x \otimes f) \otimes y = x \otimes (f \otimes y) $$

A (strict) *monoidal category* is a premonoidal category as above satisfying the exchange law: for every morphisms $f: x \to x'$ and $g: y \to y'$,

$$ (x' \otimes g) \circ (f \otimes y) = (f \otimes y') \circ (x \otimes g) $$

allowing us to denote by $f \otimes g$ this morphism, and for every objects $x, y \in \mathcal{C}$,

$$ x \otimes \mathrm{id}_y = \mathrm{id}_{x \otimes y} = \mathrm{id}_x \otimes y $$

We sometimes omit the tensor and simply write $xy$ instead of $x \otimes y$.

**Definition 5.2.** A monoidal functor $F: \mathcal{C} \to \mathcal{D}$ between two (pre)monoidal categories is a functor equipped with a morphism $\eta: I_{\mathcal{D}} \to F(I_{\mathcal{C}})$ and a natural transformation of components

$$ \mu_{x,y} : F(x) \otimes_{\mathcal{D}} F(y) \to F(x \otimes_{\mathcal{C}} y) $$

making the following diagrams commute for every $x, y, z \in \mathcal{C}$:

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

A monoidal functor is *strong* (resp. *strict*) when $\eta$ and $\mu_{x,y}$ are isomorphisms (resp. identities).

Since giving a monoidal structure on a category adds a structure of monoid on the objects, this suggests introducing the following generalization of graphs and presentations, in order to present monoidal categories.
**Definition 5.3.** A monoidal graph $(P_0, s_0, t_0, P_1)$ consists of a diagram

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

in **Set**, where $P_0^*$ is the free monoid on $P_0$ and $i_0 : P_0 \to P_0^*$ is the canonical injection (sending an element to the corresponding word with one letter).

Note that a monoidal graph is simply another name for the data of a *string rewriting system*: the set $P_0$ is the *alphabet*, with $P_0^*$ as set of *words* over it, and $P_1$ is the set of *rewriting rules* along with their source and target respectively indicated by the functions $s_0$ and $t_0$. This allows us to consider classical notions in string rewriting theory (such as critical pairs) in this context, see [1, 3] for details about those.

A monoidal graph freely generates a monoidal category. If we write $P_1^*$ for its set of morphisms $i_1 : P_1 \to P_1^*$ for the canonical injection of generators into morphisms, and $s_0^*, t_0^* : P_0^* \to P_0^*$ for the source and target maps, we obtain a diagram

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

where $s_0^* \circ i_1 = s_0$ and $t_0^* \circ i_1 = t_0$. An explicit description of the morphisms in $P_1^*$ is given by the following lemma: the morphisms of the free premonoidal category are easy to describe and those of the free monoidal category can be obtained by explicitly quotienting by axioms imposing that the exchange law holds.

**Lemma 5.4.** *Suppose fixed a monoidal graph P.*

(1) The underlying category of the free premonoidal category generated by $P$ is the free category generated (in the sense of Section 2.1) by the graph $Q$

- with $Q_0 = P_0^*$ as vertices

- edges in $Q_1$ are triples

$$ (x, f, z) : xyz \to xy'z $$

with $x, z \in P_0^*$ and $f : y \to y'$ in $P_1$.

and is equipped with the expected premonoidal structure, whose left and right actions are given by

$$ x' \otimes (x, f, z) \otimes z' = (x'x, f, zz') $$

In the following, we write $x \otimes f \otimes z$, or even $xfz$, instead of $(x, f, z)$ for edges, and the morphisms in $P_1^*$ will be denoted by $P_1^\otimes$.

(2) The underlying category of the free monoidal category generated by $P$ is the category presented (in the sense of Definition 2.1) by $Q = (Q_0, Q_1, Q_2)$, where $Q_2$ is the set of all relations

$$ \chi_{z_1fz_2,z_3gz_4} : (z_1x'z_2z_3gz_4) \circ (z_1fz_2z_3yz_4) \Rightarrow (z_1fz_2z_3y'z_4) \circ (z_1xz_2z_3gz_4) \quad (5.1) $$

called exchange relations, where $z_1fz_2, z_3gz_4 \in Q_1$, with $f : x \to x'$ and $g : y \to y'$ in $P_1$.

We write $\Leftrightarrow$ for the equivalence relation generated by $Q_2$. The morphisms of this category
are denoted by $P_1^*$ and its monoidal structure is induced by the previous premonoidal structure.

**Example 5.5.** Consider the monoidal graph with $P_0 = \{a\}$ and $P_1 = \{m : aa \to a\}$. The following are morphisms in the free (pre)monoidal category:

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

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

and can be represented using string diagrams as

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

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

These are equal in the free monoidal category, but not in the free premonoidal category: one needs the exchange rules in order to transform one into the other.

With the notations of the previous lemma, a generator $xfz : xyz \to xy'z$ in $Q_1$ can also be called a *rewriting step*: it corresponds to the rewriting rule $f : y \to y'$ used in a context with the word $x$ on the left and $z$ on the right. We sometimes write

$$Q_1 = P_0^* P_1 P_0^*$$

for the set of rewriting steps. From this point of view, the morphisms in $P_1^\otimes$ are *rewriting paths* and the morphisms in $P_1^*$ are *rewriting paths* up to commutation of independent rewriting steps, i.e. up to the equivalence relation $\stackrel{\chi}{\rightleftharpoons}$.

**Definition 5.6.** A monoidal presentation $P = (P_0, s_0, t_0, P_1, s_1, t_1, P_2)$ consists of a diagram

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

in **Set**, where

- $P_0$ is a set of *object generators*;

- $P_0^*$ is the free monoid on $P_0$ and $i_0 : P_0 \to P_0^*$ is the canonical injection;

- $P_1$ is a set of *morphism generators*, with $s_0, t_0 : P_1 \to P_0^*$ indicating their source and target;

- $P_1^*$ is as in Lemma 5.4, with corresponding source and target maps $s_0^*, t_0^* : P_1^* \to P_0^*$.

- $P_2$ is a set of *relations* (or *2-cell generators*), with $s_1, t_1 : P_2 \to P_1^*$ indicating their source and target, which should satisfy the globular identities $s_0^* \circ s_1 = s_0^* \circ t_1$ and $t_0^* \circ s_1 = t_0^* \circ t_1$.

The monoidal category $\|P\|$ presented by $P$ is the monoidal category with $P_0^*$ as set of objects and whose morphisms are the elements of $P_1^*$, quotiented by the smallest congruence (wrt both composition and tensor product) identifying any two morphisms $f$ and $g$ such that there is a relation $\alpha : f \Rightarrow g$.

We also introduce the notation $P_2^*$ (resp. $P_2^\otimes$) for the set of 2-cells in the monoidal (2,1)-category (resp. premonoidal (2,1)-category) whose underlying monoidal (resp. premonoidal) category is freely generated by the underlying monoidal graph of $P$, and 2-cells are generated
by $P_2$. We do not detail these constructions: all the reader needs to remember for the sequel is that these 2-cells are formal (vertical) composites of 2-cells of the form

$$x\alpha z : x fz \Rightarrow xgz : xyz \rightarrow xy'z \qquad (5.2)$$

for $x, z \in P_0^*$ and $\alpha : f \Rightarrow g : y \rightarrow y'$ in $P_2$, or their inverses. The set of 2-cells of the form (5.2) is denoted $P_0^*P_2P_0^*$.

Note that a presented monoidal category has an underlying monoid of objects which is free. Therefore, not every monoidal category admits a presentation, e.g. the category with $N/2N$ as monoid of objects and only identities as morphisms. In this setting, the use of coherent presentation is really necessary: there is no associated notion of “quotient presentation” (as in Definition 2.6).

**Definition 5.7.** A monoidal presentation modulo consists of a monoidal presentation together with a set $\tilde{P}_1 \subseteq P_1$ of equational generators (notation $(P, \tilde{P}_1)$).

As before, we say that a morphism in $P_1^*$ (or in $P_1^{\otimes}$) is equational when it can be obtained by composing and tensoring equational generators and identities. We write $\tilde{P}_1^* \subseteq P_1^*$ (or $\tilde{P}_1^{\otimes} \subseteq P_1^{\otimes}$) for the set of equational morphisms.

We now generalize the notions of quotient and localization to monoidal categories.

**Definition 5.8.** The quotient of a monoidal category $\mathcal{C}$ by a set $\Sigma$ of morphisms is a monoidal category $\mathcal{C}/\Sigma$ together with a strict monoidal functor $\mathcal{C} \to \mathcal{C}/\Sigma$ sending elements of $\Sigma$ to identities, which is universal with this property.

**Definition 5.9.** The localization of a monoidal category $\mathcal{C}$ by a set $\Sigma$ of morphisms is a monoidal category $\mathcal{C}[\Sigma^{-1}]$ together with a strict monoidal functor $L : \mathcal{C} \to \mathcal{C}[\Sigma^{-1}]$ sending the elements of $\Sigma$ to isomorphisms, which is universal with this property.

The localization of a presented monoidal category always admits a monoidal presentation as in Lemma 2.12. Moreover, the description as a category of fractions under suitable conditions (Theorem 2.16) is still valid [7]:

**Proposition 5.10.** Suppose given a left calculus of fractions $\Sigma$ for a monoidal category $\mathcal{C}$, which is closed under tensor product, i.e. for every $f, g \in \Sigma$, we have $f \otimes g \in \Sigma$. The associated category of fractions is canonically monoidal and isomorphic to the localization in the sense of Definition 5.9.

*Proof.* The unit object is the one of $\mathcal{C}$, and given two morphisms $(f, u)$ and $(g, v)$ in the category of fractions $\mathcal{C}[\Sigma^{-1}]$, we define their tensor product as $(f, u) \otimes (f', u') = (f \otimes f', u \otimes u')$. Suppose that $(f_1, u_1)$ and $(f_2, u_2)$ (resp. $(f'_1, u'_1)$ and $(f'_2, u'_2)$) are two representatives of the same morphism, i.e. that we have mediating morphisms as on the left and the middle below:

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

The diagram on the right shows that $(f_1, u_1) \otimes (f'_1, u'_1)$ and $(f_2, u_2) \otimes (f'_2, u'_2)$ represent the same morphism. The fact that the axioms of a monoidal category are satisfied is easily deduced from the fact that $\mathcal{C}$ does satisfy those axioms and from the closure of $\Sigma$ under tensor product. $\square$
**5.2. Residuation in monoidal presentations.** We now explain how to extend the residuation techniques developed in Section 3 to presentations of monoidal categories. By Lemma 5.4, a presentation of a monoidal category can be seen as a presentation of a premonoidal category together with explicit exchange rules $\chi_{f,g}$. The general strategy is thus to apply the previous constructions and to show that they are compatible with the exchange law: this strategy turns out to work in our running example, but we explain in Section 5.5 that further generalizations of the axioms are sometimes needed, requiring to deal explicitly with exchange relations. From now on, we thus consider that $P_2$ contains relations of the form (5.1). This of course makes the presentation infinite; however, these relations will be handled in a specific way, and we will only need to consider a finite number of those (by only considering “critical situations”).

**Remark 5.11.** In fact, it is easily shown that we can restrict to relations of the form (5.1) with $z_1, z_3$ and $z_4$ empty (all the others can be deduced). We will do so in the sequel in order to simplify computations.

As an illustrative example, we will study a presentation of a category simpler than the example of $\Delta \times \Delta$ mentioned in the introduction, in order to have a smaller number of conditions to check. We consider the category $\Delta_s$ whose objects are natural numbers $p \in \mathbb{N}$ and morphisms $f: p \to q$ are surjective functions $f: [p] \to [q]$, with $[p] = \{0, \dots, p-1\}$. As in the case of $\Delta$, this category is monoidal with tensor product given on objects by addition, and with 0 as neutral element (such a category is often called a PRO). As a simple variation on the example of $\Delta$, this category admits the following presentation.

**Lemma 5.12.** The category $\Delta_s$ admits the monoidal presentation $P$ with

$$P_0 = \{a\} \qquad P_1 = \{m : aa \to a\} \qquad P_2 = \{\alpha : m \circ (ma) \Rightarrow m \circ (am)\}$$

**Example 5.13.** We are interested in presenting the category $\Delta_s \times \Delta_s$ using a presentation modulo. For reasons explained in the introduction, it is natural to expect that this category admits the monoidal presentation modulo $P$ with generators

$$P_0 = \{a, b\} \qquad P_1 = \{m : aa \to a, n : bb \to b, g : ba \to ab\}$$

and relations in $P_2$ being

$$\alpha : m \circ (ma) \Rightarrow m \circ (am)$$

$$\beta : n \circ (nb) \Rightarrow n \circ (bn)$$

$$\gamma : g \circ bm \Rightarrow mb \circ ag \circ ga$$

$$\delta : g \circ na \Rightarrow an \circ gb \circ bg$$

(plus the mandatory exchange relations) which can be depicted, in categorical notation, as

<figure><img src="image_27.png" /></figure>
In string-diagrammatic notation, the generators $m, n$ and $g$ can be respectively drawn as

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

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

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

(the notation is the same for the first two, but the typing of wires makes the notation unambiguous), and the relations can be depicted as

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

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

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

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

The set of equational generators is $\tilde{P}_1 = \{g\}$.

First, consider Assumption 3.1 on our presentation modulo. The first condition of this assumption asserts that coinitial rewriting steps are confluent whenever one of them is equational. However, we now have a monoidal structure and the exchange axioms provide obvious ways to close diagrams in many cases. For instance, given an equational generator $f: x \to x'$ and a generator $g: y \to y'$, we can always show the confluence of the pair $(fy, xg)$ of coinitial morphisms:

$$ \begin{array}{ccc} x'y \xrightarrow{x'g} & x'y' & \\ fy \searrow & \xrel{\chi_{f,g}} & \searrow fy' \\ xy \underset{xg}{\stackrel{xy'}{\longrightarrow}} & & \end{array} \qquad (5.3) $$

Moreover, whenever there is a diagram as on the left, there is also one as on the right:

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

$$ \begin{array}{ccc} xy_1 z \xrightarrow{xg'z} & xy' z & \\ xfz \searrow & \xrel{x\alpha z} & \searrow xf'z \\ xyz \underset{xgz}{\stackrel{xy_2 z}{\longrightarrow}} & & \end{array} \qquad (5.4) $$

For this reason, one only has to ensure that diagrams can be closed for pairs of coinitial morphisms which are “minimal” (wrt left and right context) and not in exchange position. This observation is well-known in rewriting theory, and used to show that, in a string rewriting system, the confluence of critical pairs implies local confluence, which is reformulated in Lemma 5.17 below. This suggests adapting Assumption 3.1 as follows.

**Definition 5.14.** A pair of coinitial rewriting steps $f: x \to y$ and $g: x \to z$ is called a *critical pair* when
Its residuals with $bga: bbaa \to baba$ are

$$f/bga = mb \circ ag \circ ana \circ gba \qquad bga/f = g$$

the first one being computed by

$$ \begin{align*} (bm \circ naa)/bga &= (bm/(bga/naa)) \circ (naa/bga) = (bm/(bg/na)a) \circ (na/bg)a \\ &= (bm/ga) \circ (an \circ gb)a = mb \circ ag \circ ana \circ gba \end{align*} $$

using the residuation rules of Definition 3.3 and relations (5.6) (this is also illustrated in the third cylinder of Example 5.25). In string diagrammatic form, we have

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

Note that residuation is defined on rewriting paths (in $P_1^\otimes$), but we did not claim it was well-defined on morphisms in $P_1^*$. In fact, it is not generally compatible with exchange as we now illustrate. Obviously, the morphism $f$ above is equivalent, up to exchange, to the morphism $f' = na \circ bbm$. But the residuals $f/bga$ and $f'/bga$ are not:

$$f'/bga = an \circ gb \circ bmb \circ bbm$$

(see again Example 5.25 for details). Graphically,

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

We recall that, in order for the definition of residual to make sense (i.e. for Lemma 3.11 and Proposition 3.12 to hold), we need a termination assumption, which directly translates as follows in the monoidal setting:

**Assumption 5.19.** There is a weight function $\omega_1: P_0^*P_1P_0^* \to N$, where $N$ is a noetherian monoid, such that for every rewriting step $f \in P_0^*P_1P_0^*$ and $g \in P_0^*P_1P_0^*$, we have $\omega_1(g/f) < \omega_1(g)$, where we extend the weight as a function $\omega_1: P_1^\otimes \to N$ on rewriting paths by $\omega_1(g \circ f) = \omega_1(g) + \omega_1(f)$ and $\omega_1(\text{id}) = 0$.

**Example 5.20.** For our example, we define a weight function

$$\omega_1 : P_1^\otimes \to \mathbb{N} \times \mathbb{N}$$

with $\mathbb{N} \times \mathbb{N}$ equipped with the pointwise sum and lexicographic ordering. The weight is defined on rewriting steps by

- $\omega_1(xmy) = (p,0)$ where $p$ is the number of occurrences of $b$ in $x$,
- $\omega_1(xny) = (p, 0)$ where $p$ is the number of occurrences of $a$ in $y$,

- $\omega_1(xgy) = (0, q)$ where $q$ is the transposition number of $xy$.

It is easily checked that the residuals in (5.6) are strictly decreasing:

$$ (1,0) = \omega_1(bm) > \omega_1(bm/ga) = \omega_1(mb \circ ag) = (0,0) $$

$$ (1,0) = \omega_1(na) > \omega_1(na/bg) = \omega_1(an \circ gb) = (0,0) $$

Moreover, this also holds for the residuals along equational rewriting steps which are obtained by exchange cells, e.g. in

$$ \begin{array}{ccc} abxaa & \xrightarrow{abxm} & abxa \\ \multicolumn{1}{c}{\searrow} & & \searrow \\ g x a a & \xrightleftharpoons[\chi_{g x, m}]{\chi_{g x, m}} & g x a \\ \multicolumn{1}{c}{\searrow} & & \searrow \\ b a x a a & \xrightarrow{b a x m} & b a x a \end{array} $$

we have $\omega_1(baxm) > \omega_1(abxm)$ because the first component is the same but the transposition number decreases. Also, the order is compatible with left and right actions in the sense that $\omega_1(f) > \omega_1(g)$ implies $\omega_1(xfy) > \omega_1(xgy)$. Thus the weight $\omega_1$ fulfills our assumption.

**5.3. The cylinder property.** In the previous section, we have explained how the monoidal structure could help us to handle more easily the existence of residuals: one only has to ensure that they exist for critical pairs in order to have their existence for pairs of coinitial rewriting steps. The situation is very similar for the cylinder property. For instance, suppose that we have a cylinder as on the left.

$$ \begin{array}{ccc} & & \\ x' & \xrightarrow{g_1/f} & y' \\ \searrow f & & \searrow \\ & & \\ x & \xrightarrow{\alpha/f} & y \\ \searrow g_2/f & & \searrow \\ & & \\ g_1 & \xrightarrow{g_1} & y \\ \searrow x & & \searrow \\ & & \\ \alpha & \xrightarrow{g_2} & y \\ & & \searrow \\ & & \\ \end{array} $$

$$ \begin{array}{ccc} & & \\ zx'z' & \xrightarrow{z(g_1/f)z'} & zy''z' \\ \searrow zfz' & & \searrow \\ & & \\ zxz' & \xrightarrow{z(g_2/f)z'} & zy''z' \\ \searrow zg_1z' & & \searrow \\ & & \\ z\alpha z' & \xrightarrow{z\alpha z'} & zyz' \\ \searrow zg_2z' & & \searrow \\ & & \\ \end{array} $$

Then for every 0-cells $z$ and $z'$, we also have a cylinder as on the right, which shows that we only have to show the cylinder property for those which are minimal wrt contexts on the left and on the right.

Similarly, consider a situation as above where the bottom cell $\alpha$ is an exchange rule

$$ \chi_{g_1,g_2} : (y_1 g_2) \circ (g_1 x_2) \Rightarrow (g_1 y_2) \circ (x_1 g_2) : x_1 x_2 \rightarrow y_1 y_2 $$

with $g_1 : x_1 \rightarrow y_1$ and $g_2 : x_2 \rightarrow y_2$. Also, suppose that the vertical arrow on the left is of the form $fx_2 : x_1 x_2 \rightarrow x'_1 x_2$ with $f : x_1 \rightarrow x'_1$. In this case, one can always complete the cylinder on the left

$$ \begin{array}{ccc} & & \\ x'_1 x_2 & \xrightarrow{y_1 y_2} & \\ \searrow f x_2 & & \searrow \\ & & \\ x_1 x_2 & \xrightarrow{(y_1 g_2) \circ (g_1 x_2)} & y_1 y_2 \\ \searrow x_1 x_2 & \xrightarrow{\chi_{g_1,g_2}} & (g_1 y_2) \circ (x_1 g_2) \\ & & \searrow \\ & & \\ \end{array} $$

$$ \begin{array}{ccc} & & \\ x_1 x'_2 & \xrightarrow{y_1 y'_2} & \\ \searrow x_1 f & & \searrow \\ & & \\ x_1 x_2 & \xrightarrow{(y_1 g_2) \circ (g_1 x_2)} & y_1 (f/g_2) \\ \searrow x_1 x_2 & \xrightarrow{\chi_{g_1,g_2}} & (g_1 y_2) \circ (x_1 g_2) \\ & & \searrow \\ & & \\ \end{array} $$

as follows (the same argument will of course apply to a cylinder as on the right). We write

$$ \alpha : (g_1/f) \circ f \Rightarrow (f/g_1) \circ g_1 : x'_1 \rightarrow y'_1 $$
for the 2-cell mediating $f$ and $g_1$ with their residual, obtained by Assumption 3.1. The missing cells above are as follows:

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

**Remark 5.21.** The above diagram should be read as follows, in reference to the notations of the cylinder diagram on the left of (5.7) (we detail this here since this convention will be used again in the following). In the center of each picture on the left is figured the 2-cell $\alpha$ (which is here $\chi_{g_1/f,g_2}$), and the morphisms $f$ and $f/g_1 = f/g_2$ are represented horizontally as pointing to the left and the right, respectively. The rest of the picture on the left exhibits $g_1/f$ and $g_2/f$. The residual $\alpha/f$ is displayed on the matching picture on the right:

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

The “~” sign between the two diagrams indicates here that the diagram on the right is the “top” of the cylinder whose “bottom” and “walls” are shown on the left; it does not indicate an equality between cells, since the diagram on the left cannot be composed and thus does not even denote a 2-cell.

The above discussion motivates the introduction of the following definition and adaptation of the cylinder property.

**Definition 5.22.** Suppose given a morphism $f : x \to x'$ and a 2-cell $\alpha : g_1 \Rightarrow g_2 : x \to y$ in $P_0^*P_2P_0^*$ (consisting of one relation in context), as in the left of (5.7). Such a pair is *critical* when

- $f$ is different from both $g_1$ and $g_2$,

- it is minimal wrt contexts: if there is another such pair $(f', \alpha')$ and $z, z' \in P_0^*$ such that $f = zf'z'$ and $\alpha = z\alpha'z'$ then $z$ and $z'$ are both empty,

- it is not of the form (5.8).
**Remark 5.23.** The critical pairs, in the sense of the previous definition, can easily be computed by an adaptation of the usual critical pair algorithm for string rewriting systems. This is illustrated in Example 5.25.

**Assumption 5.24.** The presentation $(P, \tilde{P}_1)$ satisfies the cylinder property: for every rewriting step $f: x \to x'$ in $P_0^* \tilde{P}_1 P_0^*$ (resp. in $P_0^* P_1 P_0^*$) and 2-cell $\alpha: g_1 \Leftrightarrow g_2: x \to y$ in $P_0^* P_2 P_0^*$ with $g_1$ and $g_2$ in $P_0^* P_1 P_0^*$ (resp. $P_0^* \tilde{P}_1 P_0^*$) which are critical in the sense of Definition 5.22, we have $f/g_1 = f/g_2$ and there exists a 2-cell $g_1/f \Leftrightarrow g_2/f$. We write $\alpha/f$ for an arbitrary choice of such a 2-cell.

$$ \begin{tikzcd} & & \alpha/f \arrow[r, "g_1/f"] \arrow[d, "g_2/f"] & y' \arrow[d, "f/g_1=f/g_2"'] \\ x' \arrow[r, "g_1/f"] & y \arrow[d, "g_2"'] & & \\ f \arrow[r, "g_1"] & x \arrow[u, "\alpha"'] \arrow[r, "g_2"] & & \end{tikzcd} \qquad (5.9) $$

We have restricted the cylinder property to critical pairs in order to have less computations to perform, but the previous discussion shows that the cylinder property holds even for non-critical pairs when the assumption is valid.

**Example 5.25.** The presentation of Example 5.13 satisfies the cylinder property. The critical cylinder diagrams are

<figure><img src="image_40.png" /></figure>
<figure><img src="image_41.png" /></figure>

Let us explain how these were computed. Given a critical cylinder as in (5.9), either the
vertical morphism ($f$) or the horizontal arrows ($g_1$ and $g_2$ at the source and target of the
relation $\alpha$) are equational:

- if the vertical arrow is equational, then it is of the form $xgy : xbay \to xaby$; therefore the horizontal relation should have a 0-source which “intersects” $ba$ in a non-trivial way; this source thus either

- begins by an **a**: this gives rise to the first cylinder,

- ends by a **b**: this gives rise to the second cylinder, or

- contains $ba$: this gives rise to the third cylinder.

- if the horizontal arrows are equational, then the horizontal relation is necessarily an exchange between two morphisms of the form $xgy$, because no generating relation has equational source and target. We can then examine all the possibilities for $x$ and $y$, and vertical rewriting steps, and show that they are all trivial, for instance

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

are both of the form (5.8).

In order for the global cylinder property to hold (Proposition 3.14), we need again a
termination assumption, which can be reformulated as follows in the monoidal setting.

**Assumption 5.26.** There is a weight function $\omega_2 : P_0^* P_2 P_0^* \to N$, where $N$ is a noetherian commutative monoid, such that for every $\alpha : g_1 \Rightarrow g_2$ in $P_2$ and $f$ in $P_1$ such that $\alpha/f$ exists, we have $\omega_2(\alpha/f) < \omega_2(\alpha)$, where $\omega_2$ is extended to arbitrary 2-cells by acting the same on inverses, sending both compositions to addition and identities to the neutral element.

**Example 5.27.** Going back to Example 5.25, we define $\omega_2 : P_2 \to \mathbb{N} \times \mathbb{N}$ in a similar way as in Example 5.20 by

- $\omega_2(x\alpha y) = (p, 0)$ where $p$ is the number of occurrences of $b$ in $x$,

- $\omega_2(x\beta y) = (p, 0)$ where $p$ is the number of occurrences of $a$ in $y$,

- $\omega_2(x\chi y) = (0, q)$ where $q$ is the transposition number of $xy$.

It is easy to check that this interpretation is compatible with contexts, i.e. $\omega_2(\alpha) > \omega_2(\beta)$ implies $\omega_2(x\alpha y) > \omega_2(x\beta y)$, that the cylinders of Example 5.25 are strictly decreasing (the “top” is smaller than the “bottom”), and that residual of exchange relations are decreasing.
The global cylinder property follows from these assumptions (replacing $P_1^*$ by $\tilde{P}_1^\otimes$ in Proposition 3.14, see Example 5.18), as well as other properties mentioned in Section 3.2. Moreover, Theorem 4.2 holds in our context, in a way which is compatible with monoidal structure. Namely, the category of normal forms is monoidal with the tensor product defined on objects by

$$ \hat{x} \otimes \hat{y} = \hat{x}\hat{y} $$

and the action of objects $\hat{x}$ and $\hat{z}$ on a morphism $f : y \to y'$ is defined (similarly to the proof of Theorem 4.2) by

$$ \hat{x} \otimes f \otimes \hat{z} = u_{y''} \circ (\hat{x}f\hat{z}/u_{\hat{x}\hat{y}\hat{z}}) $$

where $y''$ is the target of $\hat{x}f\hat{z}/u_{\hat{x}\hat{y}\hat{z}}$. Graphically,

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

Similarly, the quotient category is monoidal as a quotient of a monoidal category by a congruence respecting tensor product.

**Theorem 5.28.** The canonical monoidal functor $\|P\|_{\downarrow \tilde{P}_1} \to \|P\|/\tilde{P}_1$ is a monoidal isomorphism of categories.

**5.4. The coherence theorem.** We can finally extend the coherence Theorem 4.5, by verifying that it is compatible with the monoidal structure of the categories:

**Theorem 5.29.** A presentation modulo $(P, \tilde{P}_2)$ which satisfies Assumptions 3.1 to 3.16 is coherent, in the sense that there exists a pair of functors

$$ F : \|P\|/\tilde{P}_1 \rightleftharpoons \|P\|[\tilde{P}_1^{-1}] : G $$

forming an equivalence of categories, with $F$ strong monoidal and $G$ strict monoidal.

*Proof.* The functors are constructed in the proofs of Theorems 4.2 and 4.5; we only have to check that they are monoidal. We have $F(I) = I$, so we can take $\eta = \mathrm{id}_I$. Given two objects $\hat{x}$ and $\hat{y}$ in $\|P\|_{\downarrow \tilde{P}_1}$ (which is monoidally isomorphic to $\|P\|/\tilde{P}_1$ by Theorem 5.28), we have $F(\hat{x}) \otimes F(\hat{y}) = \hat{x}\hat{y}$ and $F(\hat{x} \otimes \hat{y}) = \hat{x}\hat{y}$. There exists a normalization path $u : \hat{x}\hat{y} \to \hat{x}\hat{y}$ in $\|P\|$ and we define $\mu_{x,y} = Lu$, where $L : \|P\| \to \|P\|[\tilde{P}_1^{-1}]$ is the localization functor, and $\mu_{x,y}$ is invertible because $u$ is equational. The axioms for monoidal functors are easily verified by convergence of the equational rewriting system (Assumption 3.1). For instance, the first diagram of Definition 5.2 boils down to

<figure><img src="image_44.png" /></figure>
which follows from Newman’s Lemma 3.2. Conversely, the functor $G$ is defined on objects by $G(x) = \hat{x}$ so that we have $G(I) = I$ and

$$G(x) \otimes G(y) = \hat{x}\hat{y} = \widehat{xy} = G(x \otimes y)$$

from which we deduce that we can take $\eta = \mathrm{id}_I$ and $\mu_{x,y} = \mathrm{id}_{\widehat{xy}}$.

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

In particular, the presentation of Example 5.13 is coherent.

**5.5. A variant of the cylinder property.** As we saw in Example 5.18, residuation is not in general compatible with exchange, so that we cannot expect the cylinder property (and Assumption 3.13 in particular) to hold in every case. In fact, a reasonable generalization of the global cylinder property (Proposition 3.14) could be: given coinitial morphisms $f: x \to x'$ in $\tilde{P}_1^*$ (resp. in $P_1^*$) and $g_1, g_2: x \to y$ in $P_1^*$ (resp. in $\tilde{P}_1^*$) such that there exists a composite 2-cell $\alpha: g_1 \overset{*}{\Leftrightarrow} g_2$, we have $f/g_1 \overset{*}{\Leftrightarrow} f/g_2$ and there exists a 2-cell $g_1/f \overset{*}{\Leftrightarrow} g_2/f$.

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

Note that we do not require $g_1/f$ and $g_2/f$ to be equal, but only merely equivalent. However, such a general global cylinder property seems to be difficult to be deduced from a local property that would generalize Assumption 3.13 and could easily be checked in practice, so that we have to restrict to particular cases for now. As an illustration, in this section, we study the dual of the presentation modulo of Example 5.13 and show that it can be handled using a different local cylinder property.

**Example 5.30.** We write now $P$ for the opposite of the presentation of Example 5.13: it has $P_0 = \{a, b\}$ as set of generators for objects and the generators for morphisms are the dual of those of Example 5.13 (we write $\bar{f}$ for the dual of a generator $f$):

$$P_1 = \{\bar{m} : a \to aa, \bar{n} : b \to bb, \bar{g} : ab \to ba\}$$

where $\bar{g}$ is the only equational generator: $\tilde{P}_1 = \{\bar{g}\}$. We would like to show that this presentation satisfies Assumptions 3.1 to 3.16, in order to be able to apply our main Theorem 5.29. Notice that, here, it is important that the termination assumptions are restricted to equational morphisms, since there is no hope to have a terminating rewriting system with all generators. For instance, we have

$$a \xrightarrow{\bar{m}} aa \xrightarrow{\bar{m}a} aaa \xrightarrow{\bar{m}aa} aaaa \xrightarrow{\cdots} \dots$$

The relations in $P_2$ are the dual of those of Example 5.13:

$$\bar{\alpha} : \bar{m}a \circ \bar{m} \Rightarrow a\bar{m} \circ \bar{m}$$

$$\bar{\beta} : \bar{n}b \circ \bar{n} \Rightarrow b\bar{n} \circ \bar{n}$$

$$\bar{\gamma} : b\bar{m} \circ \bar{g} \Rightarrow \bar{g}a \circ a\bar{g} \circ \bar{m}b$$

$$\bar{\delta} : \bar{n}a \circ \bar{g} \Rightarrow b\bar{g} \circ \bar{g}b \circ a\bar{n}$$

The orientation of the source (resp. target) cell has been reversed, and the orientation of the relation does not really matter here since we are interested in the generated equivalence
relation (here, we chose to keep the same orientation). Assumption 3.1 can be checked by
constructing the two critical residuation squares:

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

Termination of the equational rewriting system is easily checked using a transposition number as before (counting now the number of occurrences of *b* after occurrences of *a*). Assumption 3.6 can be checked by a variation of Example 5.20 (obtained by exchanging the role of *a* and *b* in $\omega_1$). However, there is no hope that Assumption 3.13 will hold. Namely, consider the “cylinder” formed by $\bar{g}$ and $\chi_{\bar{m},\bar{n}}$ as depicted below:

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

This is not a proper cylinder because we have

$$
\overline{g} / (a \overline{a} \circ \overline{m} b) = b \overline{g} a \circ \overline{g} b a \circ a b \overline{g} \circ a \overline{g} b \neq b \overline{g} a \circ b a \overline{g} \circ \overline{g} a b \circ a \overline{g} b = \overline{g} / (\overline{m} b b \circ a \overline{n})
$$

The two morphisms in the middle are not equal, they are only equivalent up to exchange (up to the relation $\stackrel{\wedge}{\alpha}$). Also notice that the residual of the exchange relation $\chi_{\bar{m},\bar{n}}$ after $\bar{g}$ is an exchange relation ($\chi_{\bar{n},\bar{m}}$ as pictured on the right in the above figure).

This example suggests modifying Assumption 3.13 to
**Assumption 5.31.** The presentation $(P, \tilde{P}_1)$ satisfies the following conditions.

(1) The cylinder property holds up to $\mathrel{\Leftrightarrow}$: for every rewriting step $f: x \to x'$ in $P_0^* \tilde{P}_1 P_0^*$ (resp. in $P_0^* P_1 P_0^*$) and 2-cell $\alpha: g_1 \Leftrightarrow g_2: x \to y$ in $P_0^* P_2 P_0^*$ with $g_1$ and $g_2$ in $P_0^* P_1 P_0^*$ (resp. $P_0^* \tilde{P}_1 P_0^*$) which are critical in the sense of Definition 5.22, we have $f/g_1 \mathrel{\Leftrightarrow} f/g_2$ and there exists a 2-cell $g_1/f \mathrel{\Leftrightarrow} g_2/f$. We write $\alpha/f$ for an arbitrary choice of such a 2-cell.

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

(2) Residuation is compatible with the relation $\mathrel{\Leftrightarrow}$: in the cases above where $\alpha$ is an exchange cell in context, its residual $\alpha/f$ is also a composite of exchange cells in context.

Note that the second condition implies that we can consider morphisms up to exchange, and compute their residuals:

**Lemma 5.32.** For every coinitial morphisms $f, f'$ and $g, g'$ such that $f \mathrel{\Leftrightarrow} f'$ and $g \mathrel{\Leftrightarrow} g'$, with $f$ and $f'$ equational, we have $g/f \mathrel{\Leftrightarrow} g'/f'$.

**Remark 5.33.** In the presentation of Example 5.13, residuation is not compatible with exchange because the last cylinder of Example 5.25 shows that an exchange relation can have a residual which does not consist of exchange relations (in context) only. Thus, while first condition of Assumption 5.31 is a relaxed version of Assumption 3.13, the second condition is a strengthening, and the two assumptions are thus incomparable.

**Example 5.34.** In our Example 5.30, one easily checks that the only critical cylinder is (5.10). The only residuals of exchange relations are thus of the form (5.8) (in context) and are therefore exchange relations in context: residuation is compatible with $\mathrel{\Leftrightarrow}$. As mentioned before, the critical cylinder (5.10) is of the right shape, up to exchange. For the termination Assumption 3.16, we distinguish two cases depending on whether the vertical arrow is equational or not, as explained in Remark 3.18. When the vertical arrow is equational (i.e. of the form $x \bar{g} y$), termination is shown using the variant of Example 5.27 obtained by exchanging the role of $a$ and $b$ in $\omega_2$. However, this same weight $\omega_2$ will not work when the vertical arrow is not equational. For instance, the residual of the relation

$$ab\chi_{\bar{g},\bar{g}} : \text{abba}\bar{g} \circ \text{abg}ab \Rightarrow \text{abg}ba \circ \text{abab}\bar{g} : \text{ababab} \rightarrow \text{abbaba}$$

after the morphism

$$\bar{m}babab : \text{ababab} \rightarrow \text{aababab}$$

is

$$aab\chi_{\bar{g},\bar{g}} : \text{aabba}\bar{g} \circ \text{aabg}ab \Rightarrow \text{aabg}ba \circ \text{aabab}\bar{g} : \text{aababab} \rightarrow \text{aabbaba}$$

and we have

$$(0,1) = \omega_1(ab\chi_{\bar{g},\bar{g}}) \not\supseteq \omega_1(aab\chi_{\bar{g},\bar{g}}) = (0,2)$$

Intuitively, in $ab\chi_{\bar{g},\bar{g}}$ there is one transposition left to do in the context, whereas after residuation the $a$ was duplicated and therefore there are two transpositions left in the context in $aab\chi_{\bar{g},\bar{g}}$. However, it can be noticed that in cases of the form (5.8) (in context) the residual
of the vertical rewriting step is always a rewriting step (as opposed to a rewriting path) and therefore the global cylinder property can be shown as explained in Remark 3.18. Finally, it can be shown as in Theorem 5.29 that the presentation modulo $(P, \tilde{P}_1)$ is coherent.

## 6. CONCLUSION

We have introduced a notion of presentation of a (monoidal) category modulo an “equational” rewriting system, and provided coherence conditions ensuring that the equational rules are well-behaved wrt the generators. In particular, we show that, under those assumptions, all the three possible natural constructions for the presented category are equivalent. These assumptions are “local” in the sense that they are given directly on the presentations, and can thus be used in practice in order to perform computations, as illustrated in the article. A more general theory of situations where quotient coincides with localization is left for future work.

In the future, we would like to investigate more applications, by studying generic situations. For instance, given two monoidal categories with a coherent presentation, can we always construct a monoidal presentation of their product? Having more illustrative examples is also important to evaluate how generic the assumptions we proposed are. As we have explained in Section 5.3, the general methodology seems to be quite stable, but there are many possible local conditions in order to implement it (e.g. local cylinder assumptions such as Assumptions 3.13 or 5.31 in order to show the global cylinder property). In particular, we would like to have more general conditions which would encompass both Assumptions 3.13 and 5.31. On the practical side, it would be interesting to study extensions of the Knuth-Bendix procedure which could transform a presentation in order to hopefully complete it into one satisfying our assumptions. Finally, we would like to study applications to coherence of various algebraic structures: presentations modulo allow one to turn some of the generators into isomorphisms, while remaining equivalent to the situation where those generators are identities, which is what the coherence theorems (such as MacLane’s theorem for monoidal categories) ensure, in a slightly different formal context.

## REFERENCES

[1] F. Baader and T. Nipkow. *Term rewriting and all that*. Cambridge University Press, 1999.

[2] M. A. Bednarczyk, A. M. Borzyszkowski, and W. Pawlowski. Generalized Congruences – Epimorphisms in Cat. *Theory and Applications of Categories*, 5(11):266–280, 1999.

[3] M. Bezem, J. W. Klop, and R. de Vrijer. *Term rewriting systems*. Cambridge University Press, 2003.

[4] F. Borceux. *Handbook of Categorical Algebra 1. Basic Category Theory*. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.

[5] A. Burroni. Higher-dimensional word problems with applications to equational logic. *Theoretical computer science*, 115(1):43–62, 1993.

[6] F. Clerc and S. Mimram. Presenting a Category Modulo a Rewriting System. In *LIPIcs-Leibniz International Proceedings in Informatics*, volume 36. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015.

[7] B. Day. Note on monoidal localisation. *Bulletin of the Australian Mathematical Society*, 8(01):1–16, 1973.

[8] P. Dehornoy. On completeness of word reversing. *Discrete Mathematics*, 225(1):93–119, 2000.

[9] P. Dehornoy, F. Digne, E. Godelle, D. Krammer, and J. Michel. *Foundations of Garside theory*, volume 22 of *EMS tracts in mathematics*. European Mathematical Society, 2015.

[10] P. Gabriel and M. Zisman. *Calculus of fractions and homotopy theory*, volume 6. Springer, 1967.
[11] Y. Guiraud and P. Malbos. Polygraphs of finite derivation type. *arXiv:1402.2587*, 2014. To appear in *Mathematical Structures in Computer Science*.

[12] Y. Guiraud, P. Malbos, and S. Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids. In *RTA - 24th International Conference on Rewriting Techniques and Applications*, volume 21, pages 223-238, 2013.

[13] G. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. *Journal of the ACM (JACM)*, 27(4):797-821, 1980.

[14] Y. Lafont. Towards an algebraic theory of boolean circuits. *Journal of Pure and Applied Algebra*, 184(2):257-310, 2003.

[15] J.-J. Lévy. *Réductions correctes et optimales dans le lambda-calcul*. PhD thesis, Université Paris VII, 1978.

[16] S. Mac Lane. *Categories for the working mathematician*, volume 5. Springer, 1998.

[17] S. Mimram. Towards 3-Dimensional Rewriting Theory. *Logical Methods in Computer Science*, 10(1):1-47, 2014.

[18] M. H. A. Newman. On theories with a combinatorial definition of "equivalence". *Annals of mathematics*, pages 223-243, 1942.

[19] A. J. Power. An *n*-categorical pasting theorem. In *Category theory*, pages 326-358. Springer, 1991.

[20] J. Power and E. Robinson. Premonoidal categories and notions of computation. *Mathematical structures in computer science*, 7(05):453-468, 1997.

[21] R. Street. Limits indexed by category-valued 2-functors. *Journal of Pure and Applied Algebra*, 8(2):149-181, 1976.

[22] H. Tietze. Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten. *Monatshefte für Mathematik und Physik*, 19(1):1-118, 1908.