# Coherence of Gray Categories via Rewriting

Simon Forest, Samuel Mimram

► To cite this version:

Simon Forest, Samuel Mimram. Coherence of Gray Categories via Rewriting. 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Jul 2018, Oxford, United Kingdom. 10.4230/LIPIcs.FSCD.2018.15 . hal-02154822

HAL Id: hal-02154822

https://hal.science/hal-02154822

Submitted on 17 Jun 2019

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Coherence of Gray Categories via Rewriting

## Simon Forest

LIX, École Polytechnique, France
simon.forest@lix.polytechnique.fr

## Samuel Mimram

LIX, École Polytechnique, France
samuel.mimram@lix.polytechnique.fr

## Abstract

Over the recent years, the theory of rewriting has been extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to low-dimensional weak categories, and consider in details the first non-trivial case: presentations of tricategories. By a general result, those are equivalent to the stricter Gray categories, for which we introduce a notion of rewriting system, as well as associated tools: critical pairs, termination orders, etc. We show that a finite rewriting system admits a finite number of critical pairs and, as a variant of Newman's lemma in our context, that a convergent rewriting system is coherent, meaning that two parallel 3-cells are necessarily equal. This is illustrated on rewriting systems corresponding to various well-known structures in the context of Gray categories (monoids, adjunctions, Frobenius monoids). Finally, we discuss generalizations in arbitrary dimension.

**2012 ACM Subject Classification** Theory of computation → Rewrite systems

**Keywords and phrases** rewriting, coherence, Gray category, polygraph, pseudomonoid, precategory

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2018.15

The rewriting systems which are convergent have a fundamental property, which is a consequence of Newman's and other classical lemmas in rewriting theory: the space between any two rewriting zigzags with the same source and the same target can be filled with tiles witnessing the confluence of critical branchings. Otherwise said, every diagram commutes modulo the commutation of diagrams induced by critical branchings, which thus axiomatize the coherence of the structure.

Over the recent years, there have been many efforts to generalize the techniques of rewriting from words and terms to morphisms in strict *n*-categories, starting from the pioneering work of Burroni and Lafont [3, 15, 16]. Those widen the range of applicability of rewriting, and also allow a precise formulation of the above remark initially formulated by Squier, and generalized by Guiraud and Malbos by considering coherent presentations [17, 8, 9]. As a typical example, starting from the 2-category of planar binary forests, which is generated by a binary ($\mu$) and a nullary corolla ($\eta$), one can consider rewriting rules expressing the fact that $\mu$ is associative and $\eta$ is both a left and right unit for $\mu$. The resulting rewriting system is convergent, and the technique described above allows to prove a coherence theorem for pseudomonoids, of which MacLane's coherence result is a particular case (a monoidal category is a pseudomonoid in the cartesian 2-category **Cat**).

It is of course of interest to generalize the coherence theorems for classical algebraic structures from strict to weak *n*-categories. For instance, coherence for pseudomonoids in tricategories is shown in [14]. A rewriting approach in this domain is desirable, but the way one could handle all the coherence morphisms present in weak categories was not

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

© Simon Forest and Samuel Mimram;
licensed under Creative Commons License CC-BY

3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018).

Editor: Hélène Kirchner; Article No. 15; pp. 15:1–15:16

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
15:2 Coherence of Gray Categories via Rewriting

clear. Recently, the use of semistRICT weak *n*-categories was advocated by the creators of the
graphical proof-assistant Globular [1, 2] as a formalism adapted to computer manipulations:
without loss of generality most of the coherence morphisms can be considered to be identities,
excepting the interchangers and their coherences.

In this article, we develop the theory of rewriting for semistRICT 3-categories, also called
Gray categories, which is the first dimension in which the strict and weak definitions are
not equivalent [6, 11]. We illustrate that this provides systematic principles for proving
coherence of algebraic structures in Gray categories, allowing us to recover results in this
direction recently proved [14, 4, 20] as well as new ones. Moreover, it turns out that this
weak framework is better behaved than the strict one in some respects: it was observed
that a finite rewriting system on strict 2-morphisms can give rise to an infinite number of
critical branchings [15, 8], which is the source of many difficulties [16], both of theoretical and
practical nature, whereas in the present setting we show that only a finite number of critical
pairs can be generated. Finally, we also hint at generalizations in arbitrary dimension.

1 Coherent presentations of Gray categories

1.1 Sesquicategories

We begin by recalling the notion of 2-category as a variant of sesquicategories, details can be
found in [18]. A *sesquicategory*, or *2-precategory*, *C* consists of

a set $C_0$ of 0-cells,

a set $C_1(x, y)$ of 1-cells $u : x \to y$ for every 0-cells $x$ and $y$,

a set $C_2(u, v)$ of 2-cells $\alpha : u \Rightarrow v : x \to y$ every parallel 1-cells $u, v : x \to y$,

an identity 1-cell $1_x : x \to x$ for every 0-cell $x$,

a composition function which to every 1-cells $u : x \to y$ and $v : y \to z$ associates a 1-cell
$u * v : x \to y$,

an identity 2-cell $1_u : u \Rightarrow u$ for every 1-cell $u$,

a *vertical* composition function which to every 2-cell $\alpha : v \Rightarrow v'$ and $\beta : v' \Rightarrow v''$ associates a 2-cell $\alpha * \beta : v \Rightarrow v''$ (middle of (1)),

a left whiskering composition function which to every 1-cell $u : x' \to x$ and 2-cell $\alpha : v \Rightarrow v'$ associates a 2-cell $u * \alpha : u \Rightarrow v \Rightarrow u * v' : x \to y'$ (left of (1)),

a right whiskering composition function which to every 2-cell $\alpha : v \Rightarrow v'$ and 1-cell $w : y \to y'$ associates a 2-cell $\alpha * w : v \Rightarrow w \Rightarrow v' * w : x \to y'$ (right of (1)).

$$
x' \xrightarrow{u} x \underset{v'}{\overset{v}{\rightleftarrows}} y \qquad x \underset{v''}{\overset{v}{\rightleftarrows}} \underset{v'}{\underset{v'}{\rightleftarrows}} y \qquad x \underset{v'}{\overset{v}{\rightleftarrows}} y \xrightarrow{w} y' \qquad (1)
$$

such that compositions are associative and admit identities as neutral elements: for suitably
typed 0-cells $x, y$, 1-cells $u, v, w$ and 2-cells $\alpha, \beta, \gamma$,

$$
\begin{align*}
(u * v) * w &= u * (v * w) & 1_x * u &= u & u * 1_y &= u \\
(\alpha * \beta) * \gamma &= \alpha * (\beta * \gamma) & 1_u * \alpha &= \alpha & \alpha * 1_v &= \alpha \\
u * (\alpha * \beta) &= (u * \alpha) * (u * \beta) & u * 1_v &= 1_{u*v} & (\alpha * \beta) * w &= (\alpha * w) * (\beta * w) & 1_v * w &= 1_{v*w} \\
(u * v) * \alpha &= u * (v * \alpha) & 1_x * \alpha &= \alpha & \alpha * (v * w) &= (\alpha * v) * w & \alpha * 1_y &= \alpha \\
(u * \alpha) * w &= u * (\alpha * w) & & & & & & (2)
\end{align*}
$$

In a composition, the dimension of the involved cells determines which composition is used,
which allows us to unambiguously denote them by the same symbol. In a more terse way,
the category of sesquicategories can be defined as the category of categories enriched over **Cat** equipped with the “funny tensor product” [5].

A 2-category *C* is a sesquicategory such that the interchange law holds: this means that for every 2-cells $\alpha : u \Rightarrow u' : x \to y$ and $\beta : v \Rightarrow v' : y \to z$, we have

$$ (\alpha * v) * (u' * \beta) = (u * \beta) * (\alpha * v') \quad \xrightarrow[\alpha]{v} \quad \xrightarrow[\beta]{u'} \quad \xrightarrow{z} \quad \xrightarrow[\beta]{v'} \quad \xrightarrow{u'} \quad \xrightarrow[\alpha]{v} \quad \xrightarrow{z} \quad (3) $$

Since both of the above compositions are equal, we can define the 0-composition of $\alpha$ and $\beta$ to be either of them. By contrast, in a sesquicategory, the 0-composition of 2-cells does not make sense: we can only compose 2-cells in codimension 1.

## 1.2 Signatures

In the following, we will be interested in rewriting morphisms in freely generated sesquicategories. Recall that a *graph* consists of

- a set $P_0$ of vertices,

- a set $P_1$ of edges,

- functions $s_0, t_0 : P_1 \to P_0$ associating to each edge its source and target vertex.

We write $P_1^*$ for the set of paths in the graph, $s_0^*, t_0^* : P_1^* \to P_0$ the source and target functions on paths, and $uv$ for the concatenation of composable paths $u$ and $v$.

A *signature* $P$ consists of

- a graph $(P_0, s_0, t_0, P_1)$ whose vertices and edges are called 0- and 1-generators,

- a set $P_2$ of 2-generators together with functions $s_1, t_1 : P_2 \to P_1^*$ such that $s_0^* \circ s_1 = s_0^* \circ t_1$ and $t_0^* \circ s_1 = t_0^* \circ t_1$.

We write $a : x \to y$ to indicate that $a$ is a 1-generator with $s_0(a) = x$ and $t_0(a) = y$, and similarly for 2-generators $\alpha : u \Rightarrow v$ with $s_1(\alpha) = u$ and $t_1(\alpha) = v$.

**Example 1 (Monoids).** The signature for *monoids* is

$$ P_0 = \{\star\} \qquad P_1 = \{1 : \star \to \star\} \qquad P_2 = \{\mu : 2 \Rightarrow 1, \eta : 0 \Rightarrow 1\} $$

Note that the set $P_1^*$ is isomorphic to $\mathbb{N}$, thus the notation for its elements. The 2-generators of this signature should respectively be understood as a formal multiplication $(\mu)$ and unit $(\eta)$, which we will use below to express the structure of a monoid.

A signature $P$ freely generates a sesquicategory with $P_0$ as 0-cells, $P_1^*$ as 1-cells (composition being concatenation and identities empty paths), and whose 2-cells are generated by $P_2$. We write $P_2^*$ for its set of 2-cells, whose elements can be described explicitly as follows.

**Proposition 2.** The 2-cells in $P_2^*$ can be described as the sequences of the form

$$ (u_1 * \alpha_1 * w_1) * (u_2 * \alpha_2 * w_2) * \dots * (u_n * \alpha_n * w_n) $$

with $u_i : x \to x_i$ in $P_1^*$, $\alpha_i : v_i \Rightarrow v'_i : x_i \to y_i$ in $P_2$, $w_i : y_i \to y$ in $P_1^*$ (the compositions above are formal ones). The canonical inclusion $P_2 \to P_2^*$ sends a 2-generator $\alpha : u \Rightarrow v : x \to y$ to $(1_x * \alpha * 1_y)$, vertical composition is given by concatenation, left whiskering the above morphism by $u$ amounts to replace each $u_i$ by $uu_i$, and similarly for right whiskering.

**Proof.** The above sequences are the normal forms for a suitable orientation of the relations (2) as a convergent rewriting system on formal expressions. $\blacksquare$

<figure><img src="image_4.png" /></figure>
15:4 Coherence of Gray Categories via Rewriting

As customary, such morphisms can be pictured using string diagrams. For instance, in the signature of monoids (Ex. 1), if we draw $\mu$ by $\triangleright$, we can picture the following morphisms:

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

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

Note that in these pictures, there can be only one generator at a given height, and the relative heights matter, so that the two 2-cells are not considered to be equal (contrarily to 2-categories).

1.3 Rewriting systems

A *rewriting system* consists of a signature $\mathbf{P}$ together with a set $\mathbf{P}_3$ of 3-generators, or *rewriting rules*, equipped with source and target functions $s_2, t_2 : \mathbf{P}_3 \to \mathbf{P}_2^*$. A *rewriting step*

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

$$ \chi_- * (u * A * v) * \chi_+ : \chi_- * (u * \phi * v) * \chi_+ \Rightarrow \chi_- * (u * \psi * v) * \chi_+ $$

consists of a rewriting rule $A : \phi \Rightarrow \psi : v_- \Rightarrow v_+ : x \to y$ together with 1-cells $u : x' \to x$, $v : y \to y'$ and 2-cells $\chi_- : v_- \Rightarrow v_-$, $\chi_+ : v_+ \Rightarrow v'_+$ as on the right above. A *rewriting path* is a finite sequence of composable rewriting steps $R_i : \phi_i \Rightarrow \psi_i$, with $\phi_{i+1} = \psi_i$.

► **Example 3.** The rewriting system for monoids has, on the signature of Ex. 1, the rules

$$ A : (\mu * 1) * \mu \Rightarrow (1 * \mu) * \mu $$

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

$$ L : (\eta * 1) * \mu \Rightarrow \mu $$

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

$$ R : (1 * \eta) * \mu \Rightarrow \mu $$

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

There is, for instance, a rewriting step

$$ (3 * \mu * 1) * (1 * A * 1) * ((\mu * 1) * \mu) : $$

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

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

We write $\mathbf{P}_3^*$ for the set of rewriting paths, and $s_2^*, t_2^* : \mathbf{P}_3^* \to \mathbf{P}_2^*$ for the associated source and target functions. We can form a 3-precategory, noted $\mathbf{P}^*$, with $\mathbf{P}_i^*$ as $i$-cells for $i = 0, 1, 2, 3$ (by convention $\mathbf{P}_0^* = \mathbf{P}_0$) and expected compositions. The notion of 3-precategory will be detailed in Sec. 4.1, but we can already say that it is the expected generalization of 2-precategories (see Sec. 1.1) in dimension 3: a *3-precategory* consists of a set $C_i$ of $i$-cells for $i = 0, 1, 2, 3$ together with their source and target in lower dimension (except for 0-cells), identities for 0, 1, 2-cells, and compositions between composable $i$- and $j$-cells, with $i, j = 1, 2, 3$, so that compositions are associative and unital in a suitable way. Note that, contrarily to 3-categories, there is only one kind of composition between $i$- and $j$-cells: those can only be composed in codimension $i \wedge j - 1$ (we write $i \wedge j$ for the minimum of $i$ and $j$), which again allows to unambiguously use the same symbol for all compositions. A morphism of 3-precategories is called a *3-prefunctor*. By generalizing the argument of Prop. 2, one can show that $\mathbf{P}^*$ enjoys the following universal property, see Sec. 4.2 for details:

► **Proposition 4.** The 3-precategory $\mathbf{P}^*$ is the free 3-precategory whose underlying 2-precategory is the one generated by the underlying signature of $\mathbf{P}$ and containing the rewriting rules as 3-cells.
Following the terminology of [9], we say that two rewriting paths $P$ and $Q$ are Peiffer-equivalent when they differ only by successively permuting adjacent rewriting steps at disjoint positions, what we write $P \equiv Q$ below. For instance, with the notations of Ex. 3, the two following paths are Peiffer-equivalent:

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

More generally, we can define the Peiffer-equivalence in a 3-precategory as the smallest congruence (w.r.t. compositions) such that, with cells as on the left, we have the relation on the right:

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

## 1.4 (3,2)-precategories

A (3, 2)-precategory is a 3-precategory in which every 3-cell $P: \phi \Rightarrow \psi$ is invertible: there exists a 3-cell $Q: \psi \Rightarrow \phi$ such that $P * Q = 1_\phi$ and $Q * P = 1_\psi$.

Given a rewriting system $P$, consider the rewriting system $Q$ with $Q_i = P_i$ for $i = 0, 1, 2$ and $Q_3 = P_3 \sqcup P_3^-$ where $P_3^- = \{A^- : \psi \Rightarrow \phi \mid A : \phi \Rightarrow \psi \in P_3\}$ is the set of formally reverted rules in $P_3$. We write $P_3^\top$ for the set of 3-cells in $Q_3^*$ quotiented by the smallest congruence such that $A * A^- = 1_\phi$ and $A^- * A = 1_\psi$ for every generator $A$ in $P_3$, and call its elements rewriting zigzags. We can form a 3-precategory, noted $P^\top$, with $P_i^*$ as $i$-cells for $i = 0, 1, 2$, $P_3^\top$ as 3-cells, and expected compositions: it is defined as $P^*$ excepting that 3-cells are rewriting zigzags instead of rewriting paths.

**Proposition 5.** The 3-precategory $P^\top$ is the free (3, 2)-precategory on the 3-precategory $P^*$.

According to the above proposition, we generalize the above notation and write $P^-$ for the inverse of an arbitrary 3-cell $P$. Note that any 3-cell decomposes as $P_1^- * Q_1 * \dots * P_n^- * Q_n$ where $P_i$ and $Q_i$ are rewriting paths (thus the terminology of rewriting zigzag). In the following, we will be mostly interested in (3, 2)-precategories (as opposed to 3-precategories).

## 1.5 Presentations

In order to describe interesting 3-precategories using rewriting systems, we need to be able to quotient the 3-cells in the freely generated 3-precategory. A *presentation* consists of a rewriting system $P$ equipped with a set $P_4$ of *relations* together with functions $s_3, t_3 : P_4 \to P_3^\top$ indicating the source and the target rewriting path of a relation, such that $s_2^* \circ s_3 = s_2^* \circ t_3$ and $t_2^* \circ s_3 = t_2^* \circ t_3$ (relations are between rewriting paths with same source and same target). We often write $\Gamma : P \Rightarrow Q$ to indicate that $\Gamma$ is a relation with $s_3(\Gamma) = P$ and $t_3(\Gamma) = Q$. We denote by $\equiv_{P_4}$ (or sometimes even $\equiv$), the smallest congruence on 3-cells in $P_3^\top$ such that $P \equiv_{P_4} Q$ for every relation $\Gamma : P \Rightarrow Q$ in $P_4$.

The (3, 2)-precategory $\bar{P}$ presented by a presentation $P$ is the 3-category obtained from $P^\top$ by quotienting 3-cells under $\equiv_{P_4}$.
2. for every 2-generators $\alpha$ and $\beta$ and 1-cell $v$ as below:

$$x \underset{u'}{\overset{u}{\rightleftharpoons}} x' \xrightarrow{v} y' \underset{w'}{\overset{w}{\rightleftharpoons}} z$$

left, there is a 3-generator $X_{\alpha,v,\beta}$, called interchange generators, as below:

$$X_{\alpha,v,\beta}: \quad (\alpha * v * w) * (u' * v * \beta) \Rightarrow (u * v * \beta) * (\alpha * v * w') \\ x \underset{u'}{\overset{u}{\rightleftharpoons}} x' \xrightarrow{v} y' \underset{w'}{\overset{w}{\rightleftharpoons}} z \Rightarrow x \underset{u'}{\overset{u}{\rightleftharpoons}} x' \xrightarrow{v} y' \underset{w'}{\overset{w}{\rightleftharpoons}} z$$

and we write $P_X \subseteq P_3$ for the set of interchange generators,

3. for every 3-generator $A$, 1-cell $v$ and 2-generator $\alpha$ as on the left or on the right below

$$x \underset{u'}{\overset{u}{\rightleftharpoons}} \underset{w'}{\overset{w}{\rightleftharpoons}} \psi x' \xrightarrow{v} y' \underset{w'}{\overset{w}{\rightleftharpoons}} y \qquad x \underset{u'}{\overset{u}{\rightleftharpoons}} \underset{w'}{\overset{w}{\rightleftharpoons}} \alpha x' \xrightarrow{v} y' \underset{w'}{\overset{w}{\rightleftharpoons}} \psi y \quad (6)$$

there is respectively a relation, called interchange naturality generator,

$$((A * v * w) * (u' * v * \alpha)) * X_{\psi,v*\alpha} \Rightarrow X_{\phi,v*\alpha} * ((u * w * \alpha) * (A * v * w'))$$

$$((\alpha * v * w) * (u' * v * A)) * X_{\alpha * v, \psi} \Rightarrow X_{\alpha * v, \phi} * ((u * v * A) * (\alpha * v * w'))$$

where the interchangers $X_{\alpha * v, \psi}$ are suitable composite of interchange generators (see proposition below).

The above families of 3- and 4-cells are called the structural generators of the presentation. We will not insist much about it in the following, but the choice of structural cells is implicitly supposed to be part of a Gray presentation.

**► Proposition 7.** Given a Gray presentation $P$, the presented (3,2)-precategory $\bar{P}$ is canonically a Gray (3,2)-category.

**Proof sketch.** The first family of relations of $P$ generates, by congruence, all the Peiffer equivalences, the second family of 3-cells generates, by composition, all the interchangers, and the third family of relations generates, by congruence, all the naturality conditions. ◀

**► Example 8.** The Gray presentation of monoids consists of the rewriting system of Ex. 3, as well as additional interchange generators

$$\begin{tikzpicture}[baseline=(current bounding box.center)]
\node (A) at (0,0) {$\begin{tikzpicture}[baseline=(current bounding box.center)]
  \draw (0,0) -- (0,1) -- (1,1) -- (1,0) -- cycle;
  \node at (0.5,0.5) {$\rightarrow$};
  \node at (0.5,1) {$\rightarrow$};
  \node at (1.5,0.5) {$\rightarrow$};
  \node at (1.5,1) {$\rightarrow$};
  \node at (0.25,0.25) {$\rightarrow$};
  \node at (0.25,0.75) {$\rightarrow$};
  \node at (1.25,0.25) {$\rightarrow$};
  \node at (1.25,0.75) {$\rightarrow$};
  \node at (0.5,0.5) {$\Rightarrow$};
  \node at (0.5,1) {$\Rightarrow$};
  \node at (1.5,0.5) {$\Rightarrow$};
  \node at (1.5,1) {$\Rightarrow$};
  \node at (0.25,0.25) {$\Rightarrow$};
  \node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}$};
\node at (0.5,0.5) {$\Rightarrow$};
\node at (0.5,1) {$\Rightarrow$};
\node at (1.5,0.5) {$\Rightarrow$};
\node at (1.5,1) {$\Rightarrow$};
\node at (0.25,0.25) {$\Rightarrow$};
\node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}}$$

together with the relations

$$\begin{tikzpicture}[baseline=(current bounding box.center)]
\node (A) at (0,0) {$\begin{tikzpicture}[baseline=(current bounding box.center)]
  \draw (0,0) -- (0,1) -- (1,1) -- (1,0) -- cycle;
  \node at (0.5,0.5) {$\rightarrow$};
  \node at (0.5,1) {$\rightarrow$};
  \node at (1.5,0.5) {$\rightarrow$};
  \node at (1.5,1) {$\rightarrow$};
  \node at (0.25,0.25) {$\rightarrow$};
  \node at (0.25,0.75) {$\rightarrow$};
  \node at (1.25,0.25) {$\rightarrow$};
  \node at (1.25,0.75) {$\rightarrow$};
  \node at (0.5,0.5) {$\Rightarrow$};
  \node at (0.5,1) {$\Rightarrow$};
  \node at (1.5,0.5) {$\Rightarrow$};
  \node at (1.5,1) {$\Rightarrow$};
  \node at (0.25,0.25) {$\Rightarrow$};
  \node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}$};
\node at (0.5,0.5) {$\Rightarrow$};
\node at (0.5,1) {$\Rightarrow$};
\node at (1.5,0.5) {$\Rightarrow$};
\node at (1.5,1) {$\Rightarrow$};
\node at (0.25,0.25) {$\Rightarrow$};
\node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}}$$

$$\begin{tikzpicture}[baseline=(current bounding box.center)]
\node (A) at (0,0) {$\begin{tikzpicture}[baseline=(current bounding box.center)]
  \draw (0,0) -- (0,1) -- (1,1) -- (1,0) -- cycle;
  \node at (0.5,0.5) {$\rightarrow$};
  \node at (0.5,1) {$\rightarrow$};
  \node at (1.5,0.5) {$\rightarrow$};
  \node at (1.5,1) {$\rightarrow$};
  \node at (0.25,0.25) {$\rightarrow$};
  \node at (0.25,0.75) {$\rightarrow$};
  \node at (1.25,0.25) {$\rightarrow$};
  \node at (1.25,0.75) {$\rightarrow$};
  \node at (0.5,0.5) {$\Rightarrow$};
  \node at (0.5,1) {$\Rightarrow$};
  \node at (1.5,0.5) {$\Rightarrow$};
  \node at (1.5,1) {$\Rightarrow$};
  \node at (0.25,0.25) {$\Rightarrow$};
  \node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}$};
\node at (0.5,0.5) {$\Rightarrow$};
\node at (0.5,1) {$\Rightarrow$};
\node at (1.5,0.5) {$\Rightarrow$};
\node at (1.5,1) {$\Rightarrow$};
\node at (0.25,0.25) {$\Rightarrow$};
\node at (0.25,0.75) {$\Rightarrow$};
\end{tikzpicture}}$$
15:8 Coherence of Gray Categories via Rewriting

as well as Peiffer generators, e.g.

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

for an arbitrary 2-cell $\chi : n + 1 \Rightarrow n + 3$, and interchange naturality generators, e.g.

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

In the following, when describing a Gray presentation, we will not mention the structural cells which are always implicitly supposed to be present.

A *model* of a presentation P in a Gray category C is a Gray functor $\bar{P} \to C$ from the presented Gray (3,2)-category to C.

**► Example 9.** A model of the presentation P of monoids (Ex. 8) in a Gray category C consists in a 1-cell $a : x \to x$ together with 2-cells $\mu : a * a \Rightarrow a$ and $\eta : 1_x \Rightarrow a$ and invertible 3-cells A, L, R (as in Ex. 3) satisfying suitable relations (as in Ex. 8). This is precisely what is usually called a *pseudomonoid* in C.

**► Remark.** A notion of presented Gray category (as opposed to (3,2)-category) can also be defined: it is slightly more involved since we still need to formally invert (by a localization) some morphisms, at least the interchangers. Similarly, we could consider their models which are functors to Gray categories. However, in practice people consider algebraic structures with invertible 3-cells (e.g. pseudomonoids), which explains why we are mostly interested in Gray (3,2)-categories here for simplicity.

Our goal is to show that some presentations are coherent, meaning that all the diagrams made of structural morphisms commute in the models. Formally, a Gray category is *coherent* when between any pair of parallel 2-cells there is at most one 3-cell and a Gray presentation is *coherent* when the associated Gray (3,2)-category is.

## 2 Rewriting

### 2.1 Confluence

Every rewriting system induces an abstract rewriting system (i.e., a graph) with 2-cells in $P_2^*$ as vertices and rewriting steps as edges (the set of paths thus being $P_3^*$), from which we can use the classical notions and properties of rewriting theory, detailed below. We slightly depart from the tradition by, for confluence properties, asking that diagrams should be closed and commute *modulo the relations* in $P_4$.

Given a rewriting path $P : \phi \Rightarrow \psi$, we say that $\phi$ *rewrites* to $\psi$. A *normal form* is a 2-cell $\phi$ such that the only rewriting path with source $\phi$ is the empty one. A *branching* is
a pair of coinitial rewriting paths $P_1 : \phi \Rightarrow \phi_1$ and $P_2 : \phi \Rightarrow \phi_2$; it is *local* when both $P_1$ and $P_2$ are rewriting steps, it is *joinable* when there exists a pair of cofinal rewriting paths $Q_1 : \phi_1 \Rightarrow \psi$ and $Q_2 : \phi_2 \Rightarrow \psi$, it is *confluent* when there exists a pair of cofinal rewriting paths $Q_1 : \phi_1 \Rightarrow \psi$ and $Q_2 : \phi_2 \Rightarrow \psi$ such that $P_1 * Q_1 \equiv_{P_4} P_2 * Q_2$, see left of (9). Similarly, a rewriting zigzag $P : \phi_1 \Rightarrow \phi_2$ in $P_3^\top$ is *confluent* when there exists a pair of cofinal rewriting paths $Q_1 : \phi_1 \Rightarrow \psi$ and $Q_2 : \phi_2 \Rightarrow \psi$ such that $P * Q_2 \equiv Q_1$, see right of (9)

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

A rewriting system is

- *terminating* when every sequence of composable rewriting steps is finite,

- (locally) confluent when every (local) branching is confluent,

- *Church-Rosser* when every rewriting zigzag is confluent,

- convergent if both terminating and locally confluent.

In a terminating rewriting system, every 2-cell $\phi$ rewrites to a normal form $\hat{\phi}$. The classical proof by well-founded induction of Newman's lemma [19], can be directly adapted (as in [8, Thm. 3.1.6]) in order to show

**► Theorem 10.** *A convergent rewriting system is confluent.*

Finally, for abstract rewriting systems it is well known that confluence implies the Church-Rosser property. In this setting, this translates as the following theorem, which adapts in our setting, the proof of Squier's theorem for coherent presentations of categories, see [17, Thm. 5.2] and [8, Thm. 4.3.2]:

**► Theorem 11.** *A convergent presentation $P$ is Church-Rosser and coherent.*

**Proof.** Suppose given a rewriting path $P : \phi \Rightarrow \psi$. Since $P$ is terminating, there is a rewriting path $P_\phi : \phi \Rightarrow \hat{\phi}$ (resp. $P_\psi : \psi \Rightarrow \hat{\psi}$) from $\phi$ (resp. $\psi$) to a normal form $\hat{\phi}$ (resp. $\hat{\psi}$). Moreover, by confluence, we have $\hat{\phi} = \hat{\psi}$ and $P_\phi \equiv P * P_\psi$, see the left of (10). Therefore, we have equivalences $P \equiv P_\phi * P_\psi^-$ and $P^- \equiv P_\psi * P_\phi^-$, as in the middle and right of (10):

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

Finally, as explained above, a 3-cell of $\bar{P}$ is a zigzag of rewriting paths $P_1^- * Q_1 * \dots * P_n^- * Q_n$ which is equivalent (modulo relations and axioms for inverses) to $P_\phi * P_\psi^-$:

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

Note that the 3-cell $P_\phi * P_\psi^-$ only depends on the source $\phi$ and the target $\psi$. We immediately deduce that two parallel 3-cells in $\bar{P}$ are equal. ◀

<figure><img src="image_20.png" /></figure>
## 2.2 Termination

Termination of a presentation is usually proved by checking that rules are decreasing according to some suitable order. A termination order is a well-founded partial order < on parallel 2-cells of a presentation P such that

- for every rewriting rule $A : \phi \Rightarrow \psi$ we have $\phi > \psi$,

- given composable 2-cells $\phi, \psi_1$ and $\phi'$ (resp. $\phi, \psi_2$ and $\phi'$) such that $\psi_1 > \psi_2$, we have $\phi * \psi_1 * \phi' > \phi * \psi_2 * \phi'$

- given 2-cells $\phi > \psi$ and composable 1-cells $u$ and $w$, we have $u * \phi * w > u * \psi * w$.

**Proposition 12.** *A rewriting system equipped with a termination order is terminating.*

**Example 13.** A termination order for the rewriting system of monoids (Ex. 3) can be constructed as follows. Firstly, the three non-structural rewriting rules can be shown to be terminating exactly as for 3-polygraph of monoids [15, Sect. A.2] (roughly $L$ and $R$ decrease the number of generators and $A$ puts $\mu$ generators on the right), by a termination order for which the interchangers are left invariant. Secondly, the interchangers make 2-cells decrease in the following sense. A 2-cell corresponds to a forest of leveled planar binary trees (where nodes correspond to 2-generators), i.e., trees equipped with a total “vertical” order refining the depth order. The interchanger rules decrease the sum, for each generators, of the number of generators above (w.r.t. to the vertical order) and on the left (which is easily defined for such forests).

## 2.3 Critical branchings

Given a local branching $(P_1, P_2)$, the following situations can occur. The branching is

- trivial when $P_1 = P_2$,

- non-minimal when there is another branching $(Q_1, Q_2)$ such that $P_i = \phi * (u * Q_i * v) * \psi$ for $i = 0, 1$ for some 1-cells $u, v$ and 2-cells $\phi, \psi$, not all identities,

- independent, or Peiffer, when there are morphisms of the form (4) such that

$$P_1 = ((u_1 * A_1 * w_1) * \chi * (u_2 * \phi_2 * w_2))$$

$$P_2 = ((u_1 * \phi_1 * w_1) * \chi * (u_2 * A_2 * w_2))$$

- natural when there are morphisms as on the left of (6) such that

$$P_1 = ((A * v * w) * (u' * v * \alpha))$$

$P_2$ is the first rewriting step of $X_{\phi,v*\alpha}$, and similarly for the situation on the right of (6),

- critical when it is of none of the above forms.

Since, by definition of Gray presentations, non-critical branchings are necessarily confluent, we have:

**Theorem 14.** *A presentation is locally confluent if and only if every critical branching is confluent.*

As usual, critical branchings can be computed by considering the ways two left members $\phi_1$ and $\phi_2$ of rules can overlap non-trivially (sharing at least one 2-generator). Graphically, the following generic situations can happen, where the two regions respectively represent $\phi_1$ and $\phi_2$, the square $\psi$ in the middle being the intersection (overlap) of both, which is supposed
not to be an identity 2-cell:

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

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

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

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

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

(and also the situations obtained by swapping $\phi_1$ and $\phi_2$). From this, one deduces that any pair of rules can give rise to a finite number of critical branchings which can effectively be computed (the algorithmic aspects will be detailed in future works). Moreover, note that a non-structural rewriting rule $R: \phi \Rightarrow \psi$ can only give rise to a finite number of critical branchings with interchangers: if the two 2-generators involved in an interchanger $X_{\alpha,v,\beta}$ are too far apart horizontally (i.e., $v$ is a composite of too many 1-cells), the branching is necessarily an exchange branching, e.g. left of (8). Similarly, that two interchangers never make a critical branching (all such branchings are natural), e.g. right of (8). From the above considerations, we deduce:

**► Theorem 15.** A presentation with a finite number of 2-generators and of non-structural 3-generators, with non-identity 2-cells as sources, has a finite number of critical branchings.

It should be noted that this theorem contrasts with the situation for presentations of (3,2)-categories (where interchangers are identities), where a finite presentation can give rise to an infinite number of critical branchings [15, 8]. Our formalization of rewriting systems avoids this problem, at the cost of having to explicitly handle interchangers.

**► Example 16.** The presentation for monoids (Ex. 8) has five critical branchings:

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

## 2.4 A coherent completion procedure

The general methodology for constructing confluent presentations is the following one. Suppose given a presentation $P$ (usually containing no relation in $P_4$ excepting structural ones).

1. Find a termination order for the rules of $P$: if none can be found try to reorient some rules. Conclude that $P$ is terminating by Prop. 12.

2. Compute the critical branchings and check that they are joinable: if a critical branching is not joinable, add a new rule to make it confluent (this is the Knuth-Bendix completion procedure [13]).

3. For every critical branching, choose a way to join it and add a corresponding relation in $P_4$ (if not already present).

4. Conclude that $P$ is locally confluent by Thm. 14, thus confluent by Thm. 10 and thus coherent by Thm. 11.

5. Optionally, remove some redundant rules and relations in order to achieve a smaller presentation.

This methodology is illustrated in next section. Note that steps 2 and 3 can be combined, giving rise to a "homotopical completion procedure" and 5 can be partly automated: this is detailed in the case of coherent presentations of monoids in [10] and left for future work for Gray presentations.
# 3 Applications

## 3.1 Pseudomonoids

Consider the presentation P for monoids given in Ex. 8 whose termination was shown in Ex. 13. There are five critical branchings, given in Ex. 16, which are all joinable. If we add five corresponding relations in P we obtain a convergent, and thus coherent, presentation. Note however that the presentation P given in Ex. 8 has only two relations: in fact, three of the five relations are derivable from the other and can thus be removed (the argument given in [8] for pseudomonoids in 3-categories can directly be adapted to our setting). This allows us to recover the coherence theorem of [14].

## 3.2 Adjunctions

The presentation for adjunctions is given by $P_0 = \{x, y\}$, $P_1 = \{a : x \to y, b : y \to x\}$ and $P_2 = \{\eta : 1_x \Rightarrow ab, \varepsilon : ba \Rightarrow 1_y\}$ where $\eta$ and $\varepsilon$ are respectively pictured as $\cap$ and $\cup$. The two rules are shown on the left below and the relations corresponding to the two critical branchings are on the right:

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

They are sometimes called the *swallowtail relations*. A model for this presentation in the 2-category **Cat** (seen as a (3,2)-precategory with only identity 3-cells) is precisely an adjunction. Termination can be shown by observing that the two non-structural rules decrease the number of generators and the structural rules decrease the number of generators which are “on the left and above”, as in the previous case. We deduce that this presentation is coherent, thus recovering a variant of the coherence theorem shown in [4] (see below).

## 3.3 Self-dualities

The theory for self-dualities is the following variant of the previous one. We have $P_0 = \{\star\}$, $P_1 = \{a : \star \to \star\}$, $P_2 = \{\eta : 1_\star \Rightarrow aa, \varepsilon : aa \Rightarrow 1_\star\}$ where $\eta$ and $\varepsilon$ are respectively pictured as $\cap$ and $\cup$. The two rules are those on the left of (11). Note that because of the difference in “typing” of 0- and 1-cells, the rewriting system is not anymore terminating, since we have the reduction

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

Moreover, this endomorphism 3-cell is not an identity, preventing any hope for the presentation to be coherent. Following [4], we can still aim at showing a partial coherence result by restricting to 2-cells which are *connected*, i.e., whose graphical representation is *connected* (we do not give the formal definition here). In this case, termination can actually be shown by using the same arguments as in Sec. 3.2. However, the critical pairs are not joinable either since, for instance, we have

<figure><img src="image_29.png" /></figure>
15:14 Coherence of Gray Categories via Rewriting

for every $(u, v) \in C_i \times_{i \wedge j-1} C_j$ with $0 < i, j \le n$,

$$1_u * v = \begin{cases} v & \text{if } i \le j \\ 1_{u \ast v} & \text{if } i > j \end{cases} \qquad u * 1_v = \begin{cases} u & \text{if } i \ge j \\ 1_{u \ast v} & \text{if } i < j \end{cases}$$

such that, for composable cells $u, v, w$, with $k < l$,

$$(u *_k v) *_k w = u *_k (v *_k w) \qquad \begin{aligned} u *_k (v *_l w) &= (u *_k v) *_l (u *_k w) \\ (u *_l v) *_k w &= (u *_k v) *_l (u *_k w) \end{aligned}$$

A morphism of $n$-precategories, called an $n$-prefunctor, is a morphism between the underlying globular sets which preserves identities and compositions as expected. We write $\mathbf{PCat}_n$ for the category of $n$-precategories. This category is locally presentable and thus complete and cocomplete. Given an $n$-precategory $C$, we write $C_0$ for its set of 0-cells seen as an $n$-category with empty sets of $i$-cells for $0 < i \le n$. The “funny tensor product” $C \boxtimes D$ of two $n$-precategories $C$ and $D$ is defined as the pushout on the right where the arrows are the obvious inclusions. This makes $\mathbf{PCat}_n$ into a monoidal category and we have:

$$\begin{array}{ccc} C_0 \times D_0 & \to & C \times D_0 \\ \downarrow & & \downarrow \\ C_0 \times D & \to & C \boxtimes D \end{array}$$

**Proposition 17.** An $n+1$-precategory is the same as a category enriched in $\mathbf{PCat}_n$ equipped with the funny tensor product.

## 4.2 Prepolygraphs

We now briefly introduce the notion of prepolygraph which generalizes in arbitrary dimension the notion of rewriting system, by a direct adaptation the definition invented by Burroni for $n$-categories [3]. We write $\mathbf{PCat}_n^+$ for the pullback on the right where the arrow on the top is the forgetful functor and the one on the left is the truncation functor (forgetting the set of $n+1$-cells in an $n+1$-globular set). An object in this category consists of an $n$-precategory equipped with a set of $n+1$-cells (for which there is no notion of composition). There is a forgetful functor $\mathbf{PCat}_{n+1} \to \mathbf{PCat}_n^+$ which amounts to forget about compositions involving $n+1$-cells, which admits a right adjoint $L_n : \mathbf{PCat}_n^+ \to \mathbf{PCat}_{n+1}$, generating all the formal compositions of $n+1$-cells.

$$\begin{array}{ccc} \mathbf{PCat}_n^+ & \dashrightarrow & \mathrm{Glob}_{n+1} \\ \mathbf{PCat}_n & \to & \mathrm{Glob}_n \end{array}$$

We now define by induction on $n \in \mathbb{N}$, the category $\mathbf{Pol}_n$ of $n$-prepolygraphs together with a functor $F_n : \mathbf{Pol}_n \to \mathbf{PCat}_n$ associating to each $n$-prepolygraph the associated freely generated $n$-precategory. For $n=0$, we set $\mathbf{Pol}_0 = \mathbf{Set}$ and $F_0$ is the identity functor ($\mathbf{PCat}_0$ is isomorphic to $\mathbf{Set}$). The category of $n+1$-prepolygraphs is defined by the pullback on the right where the vertical arrow is the expected forgetful functor, and we define the functor $F_{n+1} = L_{n+1} \circ F_n^+$. More explicitly, an $n$-prepolygraph consists in a diagram of sets

$$\begin{array}{ccc} \mathbf{Pol}_{n+1} & \xrightarrow{F_n^+} & \mathbf{PCat}_n^+ \\ \mathbf{Pol}_n & \xrightarrow{F_n} & \mathbf{PCat}_n \end{array}$$

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

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

such that $s_i^* \circ s_{i+1} = s_i^* \circ t_{i+1}$ and $t_i^* \circ s_{i+1} = t_i^* \circ t_{i+1}$, together with a structure of $n$-precategory on the globular set on the bottom row: $P_i$ is the set of $i$-generators, $s_i, t_i : P_{i+1} \to P_i^*$
respectively associate to each $i$-1-generator its *source* and *target*, and $P_i^*$ is the set of *i*-cells, i.e., formal compositions of *i*-generators.

The cells in such prepolygraphs are particularly easy to manipulate because of the following normal form, generalizing Prop. 2 and its proof. We plan to investigate algorithmic aspects (for computing critical pairs, etc.) based on this representation in future works.

**Theorem 18.** A non-identity $k$-cell $P$ in an $n$-prepolygraph decomposes uniquely as $P = R^1 * R^2 * \dots * R^p$ with each $R^i$ being a $k$-rewriting step, i.e., a composite of the form $R^i = u_{k-1}^i * (\dots * (u_2^i * (u_1^i * A^i * w_1^i) * w_2^i) * \dots) * w_{k-1}^i$ where $A^i$ is a $k$-generator and $w_j^i$ are $j$-cells.

Interestingly, this formalization based on prepolygraphs corresponds precisely to the one proposed by Bar and Vicary [2]: their representation is more economical thanks to the use of integers in order to encode cells, but somewhat obscures the universal properties it satisfies.

**Proposition 19.** The $n$-signatures of [2] correspond to the $n$-prepolygraphs defined above.

Their work gives hints at a way to generalize Gray presentations in order to present semistrict tetracategories, by providing the adapted collections of structural cells. We plan to investigate this, as well as an adaptation of our techniques in order to provide automation to their tool Globular [1] in future work.

References

1 Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. In *LIPIcs*, volume 52, pages 34:1–34:11, 2016. arXiv: 1612.01093.

2 Krzysztof Bar and Jamie Vicary. Data structures for quasistrict higher categories. In *Logic in Computer Science (LICS)*, 32nd Annual Symposium on, pages 1–12. IEEE, 2017. arXiv:1610.06908.

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

4 Lawrence Dunn and Jamie Vicary. Coherence for frobenius pseudomonoids and the geometry of linear proofs. Preprint, 2016. arXiv:1601.05372.

5 François Foltz, Christian Lair, and GM Kelly. Algebraic categories with few monoidal biclosed structures or none. *Journal of Pure and Applied Algebra*, 17(2):171–177, 1980.

6 Robert Gordon, Anthony John Power, and Ross Street. *Coherence for tricategories*, volume 558. American Mathematical Soc., 1995.

7 John Walker Gray. *Formal category theory: adjointness for 2-categories*, volume 391. Springer, 2006.

8 Yves Guiraud and Philippe Malbos. Higher-dimensional categories with finite derivation type. *Theory and Applications of Categories*, 22(18):420–478, 2009.

9 Yves Guiraud and Philippe Malbos. Polygraphs of finite derivation type. *Mathematical Structures in Computer Science*, pages 1–47, 2016. arXiv:1402.2587.

10 Yves Guiraud, Philippe Malbos, and Samuel 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.

11 Nick Gurski. *Coherence in three-dimensional category theory*, volume 201. Cambridge Univ. Press, 2013.

12 Aleks Kissinger and Jamie Vicary. Semistrict $n$-categories via rewriting. *Proceedings of the first workshop on Higher-Dimensional Rewriting and Applications*, 2015.
15:16 Coherence of Gray Categories via Rewriting

13 Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. In *Computational problems in abstract algebra*, pages 263–297, 1970.

14 Stephen Lack. A coherent approach to pseudomonads. *Advances in Math.*, 152(2):179–202, 2000.

15 Yves Lafont. Towards an algebraic theory of boolean circuits. *Journal of Pure and Applied Algebra*, 184(2):257–310, 2003.

16 Samuel Mimram. Towards 3-Dimensional Rewriting Theory. *Logical Methods in Computer Science*, 10(1):1–47, 2014. arXiv:1403.4094.

17 Craig C Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. *Theoretical Computer Science*, 131(2):271–294, 1994.

18 Ross Street. Categorical structures. *Handbook of algebra*, 1:529–577, 1996.

19 Terese. *Term Rewriting Systems*. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

20 Dominic Verdon. Coherence for braided and symmetric pseudomonoids. Preprint, 2017. arXiv:1705.09354.