# Rewriting in Gray categories with applications to coherence

Simon Forest, Samuel Mimram

► To cite this version:

Simon Forest, Samuel Mimram. Rewriting in Gray categories with applications to coherence. Mathematical Structures in Computer Science, 2022, 32 (5), pp.574-647. 10.1017/S0960129522000299 hal-04244411

HAL Id: hal-04244411

https://hal.science/hal-04244411v1

Submitted on 16 Oct 2023

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 CC BY 4.0 - Attribution - International License
# Rewriting in Gray categories with applications to coherence

Simon Forest, Samuel Mimram

## Abstract

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which are adapted to mechanized computations and include Gray categories as particular cases. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier's theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, Frobenius monoids.

## Introduction

Algebraic structures, such as monoids, can be defined inside arbitrary categories. In order to generalize their definition to higher categories, the general principle is that one should look for a *coherent* version of the corresponding algebraic theory: this roughly means that we should add enough higher cells to our algebraic theory so that “all diagrams commute” up to these cells. For instance, when generalizing the notion of monoid from monoidal categories to monoidal 2-categories, associativity and unitality are now witnessed by 2-cells, and one should add new axioms in order to ensure their coherence: in this case, those can be chosen to be MacLane’s unit and pentagon equations, thus resulting in the notion of pseudomonoid. The fact that these are indeed enough to make the structure coherent constitutes a reformulation of MacLane’s celebrated coherence theorem for monoidal categories [22]. In this context, a natural question is: how can we systematically find those higher coherence cells?

Rewriting theory [2, 31] provides a satisfactory answer to this question. Its starting point is the observation that it is often useful to provide an orientation to equations in algebraic structures, which dates back to the work of Dehn [8] and Thue [32] on presentations of groups and monoids respectively. Namely, when the resulting rewriting system is suitably behaved (confluent and terminating) equality can be tested efficiently (by comparing normal forms). Moreover, confluence of the whole rewriting system can be decided algorithmically by computing critical branchings and testing for the confluence of those only, which are always in finite number when the rewriting system is finite. In fact, this result can be reformulated as the fact that the confluence diagrams for critical branchings provide us precisely with enough cells to make the structure coherent. This was first observed by Squier for monoids, first formulated in homological language [26] and then generalized as a homotopical condition [27, 20]. These results were then extended to strict higher categories by Guiraud and Malbos [13, 14, 15] based on a notion of rewriting system adapted to this setting, which is provided by Burroni’s *polygraphs* [7] (also called computads [28]). In particular, their work allows recovering the coherence laws for pseudomonoids in this way.

Our aim is to generalize those techniques in order to be able to define coherent algebraic structures in *weak* higher categories. We actually handle here the first non-trivial case, which is the one of dimension 3. Namely, it is well-known that tricategories are not equivalent to strict 3-categories: the “best” one can do is to show that they are equivalent to *Gray categories* [11, 17], which is an intermediate structure between weak and strict 3-categories, roughly consisting in 3-categories in which the exchange law is not required to hold strictly. This means that classical rewriting techniques cannot be used off the shelf in this context and one has to adapt those to Gray categories, which is the object of this article.
It turns out that a slightly more general notion than Gray categories is adapted to rewriting: *precategories*. The notion of precategory is a generalization of the one of sesquicategory, whose use has already been advocated by Street in the context of rewriting [29]. The interest in those has also been renewed recently, because they are at the heart of the graphical proof-assistant Globular [3, 4]. Gray categories are particular 3-precategories equipped with exchange 3-cells satisfying suitable axioms. We first work out in details the definition of precategories and, based on the work of Weber [33], show that (n+1)-precategories can be defined as categories enriched in n-precategories equipped with the so-called *funny tensor product*, see Section 1. This is analogous to the well-known fact that Gray categories are categories enriched over 2-categories equipped with the Gray tensor product [11], that we recall in Section 2. We then define in Section 3 a notion of polygraph adapted to precategories, called *prepolygraph*. It is amenable to computer implementation: there is an efficient representation of the morphisms in free precategories, which allows for mechanized computation of critical branchings. Moreover, it can be used to present other precategories, in particular Gray categories (Section 2.3). In order to study these presentations, we adapt the theory of rewriting to the context of prepolygraphs in Section 3, and we show that our notion of rewriting system retains the classical properties. In particular, a finite rewriting system always has a finite number of critical branchings, which contrasts with the case of strict categories [21, 13, 24]. It moreover allows for a Squier-type coherence theorem (Theorem 3.4.5). Finally, in Section 4, we apply our technology to several algebraic structures of interest, which allows us to recover known coherence theorems and find new ones, such as for pseudomonoids (Section 4.1), pseudoadjunctions (Section 4.2), self-dualities (Section 4.3), and also Frobenius pseudomonoids but up to a termination conjecture (Section 4.4).

**Acknowledgements** The authors would like to thank the reviewer for their high-quality proof-reading, and the associated numerous and useful comments.

# 1 Precategories

In this work, we use a variant of the notion of *n*-category called *precategory* whose 2-dimensional version is better known as *sesquicategory* [29]. Many definitions of “semi-strict” higher categories can be described as precategories with additional structures and equations, and this is in particular the case for Gray categories. Moreover, contrarily to strict higher categories, their cells can be easily described by normal forms, making them amenable to computations. This notion was used to give several definitions of semi-strict higher categories [4] and is the underlying structure of the Globular tool for higher categories [3]. Premises of it can be found in the work of Street [29] and Makkai [23]. In what follows, we give equational and enriched definitions of precategories (Section 1.2 and Section 1.4). Then, we define prepolygraphs as a direct adaptation of the notion of polygraph for strict categories (Section 1.5), and we show that the cells of such a prepolygraph admit a normal form (Section 1.8). Finally, we recall the usual construction of localization, in the context of 3-dimensional precategories only (Section 1.9), since our subsequent results will mostly target (3, 2)-precategories.

## 1.1 Globular sets

Given $n \in \mathbb{N}$, an *n-globular set* $C$ is a diagram of sets

$$C_0 \underset{\partial_0^+}{\overset{\partial_0^-}{\rightleftarrows}} C_1 \underset{\partial_1^+}{\overset{\partial_1^-}{\rightleftarrows}} C_2 \underset{\partial_2^+}{\overset{\partial_2^-}{\rightleftarrows}} \dots \underset{\partial_{n-1}^+}{\overset{\partial_{n-1}^-}{\rightleftarrows}} C_n$$

such that $\partial_i^- \circ \partial_{i+1}^- = \partial_i^- \circ \partial_{i+1}^+$ and $\partial_i^+ \circ \partial_{i+1}^- = \partial_i^+ \circ \partial_{i+1}^+$ for $0 \le i < n-1$. An element $u$ of $C_i$ is called an *i-globe* of $C$ and, for $i > 0$, the globes $\partial_{i-1}^-(u)$ and $\partial_{i-1}^+(u)$ are respectively called the *source* and *target* and $u$. We write $\mathbf{Glob}_n$ for the category of *n-globular sets*, a morphism $f: C \to D$ being a family of morphisms $f_i: C_i \to D_i$, for $0 \le i \le n$, such that $\partial_i^\epsilon \circ f_{i+1} = f_i \circ \partial_i^\epsilon$ for $\epsilon \in \{-, +\}$. Given $m \ge n$ and $C \in \mathbf{Glob}_m$, we denote by $\mathcal{T}_n^m(C)$ the *n-globular set* obtained from $C$ by removing the *i-globes* for $n < i \le m$. This operation extends to a functor $\mathcal{T}_n^m: \mathbf{Glob}_m \to \mathbf{Glob}_n$.
(iii) for $i, k, l \in \{0, \dots, n\}$ with $i = \min(k, l) - 1$, given $(u, v) \in C_{k-1} \times_i C_l$,

$$ \mathrm{id}_{u *_i v} = \begin{cases} v & \text{if } k \le l, \\ \mathrm{id}_{u *_{i,v}} & \text{if } k > l, \end{cases} $$

and, given $(u, v) \in C_k \times_i C_{l-1}$,

$$ u *_i \mathrm{id}_v = \begin{cases} u & \text{if } l \le k, \\ \mathrm{id}_{u *_{i,v}} & \text{if } l > k, \end{cases} $$

(iv) for $i, k, l, m \in \{0, \dots, n\}$ with $i = \min(k, l) - 1 = \min(l, m) - 1$, and $u \in C_k, v \in C_l$ and $w \in C_w$ such that $u, v, w$ are $i$-composable,

$$ (u *_i v) *_i w = u *_i (v *_i w), $$

(v) for $i, j, k, k' \in \{0, \dots, n\}$ such that

$$ j = \min(k, k') - 1 \quad \text{and} \quad i < j, $$

given $u \in C_{i+1}$ and $(v, v') \in C_k \times_j C_{k'}$ such that $u, v$ are $i$-composable,

$$ u *_i (v *_j v') = (u *_i v) *_j (u *_i v') $$

and, given $(u, u') \in C_k \times_j C_{k'}$ and $v \in C_{i+1}$ such that $u, v$ are $i$-composable,

$$ (u *_j u') *_i v = (u *_i v) *_j (u' *_i v). $$

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. The above description exhibits $n$-precategories as an essentially algebraic theory. Thus, $\mathbf{PCat}_n$ is a locally presentable category [1, Thm. 3.36]; consequently, it is complete and cocomplete [1, Cor. 1.28]. In the following, we write 1 for the terminal $n$-precategory for $n \ge 0$.

In dimension 2, string diagrams can be used as usual to represent compositions of 2-cells. For example, given the 2-precategory $C$ freely generated on the globular set

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

we can represent the two 2-cells

$$ (\phi *_0 g) *_1 (f' *_0 \psi) \quad \text{and} \quad (f *_0 \psi) *_1 (\phi *_0 g') $$

respectively by

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

and

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

Note that these two 2-cells are different, and that the diagram

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

makes no sense in a generic 2-precategory.
## 1.3 Truncation functors

Similarly to strict categories [25], the categories $\mathbf{PCat}_n$ for $n \ge 0$ can be related by several functors. For $m \ge n$, we have a truncation functor

$$ \mathcal{T}_n^m : \mathbf{PCat}_m \to \mathbf{PCat}_n $$

where, given an $m$-precategory $C$, $\mathcal{T}_n^m(C)$ is the $n$-precategory obtained by forgetting all the $i$-cells for $n < i \le m$. This functor admits a left adjoint

$$ \mathcal{F}_n^m : \mathbf{PCat}_n \to \mathbf{PCat}_m $$

which, to an $n$-precategory $C$, associates the $m$-precategory $\mathcal{F}_n^m(C)$ obtained by formally adding $i$-identities for $n < i \le m$, i.e., $\mathcal{F}_n^m(C)_i = C_i$ for $i \le n$ and $\mathcal{F}_n^m(C)_i = C_n$ for $i > n$.

**Proposition 1.3.1.** For $m > n$, the functors $\mathcal{T}_n^m$ and $\mathcal{F}_n^m$ admit both left and right adjoints, i.e., we have a sequence of adjunctions

$$ \mathcal{H}_n^m + \mathcal{F}_n^m + \mathcal{T}_n^m + \mathcal{R}_n^m. $$

As a consequence, the functors $\mathcal{T}_n^m$ and $\mathcal{F}_n^m$ preserve both limits and colimits.

*Proof.* Suppose given an $m$-precategory $C$. The $n$-precategory $\mathcal{H}_n^m(C)$ has the same $i$-cells as $C$ for $i < n$ and $\mathcal{H}_n^m(C)_i$ is obtained by quotienting $C_n$ under the smallest congruence $\sim$ such that $u \sim v$ whenever there exists an $(n+1)$-cell $\alpha: u \to v$. The $n$-precategory $\mathcal{R}_n^m(C)$ has the same $i$-cells as $C$ for $0 \le i \le n$ and, for $n \le i < m$, $\mathcal{R}_n^m(C)_{i+1}$ is defined from $\mathcal{R}_n^m(C)_i$ as the set of pairs $(u, v) \in \mathcal{R}_n^m(C)_i \times \mathcal{R}_n^m(C)_i$ with $\partial^-(u) = \partial^-(v)$ and $\partial^+(u) = \partial^+(v)$, with $\partial^-(u, v) = u$ as source and $\partial^+(u, v) = v$ as target. Details are left to the reader. $\square$

Given $n < m$, we write $(-)_{(n)}$ for the functor $\mathcal{F}_n^m \circ \mathcal{T}_n^m: \mathbf{PCat}_m \to \mathbf{PCat}_m$ and, given an $m$-precategory $C$, we call $C_{(n)}$ the $n$-skeleton of $C$. It corresponds to the $m$-precategory obtained from $C$ by removing all non-trivial $i$-cells with $i > n$. We write

$$ j_{(-)}: (-)_{(n)} \to \mathbf{1}_{\mathbf{PCat}_m} $$

for the counit of the adjunction $\mathcal{F}_n^m \to \mathcal{T}_n^m$. Since $\mathcal{F}_n^m$ and $\mathcal{T}_n^m$ both preserve limits and colimits by Proposition 1.3.1, so does the functor $(-)_{(n)}$.

## 1.4 The funny tensor product

We now define the funny tensor product, that we will use to give an enriched definition of precategories. It can be thought of as a variant of the cartesian product of categories where we restrict to morphisms where one of the components is the identity (or, more precisely, to formal composites of such morphisms). We give a rather direct and concise definition, and we refer the reader to the work of Weber [33] for a more abstract definition. Given $n \ge 0$ and two $n$-precategories $C$ and $D$, the *funny tensor product of C and D* is the pushout

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

Since $j_{(-)}$ is a natural transformation, the funny tensor product can be extended as a functor

$$ (-) \Box (-): \mathbf{PCat}_n \times \mathbf{PCat}_n \to \mathbf{PCat}_n. $$

We show that it equips $\mathbf{PCat}_n$ with a structure of monoidal category. First, we prove several technical lemmas.
Given an n-precategory, there are canonical morphisms

$$ \lambda_C^f: 1 \Box C \xrightarrow{\sim} C \quad \text{and} \quad \rho_C^f: C \Box 1 \xrightarrow{\sim} C $$

where $\lambda_C^f$ is defined by

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

and $\rho_C^f$ is defined similarly. Both are natural in $C$. We can conclude that:

**Proposition 1.4.4.** ($C, \Box, 1, \alpha, \lambda^f, \rho^f$) is a monoidal category.

*Proof.* The axioms of monoidal categories follow from the pushout definition of the funny tensor product and the cartesian monoidal structure on n-precategories. $\square$

In fact, the funny tensor product is a suitable product for an inductive enriched definition of precategories, i.e.,

**Proposition 1.4.5.** There is an equivalence of categories between (n+1)-precategories and categories enriched in n-precategories with the funny tensor product.

*Proof.* See Appendix A. $\square$

## 1.5 Prepolygraphs

In this section, we introduce the notion of prepolygraph which generalizes in arbitrary dimension the notion of rewriting system. This definition is an adaptation to precategories of the notion of polygraph introduced by Burroni for strict categories [7]. Polygraphs were also generalized by Batanin to algebras of any finitary monad on globular sets [6], and prepolygraphs are a particular instance of this construction, for which we provide rather here an explicit construction.

For $n \ge 0$, writing $\mathcal{U}_n$ for the canonical forgetful functor $\mathbf{PCat}_n \to \mathbf{Glob}_n$, we define the category $\mathbf{PCat}_n^+$ as the pullback

$$ \begin{array}{ccc} \mathbf{PCat}_n^+ & \xrightarrow{\mathcal{U}_n^+} & \mathbf{Glob}_{n+1} \\ \mathcal{V}_n & \searrow & \downarrow \mathcal{T}_n^{n+1} \\ \mathbf{PCat}_n & \xrightarrow{\mathcal{U}_n} & \mathbf{Glob}_n \end{array} $$

and write $\mathcal{U}_n^+ : \mathbf{PCat}_n^+ \to \mathbf{Glob}_{n+1}$ for the top arrow of the pullback and $\mathcal{V}_n : \mathbf{PCat}_n^+ \to \mathbf{PCat}_n$ for the left arrow. An object $(C, C_{n+1})$ of $\mathbf{PCat}_n^+$ consists of an n-precategory C equipped with a set $C_{n+1}$ of (n+1)-cells and two maps $d_n^-, d_n^+$: $C_{n+1} \to C_n$ (note however that there is no notion of composition for (n+1)-cells). There is a functor $\mathcal{W}_n : \mathbf{PCat}_{n+1} \to \mathbf{PCat}_n^+$ defined as the universal arrow

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

and, since categories and functors in the above diagram are induced by finite limit sketches and morphisms of finite limit sketches, they are all right adjoints (see [5, Thm. 4.1] for instance), so that $\mathcal{W}_n$ admits a left adjoint $\mathcal{L}_n : \mathbf{PCat}_n^+ \to \mathbf{PCat}_{n+1}$.
We define the category $\mathbf{Pol}_n$ of $n$-prepolygraphs together with a functor $\mathcal{G}_n: \mathbf{Pol}_n \to \mathbf{PCat}_n$ by induction on $n$. We define $\mathbf{Pol}_0 = \mathbf{Set}$ and take $\mathcal{G}_0$ to be the identity functor. Now suppose that $\mathbf{Pol}_n$ and $\mathcal{G}_n$ are defined for $n \ge 0$. We define $\mathbf{Pol}_{n+1}$ as the pullback

$$ \begin{array}{ccc} \mathbf{Pol}_{n+1} & \xrightarrow{\mathcal{G}_n^+} & \mathbf{PCat}_n^+ \\ \mathcal{T}_n^{n+1} & \underset{\sim}{\twoheadleftarrow} & \underset{\sim}{\twoheadrightarrow} \\ \mathbf{Pol}_n & \xrightarrow{\mathcal{G}_n} & \mathbf{PCat}_n \end{array} $$

and write $\mathcal{G}_n^+ : \mathbf{Pol}_{n+1} \to \mathbf{PCat}_n^+$ for the top arrow and $\mathcal{T}_n^{n+1}$ for the left arrow of the diagram. Finally, we define $\mathcal{G}_{n+1}$ as $\mathcal{L}_n \circ \mathcal{G}_n^+$.

More explicitly, an $(n+1)$-prepolygraph $P$ consists in a diagram of sets

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

such that $\partial_i^- \circ d_{i+1}^- = \partial_i^- \circ d_{i+1}^+$ and $\partial_i^+ \circ d_{i+1}^- = \partial_i^+ \circ d_{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, $d_i^-, d_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. In line with the latter notation, we will often write $P^*$ for the image of an $n$-prepolygraph $P$ by $\mathcal{G}_n$.

By definition, an $(n+1)$-prepolygraph $P$ has an underlying $n$-prepolygraph $\mathcal{T}_n^{n+1}(P)$, that we will often denote by $P_{\le n}$. More generally, for $m \ge n$, an $m$-prepolygraph $P$ has an underlying $n$-prepolygraph $P_{\le n}$ obtained by applying successively the forgetful functors $\mathcal{T}_i^{i+1}$ for $m > i \ge n$.

**Example 1.5.1.** We define the 3-prepolygraph $P$ for pseudomonoids as follows. We put

$$ P_0 = \{x\}, \quad P_1 = \{a : x \to x\}, \quad P_2 = \{\mu : \bar{2} \Rightarrow \bar{1}, \eta : \bar{0} \Rightarrow \bar{1}\}, $$

where, given $n \in \mathbb{N}$, we write $\bar{n}$ for the composite $a *_0 \cdots *_0 a$ of $n$ copies of $a$, and we define $P_3$ as the set with the following three elements

$$ \begin{array}{l} A : (\mu *_0 \bar{1}) *_1 \mu \Rightarrow (\bar{1} *_0 \mu) *_1 \mu \\ L : (\eta *_0 \bar{1}) *_1 \mu \Rightarrow \mathrm{id}_{\bar{1}} \\ R : (\bar{1} *_0 \eta) *_1 \mu \Rightarrow \mathrm{id}_{\bar{1}} \end{array} $$

Note that we make use of the arrows $\to$, $\Rightarrow$ and $\Rightarrow\Rightarrow$ to indicate the source and target of each $i$-generator for $i \in \{1, 2\}$: $a$ is a 1-generator such that $d_0^-(a) = d_0^+(a) = x$, $\mu$ is a 2-generator such that $d_1^-(\mu) = a*_0 a$ and $d_1^+(\mu) = a$, and so on. In the following, we will keep using this notation to describe the generators of other prepolygraphs.

## 1.6 Presentations

Given an $n$-precategory $C$ with $n > 0$, a congruence for $C$ is an equivalence relation $\sim$ on $C_n$ such that, for all $u, u' \in C_n$ satisfying $u \sim u'$,

$$ - \partial_{n-1}^{\epsilon}(u) = \partial_{n-1}^{\epsilon}(u') \text{ for } \epsilon \in \{-, +\}, $$

$$ - \text{ for } v, w \in C_{i+1} \text{ with } 0 \le i < n \text{ such that } v, u, w \text{ are } i\text{-composable, we have} $$

$$ v *_i u *_i w \sim v *_i u' *_i w. $$

Given such a congruence for $C$, there is an $n$-precategory $C/\sim$ which is the $n$-precategory $D$ such that $D_i = C_i$ for $i < n$ and $D_n = C_n/\sim$ and where the identities and compositions are induced by the ones on $C$.
Now, consider the composite functor

$$ \mathbf{Pol}_{n+1} \xrightarrow{\mathcal{G}_{n+1}} \mathbf{PCat}_{n+1} \xrightarrow{\mathcal{H}_n^{n+1}} \mathbf{PCat}_n . $$

To an $(n+1)$-prepolygraph $\mathbf{P}$, it associates an $n$-precategory denoted by $\bar{\mathbf{P}}$. Concretely, $\bar{\mathbf{P}}$ is isomorphic to $(\mathbf{P}_{\le n})^* / \sim \mathbf{P}$ where $\sim \mathbf{P}$ is the smallest congruence such that $\partial_n^-(u) \sim \mathbf{P} \partial_n^+(u)$ for $u \in \mathbf{P}_{n+1}$. In the following, we say that an $(n+1)$-prepolygraph $\mathbf{P}$ is a *presentation* of an $n$-precategory $\mathcal{C}$ when $\mathcal{C}$ is isomorphic to $\bar{\mathbf{P}}$.

## 1.7 Freely generated cells

Given $(C, C_{n+1}) \in \mathbf{PCat}_n^+$, we give an explicit description of the free $(n+1)$-precategory $\mathcal{L}_n(C, C_{n+1})$ it generates, similar to the one given in [25] in the case of polygraphs. This $(n+1)$-precategory has $\mathcal{C}$ as underlying $n$-precategory so that we focus on the description of the $(n+1)$-cells, which can be described as equivalence classes of terms, called here *expressions*, corresponding to formal composites of cells. These expressions are defined inductively as follows:

- for every element $u \in C_{n+1}$, there is an expression, still noted $u$,

- for every $n$-cell $u \in C_n$, there is an expression $\mathrm{id}_u$,

- for every $0 \le i < n$, for every $u \in C_{i+1}$ and every expression $v$, there is an expression $u *_i v$,

- for every $0 \le i < n$, for every expression $u$ and every $v \in C_{i+1}$, there is an expression $u*_i v$,

- for every pair of expressions $u$ and $v$, there is an expression $u*_n v$.

We then define *well-typed expressions* through typing rules in a sequent calculus. We consider judgments of the form

- $\vdash t: u \to v$, where $t$ is an expression and $u, v \in C_n$, with the intended meaning that the expression $t$ has $u$ as source and $v$ as target,

- $\vdash t = t'$: $u \to v$, where $t$ and $t'$ are expressions and $u, v \in C_n$, with the intended meaning that $t$ and $t'$ are equal expressions from $u$ to $v$.

The associated typing rules are

- for every $t \in C_{n+1}$ with $\partial_n^-(t) = u$ and $\partial_n^+(t) = v$,

$$ \vdash t: u \to v $$

- for every $u \in C_n$,

$$ \vdash \mathrm{id}_u: u \to u $$

- for every $0 \le i < n$, every $u \in C_{i+1}$ and $v, v' \in C_n$ with $\partial_i^+(u) = \partial_i^-(v)$,

$$ \begin{array}{c} \vdash t: v \to v' \\ \vdash u*_i t: (u*_i v) \to (u*_i v') \end{array} $$

- for every $0 \le i < n$, every $u, u' \in C_n$ and $v \in C_{i+1}$ with $\partial_i^+(u) = \partial_i^-(v)$

$$ \begin{array}{c} \vdash t: u \to u' \\ \vdash t*_i v: (u*_i v) \to (u'_* v) \end{array} $$

- and, for every $u, v, w \in C_n$

$$ \begin{array}{c} \vdash t: u \to v \qquad \vdash t': v \to w \\ \vdash t*_n t': u \to w \end{array} $$
The equality rules, which express different desirable properties of the equality relation, are introduced below. The first rules enforce that equality is an equivalence relation:

$$ \frac{\vdash t: u \to v}{\vdash t = t: u \to v} \qquad \frac{\vdash t = t': u \to v}{\vdash t' = t: u \to v} \qquad \frac{\vdash t = t': u \to v}{\vdash t = t'': u \to v} \qquad (3) $$

The next ones express that that identities are neutral elements for composition:

$$ \frac{\vdash t: u \to v}{\vdash \mathrm{id}_u *_n t = t: u \to v} \qquad \frac{\vdash t: u \to v}{\vdash t *_n \mathrm{id}_v = t: u \to v} \\ \frac{\vdash t: u \to u' \qquad i < n}{\vdash \mathrm{id}^{i+1}_{\partial_i^-(u)} *_i t = t: u \to u'} \qquad \frac{\vdash t: u \to u'}{\vdash t *_i \mathrm{id}^{i+1}_{\partial_i^+(u)} = t: u \to u'} $$

The next ones express that composition is associative:

$$ \frac{\vdash t_1: u_0 \to u_1 \qquad \vdash t_2: u_1 \to u_2 \qquad \vdash t_3: u_2 \to u_3}{\vdash (t_1 *_n t_2) *_n t_3 = t_1 *_n (t_2 *_n t_3): u_0 \to u_3} \\ \frac{\vdash t: v \to v' \qquad u_1, u_2 \in C_{i+1} \qquad \partial_i^+(u_1) = \partial_i^-(u_2) \qquad \partial_i^+(u_2) = \partial_i^-(v)}{\vdash u_1 *_i (u_2 *_i t) = (u_1 *_i u_2) *_i t: u_1 *_i u_2 *_i v \to u_1 *_i u_2 *_i v'} \\ \frac{\vdash t: u \to u' \qquad v_1, v_2 \in C_{i+1} \qquad \partial_i^+(u) = \partial_i^-(v_1) \qquad \partial_i^+(v_1) = \partial_i^-(v_2)}{\vdash (t *_i v_1) *_i v_2 = t *_i (v_1 *_i v_2): u *_i v_1 *_i v_2 \to u' *_i v_1 *_i v_2} \\ \frac{\vdash t: v \to v' \qquad i < n \qquad u \in C_{i+1} \qquad w \in C_{i+1} \qquad \partial_i^+(u) = \partial_i^-(v) \qquad \partial_i^+(v') = \partial_i^-(w)}{\vdash (u *_i t) *_i w = u *_i (t *_i w): u *_i v *_i w \to u *_i v' *_i w} $$

The next ones express that $(n+1)$-identities are compatible with low-dimensional compositions:

$$ \frac{i < n \qquad u \in C_{i+1} \qquad v \in C_n \qquad \partial_i^+(u) = \partial_i^-(v)}{\vdash u *_i \mathrm{id}_v = \mathrm{id}_{u*_i v}: u *_i v \to u *_i v} \\ \frac{u \in C_n \qquad i < n \qquad v \in C_i \qquad \partial_i^+(u) = \partial_i^-(v)}{\vdash \mathrm{id}_u *_i v = \mathrm{id}_{u*_i v}: u *_i v \to u *_i v} $$

The next ones express that $n$-compositions are compatible with low dimensional compositions:

$$ \frac{\vdash t_1: v_1 \to v_2 \qquad \vdash t_2: v_2 \to v_3 \qquad u \in C_{i+1} \qquad \partial_i^+(u) = \partial_i^-(v_1)}{\vdash u *_i (t_1 *_n t_2) = (u *_i t_1) *_n (u *_i t_2): u *_i v_1 \to u *_i v_3} \\ \frac{\vdash t_1: u_1 \to u_2 \qquad \vdash t_2: u_2 \to u_3 \qquad v \in C_{i+1} \qquad \partial_i^+(u_1) = \partial_i^-(v)}{\vdash (t_1 *_n t_2) *_i v = (t_1 *_i v) *_n (t_2 *_i v): u_1 *_i v \to u_3 *_i v} $$

The next ones express the distributivity properties between the different low-dimensional compositions:

$$ \frac{\vdash t: w \to w' \qquad i < j < n \qquad u \in C_{i+1} \qquad \partial_i^+(u) = \partial_i^-(w) \qquad v \in C_{j+1} \qquad \partial_j^+(v) = \partial_j^-(w)}{\vdash u *_i (v *_j t) = (u *_i v) *_j (u *_i t): u *_i (v *_j w) \to u *_i (v *_j w')} \\ \frac{\vdash t: v \to v' \qquad i < j < n \qquad u \in C_{i+1} \qquad \partial_i^+(u) = \partial_i^-(v) \qquad w \in C_{j+1} \qquad \partial_j^+(v) = \partial_j^-(w)}{\vdash u *_i (t *_j w) = (u *_i t) *_j (u *_i w): u *_i (v *_j w) \to u *_i (v' *_j w)} \\ \frac{\vdash t: v \to v' \qquad i < j < n \qquad u \in C_{j+1} \qquad \partial_j^+(u) = \partial_j^-(v) \qquad w \in C_{i+1} \qquad \partial_i^+(v) = \partial_i^-(w)}{\vdash (u *_j t) *_i w = (u *_i w) *_j (t *_i w): (u *_j v) *_i w \to (u *_j v') *_i w} \\ \frac{\vdash t: u \to u' \qquad i < j < n \qquad v \in C_{j+1} \qquad \partial_j^+(u) = \partial_j^-(v) \qquad w \in C_{i+1} \qquad \partial_i^+(v) = \partial_i^-(w)}{\vdash (t *_j v) *_i w = (t *_i w) *_j (v *_i w): (u *_j v) *_i w \to (u' *_j v) *_i w} $$

Finally, the last ones express that equality is contextual:
$$
\begin{array}{r@{\quad}l@{\qquad}l}
\vdash t = t': v \to v' & u \in C_{i+1} & \partial_i^+(u) = \partial_i^-(v) \\
\multicolumn{3}{c}{\vdash u *_i t = u*_i t': u*_i v \to u*_i v'} \\
\multicolumn{3}{c}{\vdash t = t': u \to u'} & v \in C_{i+1} & \partial_i^+(u) = \partial_i^-(v) \\
\multicolumn{3}{c}{\vdash t*_i v = t'*_i v': u*_i v \to u'*_i v} \\
\multicolumn{3}{c}{\vdash t_1 = t'_1: u_1 \to u_2} & \vdash t_2: u_2 \to u_3 \\
\multicolumn{3}{c}{\vdash t_1*_n t_2 = t'_1*_n t_2: u_1 \to u_3} \\
\multicolumn{3}{c}{\vdash t_1: u_1 \to u_2} & \vdash t_2 = t'_2: u_2 \to u_3 \\
\multicolumn{3}{c}{\vdash t_1*_n t_2 = t_1*_n t'_2: u_1 \to u_3}
\end{array}
$$

The following lemmas show that typing is unique and well-behaved regarding equality. They are
easily shown by inductions on the derivations:

**Lemma 1.7.1** (Uniqueness of typing). *Given an expression t such that the judgements *$\vdash$ t: u $\to$ v* and *$\vdash$ t: u' $\to$ v' are derivable, we have u = u' and v = v'.*

**Lemma 1.7.2.** If $\vdash t = t'$: $u \to v$ is derivable then $\vdash t: u \to v$ and $\vdash t'$: $u \to v$ are derivable.

A term *t* is *well-typed* if there are *u*, *v* ∈ *C*<sub>*n*</sub> such that *t*: *u* → *v* is derivable using the above rules. In this case, by Lemma 1.7.1, the types *u* and *v* are uniquely determined by *t*, and we write *∂*<sub>*n*</sub><sup>-</sup>(*t*) = *u* and *∂*<sub>*n*</sub><sup>+</sup>(*t*) = *v*. We define *C*<sub>*n*+1</sub><sup>*</sup> to be the set of equivalence classes under = of well-typed expressions. By Lemma 1.7.2, the operations *∂*<sub>*n*</sub><sup>-</sup> and *∂*<sub>*n*</sub><sup>+</sup> are compatible with the relation =. We finally define *L*<sub>*n*</sub>(*C*, *C*<sub>*n*+1</sub>) as the (*n*+1)-precategory with *C* as underlying *n*-precategory, *C*<sub>*n*+1</sub><sup>*</sup> as set of (*n*+1)-cells, with sources and targets given by the maps *∂*<sub>*n*</sub><sup>-</sup> and *∂*<sub>*n*</sub><sup>+</sup>. The compositions and identities on the (*n*+1)-cells are induced in the expected way by the corresponding syntactic constructions (this is well-defined by the axioms of =). It is routine to verify that:

**Theorem 1.7.3.** *The above construction defines a functor *L*<sub>*n*</sub> which is left adjoint to *W*<sub>*n*</sub>.*

1.8 Normal form for cells

Suppose given $(C, C_{n+1}) \in \mathbf{PCat}_n^+$. The set $C_{n+1}^*$ of cells of $\mathcal{L}_n(C, C_{n+1})$ was described in the previous section as a quotient of expressions modulo a congruence $=$. In order to conveniently work with its equivalence classes, we introduce here a notion of normal form for those. From now on, we adopt the convention that missing parenthesis in expressions are implicitly bracketed on the right, i.e., we write $u_1 *_n u_2 * _n \cdots * _n u_k$ instead of $u_1 * _n (u_2 * _n (\cdots * _n u_k))$.

By removing the relations (3) in the definition of the congruence = and orienting from left to
right the remaining equations, we obtain a relation $\Rightarrow$ which can be interpreted as a rewriting
relation on expressions:

$$
\begin{array}{l@{\qquad}l}
\mathrm{id}_u *_n t \Rightarrow t & t*_n \mathrm{id}_u \Rightarrow t \\
(t_1*_n t_2)*_n t_3 \Rightarrow t_1*_n (t_2*_n t_3) & (u_1*_i t_n)*_i u_2 \Rightarrow u_1*_i (t_n*_i u_2) \\
\dots & \dots
\end{array}
$$

We now study the properties of $\Rightarrow$. We recall that such a relation is said to be *terminating* when there is no infinite sequence $(t_i)_{i \ge 0}$ such that $t_i \Rightarrow t_{i+1}$ for $i \ge 0$. A *normal form* is an expression *t* such that there exists no *t'* with *t* $\Rightarrow$ *t'*. Writing $\Rightarrow^*$ for the reflexive transitive closure of $\Rightarrow$, the relation $\Rightarrow$ is said *locally confluent* when for all expressions *t*, *t*<sub>1</sub> and *t*<sub>2</sub> such that *t* $\Rightarrow$ *t*<sub>1</sub> and *t* $\Rightarrow$ *t*<sub>2</sub>, we have $t_1 \Rightarrow^* t'$ and $t_2 \Rightarrow^* t'$ for some expression *t'* (diagram on the left) and *confluent* when for all expressions *t*, *t*<sub>1</sub> and *t*<sub>2</sub> such that *t* $\Rightarrow^* t_1$ and *t* $\Rightarrow^* t_2$, we have $t_1 \Rightarrow^* t'$ and $t_2 \Rightarrow^* t'$ for some expression *t'* (diagram on the right):

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

Those notions are introduced in more details in [2].
**Lemma 1.8.1.** The relation $\Rightarrow$ is terminating.

*Proof.* In order to show termination, we define a measure on the terms that is decreased by each rewriting operation. To do so, we first define counting functions $c_n$ and $l_i, r_i$ for $0 \le i < n$ from expressions to $\mathbb{N}$ that take into account the three kinds of operations in the expression: top $n$-dimensional compositions, and lower $i$-dimensional left and right compositions. These functions count the numbers of potential reductions in an expression $t$ with the associated operations. Since reductions involving composition operations change value of counting functions of composition operations of lower dimension, we will use a lexicographical ordering of the counting functions to obtain the wanted measure. Given an expression $t$, we define $c_n(t) \in \mathbb{N}$ and $l_i(t), r_i(t) \in \mathbb{N}$ for $0 \le i < n$ by induction on $t$ as follows:

- if $g \in C_{n+1}$, we put $c_n(g) = l_i(g) = r_i(g) = 0$ for $0 \le i < n$,

- if $u \in C_n$, we put $c_n(id_u) = l_i(id_u) = r_i(id_u) = 1$,

- if $t = t_1 *_n t_2$, we put

$$ 
\begin{aligned}
c_n(t) &= 2c_n(t_1) + c_n(t_2) + 1, \\
l_i(t) &= l_i(t_1) + l_i(t_2) + 2, \\
r_i(t) &= r_i(t_1) + r_i(t_2) + 2,
\end{aligned}
$$

- if $t = u *_j t'$, we put $c_n(t) = c_n(t')$ and

$$ l_i(t) = \begin{cases} l_i(t') & \text{if } j < i, \\ 2l_i(t') + 1 & \text{if } j = i, \\ l_i(t') + 1 & \text{if } j > i, \end{cases} \qquad r_i(t) = \begin{cases} r_i(t') & \text{if } j < i, \\ r_i(t') + 1 & \text{if } j \ge i, \end{cases} $$

- if $t = t' *_j v$, we put $c_n(t) = c_n(t')$ and

$$ l_i(t) = \begin{cases} l_i(t') & \text{if } j \le i, \\ l_i(t') + 1 & \text{if } j > i, \end{cases} \qquad r_i(t) = \begin{cases} r_i(t') & \text{if } j < i, \\ 2r_i(t') + 1 & \text{if } j = i, \\ r_i(t') + 1 & \text{if } j > i. \end{cases} $$

For each expression $t$, we define

$$ N(t) = (c_n(t), l_{n-1}(t), r_{n-1}(t), \dots, l_0(t), r_0(t)) \in \mathbb{N}^{2n+1} $$

and consider the lexicographical ordering $<_{lex}$ on $\mathbb{N}^{2n+1}$. For the inductive rules of $\Rightarrow$, we observe that

- if $t = t_1 *_n t_2$ and $t' = t'_1 *_n t_2$ with $N(t_1) <_{lex} N(t'_1)$, then $N(t) <_{lex} N(t'_1)$,

- if $t = t_1 *_n t_2$ and $t' = t_1 *_n t'_2$ with $N(t'_2) <_{lex} N(t_2)$, then $N(t') <_{lex} N(t)$,

- if $t = u *'_i \tilde{t}$ and $t' = u *'_i \tilde{t}'$ with $N(\tilde{t}) <_{lex} N(\tilde{t})$, then $N(t') <_{lex} N(t)$,

- if $t = \tilde{t} *'_i v$ and $t' = \tilde{t}' *'_i v$ with $N(\tilde{t}) <_{lex} N(\tilde{t})$, then $N(t') <_{lex} N(t)$.

It is sufficient to prove that the other reduction rules decrease the norm $N(-)$. We only cover the most representative cases by computing the first component of $N(-)$ modified by the reduction rule and showing that it is strictly decreasing:

$$ 
\begin{aligned}
c_n(id_u *_n t) &= c_n(t) + 3 > c_n(t), \\
c_n((t_1 *_n t_2) *_n t_3) &= 4c_n(t_1) + 2c_n(t_2) + c_n(t_3) + 3 \\
&> 2c_n(t_1) + 2c_n(t_2) + c_n(t_3) + 2 = c_n(t_1 *_n (t_2 *_n t_3)), \\
l_i(u_1 *'_i (u_2 *'_i t)) &= 4l_i(t) + 3 > 2l_i(t) + 1 = l_i((u_1 *'_i u_2) *'_i t), \\
r_i((u_1 *'_i t) *'_i u_2) &= 2r_i(t) + 3 > 2r_i(t) + 2 = r_i(u_1 *'_i (t *'_i u_2)), \\
l_i(u *'_i (t_1 *_n t_2)) &= 2l_i(t_1) + 2l_i(t_2) + 5 \\
&> 2l_i(t_1) + 2l_i(t_2) + 4 = l_i((u *'_i t_1) *_n (u *'_i t_2)), \\
l_i(u *'_i (v *'_j t)) &= 2l_i(t) + 3 > 2l_i(t) + 2 = l_i((u *'_i v) *'_j (u *'_i t)) \text{ for } j > i.
\end{aligned}
$$
Thus, if $t \Rightarrow t'$, we have $N(t') <_{lex} N(t)$. Since the lexicographical order $<_{lex}$ on $\mathbb{N}^{2n+1}$ is well-founded, the reduction rule $\Rightarrow$ is terminating. $\square$

**Lemma 1.8.2.** *The relation $\Rightarrow$ is locally confluent.*

*Proof.* By a direct adaptation of the critical pair lemma (for example [2, Thm. 6.2.4]), it is enough to show that all critical branchings are confluent, which can be checked by direct computation. For example, given $t_1, t_2, t_3$ and $t_4$ suitably typed, there is a critical branching given by the reductions

$$ (t_1 *_{n} (t_2 *_{n} t_3)) *_{n} t_4 \Leftarrow ((t_1 *_{n} t_2) *_{n} t_3) *_{n} t_4 \Rightarrow (t_1 *_{n} t_2) *_{n} (t_3 *_{n} t_4). $$

This branching is confluent since

$$ (t_1 *_{n} (t_2 *_{n} t_3)) *_{n} t_4 \Rightarrow t_1 *_{n} ((t_2 *_{n} t_3) *_{n} t_4) \Rightarrow t_1 *_{n} (t_2 *_{n} (t_3 *_{n} t_4)) $$

and

$$ (t_1 *_{n} t_2) *_{n} (t_3 *_{n} t_4) \Rightarrow t_1 *_{n} (t_2 *_{n} (t_3 *_{n} t_4)). $$

Another critical branching is given by the reductions

$$ (u_1 *_{i} u_2) *_{i} (t_1 *_{n} t_2) \Leftarrow u_1 *_{i} (u_2 *_{i} (t_1 *_{n} t_2)) \Rightarrow u_1 *_{i} ((u_2 *_{i} t_1) *_{n} (u_2 *_{i} t_2)) $$

for $u_1, u_2 \in C_i$ with $i \le n$ and $t_1, t_2$ suitably typed. This branching is confluent since

$$ (u_1 *_{i} u_2) *_{i} (t_1 *_{n} t_2) \Rightarrow ((u_1 *_{i} u_2) *_{i} t_1) *_{n} ((u_1 *_{i} u_2) *_{i} t_2) $$

and

$$ u_1 *_{i} ((u_2 *_{i} t_1) *_{n} (u_2 *_{i} t_2)) \Rightarrow (u_1 *_{i} (u_2 *_{i} t_1)) *_{n} (u_1 *_{i} (u_2 *_{i} t_2)) \\ \Rightarrow ((u_1 *_{i} u_2) *_{i} t_1) *_{n} ((u_1 *_{i} u_2) *_{i} t_2). $$

The other cases are similar. $\square$

**Theorem 1.8.3.** Any cell in $u \in C_{n+1}^*$ admits a unique representative by an expression of the form

$$ u = u_1 *_{n} u_2 *_{n} \cdots *_{n} u_k $$

where each $u_i$ decomposes as

$$ u_i = v_n^i *_{n-1} (\cdots *_2 (v_2^i *_1 (v_1^i *_0 A^i *_0 w_1^i) *_1 w_2^i) *_2 \cdots) *_{n-1} w_n^i \quad (4) $$

where $A^i$ is an element of $C_{n+1}$ and $v_j^i$ and $w_j^i$ are j-cells in $C_j$.

*Proof.* We have seen in Lemma 1.8.1 and Lemma 1.8.2 that the relation $\Rightarrow$ is terminating and locally confluent. By Newman's lemma (see, for example, [2, Lem. 2.7.2]), it is thus confluent and every equivalence class of expressions contains a unique normal form, which can be obtained by reducing any expression to its normal form. It can be checked that those normal forms are in bijective correspondence with the expression of the form (4) (essentially, those expressions are normal forms where identities have been suitably inserted). $\square$

A cell of $C_{n+1}^*$ of the form (4) is called a *whisker*. By the inductive definition of prepolygraphs from Section 1.5 and Theorem 1.8.3, given an $m$-prepolygraph $P$ with $m > 0$, an $(i+1)$-cell $u \in P_{i+1}^*$ with $i \in \{0, \dots, m-1\}$ can be uniquely written as a composite of $(i+1)$-dimensional whiskers $u_1 *_{i} \cdots *_{i} u_k$ for a unique $k \in \mathbb{N}$ that is called the *length* of $u$ and denoted by $|u|$. Moreover, each whisker $u_j$ admits a unique decomposition of the form (4). We will extensively use this canonical form for cells of precategories freely generated by a prepolygraph in the following, often omitting to invoke Theorem 1.8.3.
- if $F_i = \mathrm{id}_\psi$ for some $i \in \{1, \dots, k\}$ and $\psi \in C_2$, then

$$ (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} = (F_1^{\epsilon_1}, \dots, F_{i-1}^{\epsilon_{i-1}}, F_{i+1}^{\epsilon_{i+1}}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} $$

- if $\epsilon_i = \epsilon_{i+1} = +$ for some $i \in \{1, \dots, k-1\}$, then

$$ (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} = (F_1^{\epsilon_1}, \dots, F_{i-1}^{\epsilon_{i-1}}, (F_i *_2 F_{i+1})^+, F_{i+2}^{\epsilon_{i+2}}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} $$

- if $\epsilon_i = \epsilon_{i+1} = -$ for some $i \in \{1, \dots, k-1\}$, then

$$ (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} = (F_1^{\epsilon_1}, \dots, F_{i-1}^{\epsilon_{i-1}}, (F_{i+1} *_2 F_i)^-, F_{i+2}^{\epsilon_{i+2}}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} $$

- if $\{\epsilon_i, \epsilon_{i+1}\} = \{-, +\}$ and $F_i = F_{i+1}$ for some $i \in \{1, \dots, k-1\}$, then

$$ (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} = (F_1^{\epsilon_1}, \dots, F_{i-1}^{\epsilon_{i-1}}, F_{i+2}^{\epsilon_{i+2}}, \dots, F_k^{\epsilon_k})_{\phi, \phi'} $$

Since the definitions of source and target of zigzags are compatible with the above equalities, they induce source and target operations $\partial^-, \partial^+$: $(C^\top)_3 \to C_2$. Given

$$ F = (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi_1, \phi_2} \in (C^\top)_3 \quad \text{and} \quad G = (G_1^{\delta_1}, \dots, G_l^{\delta_l})_{\phi_2, \phi_3} \in (C^\top)_3, $$

we define $F *_2 G$ as

$$ F *_2 G = (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k}, G_1^{\delta_1}, \dots, G_l^{\delta_l})_{\phi_1, \phi_3} $$

and, given $i \in \{0, 1\}$, $u \in C_{i+1}$ and $F = (F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'}$ with $\partial_i^+(u) = \partial_i^-(\phi)$, we define $u *_i F$ as

$$ u *_i F = ((u *_i F_1)^{\epsilon_1}, \dots, (u *_i F_k)^{\epsilon_k})_{u*_i \phi, u*_i \phi'} $$

and, finally, given $\phi \in C_2$, we define $\mathrm{id}_\phi$ as $()_{\phi, \phi}$. All these operations are compatible with the quotient equalities above, and they equip $C^\top$ with a structure of 3-precategory.

There is a canonical 3-prefunctor $H: C \to C^\top$ sending $F: \phi \Rightarrow \psi \in C_3$ to $(F^+)^{\phi, \psi}$. Moreover, given a (3, 2)-precategory $D$ and a 3-prefunctor $G: C \to D$, we can define $G': C^\top \to D$ by putting $G'(u) = G(u)$ for $u \in C_i$ with $i \le 2$ and

$$ G'((F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{\phi, \phi'}) = G'(F_1^{\epsilon_1}) *_2 \dots *_2 G'(F_k^{\epsilon_k}) $$

for a zigzag $(F_1^{\epsilon_1}, \dots, F_k^{\epsilon_k})_{u, v}$ where

$$ G'(F^\epsilon) = \begin{cases} G(F) & \text{if } \epsilon = + \\ G(F)^{-1} & \text{if } \epsilon = - \end{cases} $$

for $F \in C_3$ and $\epsilon \in \{-, +\}$. The definition of $G'$ is compatible with the quotient equalities above so that $G'$ is well-defined, and $G'$ can be shown to uniquely factorize $G$ through $H$. Hence, $(-)^\top$ is indeed a left adjoint for $\mathcal{U}$. In the following, given a 3-precategory $C$ and $F \in C_3$, we often write $F$ for $H(F)$.

## 2 Gray categories

Strict 3-categories are categories enriched in the monoidal category $\mathbf{Cat}_2$ equipped with the cartesian product. Similarly, Gray categories are categories enriched in the monoidal category $\mathbf{Cat}_2$ equipped with the Gray tensor product. The latter can be seen as an “asynchronous” variant of the cartesian product, similar to the funny tensor product, where two interleavings of the same morphisms are related by “exchange” cells. Typically, consider the 1-categories $C$ and $D$ below

$$ C = x \xrightarrow{f} x' $$

$$ D = y \xrightarrow{g} y' $$
their funny and Gray tensor products are respectively

$$ C \square D = \begin{array}{rcl} (x, y) & \xrightarrow{(f, y)} & (x', y) \\ \downarrow_{(x,g)} & & \downarrow_{(x',g)} \\ (x, y') & \xrightarrow{(f, y')} & (x', y') \end{array} $$

$$ C \boxtimes D = \begin{array}{rcl} (x, y) & \xrightarrow{(f, y)} & (x', y) \\ \downarrow_{(x,g)} & & \downarrow_{(x',g)} \\ (x, y') & \xrightarrow{(f, y')} & (x', y') \end{array} $$

where the exchange 2-cell $\chi$ can be invertible or not, depending on whether we consider the pseudo or lax variant of the Gray tensor product. We first recall quickly the definition of the Gray tensor product, both in its lax and pseudo variants. We then give a more explicit description in terms of generators and relations of categories enriched in 2-categories with the Gray tensor product. Then, we give a way for presenting canonically a Gray category.

## 2.1 The Gray tensor products

We recall here the definitions of the Gray tensor products on 2-categories, in its lax and pseudo variants. We refer the reader to [12, Sec. I,4] for details.

A (strict) 2-category is a 2-precategory $C$ such that, for all $\phi, \psi \in C_2$ with $\partial_0^+(\phi) = \partial_0^-(\psi)$,

$$ (\phi *_0 \partial_1^-(\psi)) *_1 (\partial_1^+(\phi) *_0 \psi) = (\partial_1^-(\phi) *_0 \psi) *_1 (\phi *_0 \partial_1^+(\psi)). $$

We denote $\mathbf{Cat}_2$ the full subcategory of $\mathbf{PCat}_2$ whose objects are 2-categories. We write 1 for the terminal 2-category and we write * for its unique 0-cell.

Given $C$ and $D$ two 2-categories, we write $C \boxtimes^{\text{lax}} D$ for the 2-category which is presented as follows:

- the 0-cells of $C \boxtimes^{\text{lax}} D$ are the pairs $(x, y)$ where $x \in C_0$ and $y \in D_0$,

- the 1-cells of $C \boxtimes^{\text{lax}} D$ are generated by 1-cells

$$ (f, y) : (x, y) \to (x', y) \quad \text{and} \quad (x, g) : (x, y) \to (x, y'), $$

$$ \text{for } f: x \to x' \in C_1 \text{ and } g: y \to y' \in C_2, $$

- the 2-cells of $C \boxtimes^{\text{lax}} D$ are generated by the 2-cells

$$ (\phi, y) : (f, y) \to (f', y) \quad \text{and} \quad (x, \psi) : (x, g) \to (x, g') $$

$$ \text{for } \phi: f \Rightarrow f' \in C_2, \psi: g \Rightarrow g' \in C_2 \text{ and } x, y \in C_0, \text{ and by the 2-cells} $$

$$ \begin{array}{ccc} (x, y) & \xrightarrow{(f, y)} & (x', y) \\ \downarrow_{(x,g)} & & \downarrow_{(x',g)} \\ (x, y') & \xrightarrow{(f, y')} & (x', y') \end{array} $$

$$ \text{for } f: x \to x' \in C_1 \text{ and } g: y \to y' \in C_1, $$

under the conditions that

(i) the 1-generators are compatible with 0-composition, meaning that

$$ (\mathrm{id}_x, y) = (x, \mathrm{id}_y) = \mathrm{id}_{(x,y)} $$

$$ (f *_0 f', y) = (f, y) *_0 (f', y) $$

$$ (x, g *_0 g') = (x, g) *_0 (x, g') $$

$$ \text{for all } x \in C_0, y \in D_0, \text{ 0-composable } f, f' \in C_1 \text{ and 0-composable } g, g' \in D_1, $$
(ii) the 2-generators are compatible with 0-composition, meaning that

$$(\mathrm{id}_x^2, y) = (x, \mathrm{id}_y^2) = \mathrm{id}_{(x,y)}^2$$

$$(\phi_1 *_0 \phi_2, y) = (\phi_1, y) *_0 (\phi_2, y)$$

$$(x, \psi_1 *_0 \psi_2) = (x, \psi_1) *_0 (x, \psi_2)$$

for all $x \in C_0$, $y \in D_0$, 0-composable $\phi_1, \phi_2 \in C_2$ and 0-composable $\psi_1, \psi_2 \in D_2$, i.e., graphically,

$$ (x, y) \underset{(\mathrm{id}_x, y)}{\overset{(\mathrm{id}_x, y)}{\rightleftharpoons}} (x, y) = (x, y) \underset{(x, \mathrm{id}_y)}{\overset{(x, \mathrm{id}_y)}{\rightleftharpoons}} (x, y) = (x, y) \underset{(\mathrm{id}_x, y)}{\overset{(\mathrm{id}_x, y)}{\rightleftharpoons}} (x, y) $$

$$ (x_0, y) \underset{(f'_1 *_0 f'_2, y)}{\overset{(f_1 *_0 f_2, y)}{\rightleftharpoons}} (x_2, y) = (x_0, y) \underset{(f'_1, y)}{\overset{(f_1, y)}{\rightleftharpoons}} (x_1, y) \underset{(f'_2, y)}{\overset{(f_2, y)}{\rightleftharpoons}} (x_2, y) $$

$$ (x, y_0) \underset{(x, g'_1 *_0 g'_2)}{\overset{(x, g_1 *_0 g_2)}{\rightleftharpoons}} (x, y_2) = (x, y_0) \underset{(x, g'_1)}{\overset{(x, g_1)}{\rightleftharpoons}} (x, y_1) \underset{(x, g'_2)}{\overset{(x, g_2)}{\rightleftharpoons}} (x, y_2) $$

(iii) the 2-generators are compatible with 1-composition, meaning that

$$(\mathrm{id}_f, y) = \mathrm{id}_{(f, y)}$$

$$(\phi_1 *_1 \phi_2, y) = (\phi_1, y) *_1 (\phi_2, y)$$

$$(x, \mathrm{id}_g) = \mathrm{id}_{(x, g)}$$

$$(x, \psi_1 *_1 \psi_2) = (x, \psi_1) *_1 (x, \psi_2)$$

for all $\phi_i: f_{i-1} \Rightarrow f_i: x \to x'$ and $\psi_i: g_{i-1} \Rightarrow g_i: y \to y'$ for $i \in \{1, 2\}$ and $f: x \to x'$ and $g: y \to y'$, i.e., graphically,

$$ (x, y) \underset{(f, y)}{\overset{(f, y)}{\rightleftharpoons}} (x', y) = (x, y) \underset{(f, y)}{\overset{(f, y)}{\rightleftharpoons}} (x', y) $$

$$ (x, y) \underset{(f_2, y)}{\overset{(f_0, y)}{\rightleftharpoons}} (x', y) = (x, y) \underset{(f_2, y)}{\overset{(f_0, y)}{\rightleftharpoons}} (x', y) \quad (x, y) \underset{(f_1, y)}{\overset{(f_1, y)}{\rightleftharpoons}} (x', y) $$

$$ (x, y) \underset{(x, g)}{\overset{(x, g)}{\rightleftharpoons}} (x, y') = (x, y) \underset{(x, g)}{\overset{(x, g)}{\rightleftharpoons}} (x, y') $$
$$ (x, y) \underset{(x,g_2)}{\overset{(x,g_0)}{\rightleftharpoons}} (x, y') = (x, y) \underset{(x,g_2)}{\overset{(x,g_0)}{\rightleftharpoons}} \left( \begin{array}{c} \Downarrow(x, \psi_1) \\ \Downarrow(x, \psi_2) \end{array} \right) \underset{(x,g_1)}{\longrightarrow} (x', y) $$

(iv) the interchangers are compatible with 0-composition, meaning that

$$ (\mathrm{id}_x, g) = \mathrm{id}_{(x,g)} $$

$$ (f_1 *_0 f_2, g) = ((f_1, y) *_0 (f_2, g)) *_1 ((f_1, g) *_0 (f_2, y')) $$

$$ (f, \mathrm{id}_y) = \mathrm{id}_{(f,y)} $$

$$ (f, g_1 *_0 g_2) = ((f, g_1) *_0 (x', g_2)) *_1 ((x, g_1) *_0 (f, g_2)) $$

for all $f_i: x_{i-1} \to x_i$ and $g_i: y_{i-1} \to y_i$ for $i \in \{1, 2\}$ and $f: x \to x'$ and $g: y \to y'$, i.e., graphically,

$$ \begin{array}{ccc} (x, y) & \xrightarrow{(\mathrm{id}_x, y)} & (x, y) \\ \downarrow_{(x,g)} & \underset{(\mathrm{id}_x,g)}{\rightleftharpoons} & \downarrow_{(x,g)} \\ (x, y') & \xrightarrow{(\mathrm{id}_x, y')} & (x, y') \end{array} = \begin{array}{c} (x, y) \\ (x,g) \\ (x, y') \end{array} \underset{(x,g)}{\overset{(\mathrm{id}_{(x,g)}, g)}{\rightleftharpoons}} \begin{array}{c} (x, y) \\ (x,g) \\ (x, y') \end{array} $$

$$ \begin{array}{ccc} (x_0, y) & \xrightarrow{(f_1 *_0 f_2, y)} & (x_2, y) \\ \downarrow_{(x_0,g)} & \underset{(f_1 *_0 f_2, g)}{\rightleftharpoons} & \downarrow_{(x_2,g)} \\ (x_0, y') & \xrightarrow{(f_1 *_0 f_2, y')} & (x_2, y') \end{array} = \begin{array}{c} (x_0, y) \\ (x_0,g) \\ (x_0, y') \end{array} \underset{(f_1, y')}{\overset{(f_1, y)}{\rightleftharpoons}} \begin{array}{c} (x_1, y) \\ (x_1,g) \\ (x_1, y') \end{array} \underset{(f_2, y')}{\overset{(f_2, y)}{\rightleftharpoons}} \begin{array}{c} (x_2, y) \\ (x_2,g) \\ (x_2, y') \end{array} $$

$$ \begin{array}{ccc} (x, y) & \xrightarrow{(f,y)} & (x', y) \\ \downarrow_{(x,id_y)} & \underset{(f,y)}{\rightleftharpoons} & \downarrow_{(x',id_y)} \\ (x, y) & \xrightarrow{(f,y)} & (x', y) \end{array} = \begin{array}{c} (x, y) \\ (x,y) \\ (x,y) \end{array} \underset{(f,y)}{\overset{(f,y)}{\rightleftharpoons}} \begin{array}{c} (x', y) \\ (x',y) \\ (x',y) \end{array} $$

$$ \begin{array}{ccc} (x, y_0) & \xrightarrow{(f, y_0)} & (x', y_0) \\ \downarrow_{(x,g_1)} & \underset{(x, y_0)}{\rightleftharpoons} & \downarrow_{(x', g_1)} \\ (x, y_2) & \xrightarrow{(f, y_2)} & (x', y_2) \end{array} = \begin{array}{c} (x, y_0) \\ (x,g_1) \\ (x,g_2) \end{array} \underset{(f, y_1)}{\overset{(f, y_1)}{\rightleftharpoons}} \begin{array}{c} (x', y_1) \\ (x', y_2) \\ (x', y_2) \end{array} $$

(v) the interchangers commute with the 2-generators, meaning that

$$ ((f,g) *_1 ((x,g) *_0 (\phi, y'))) = (((\phi, y) *_0 (x', g)) *_1 (f', g)) $$

$$ ((f,g) *_1 ((x, \psi) *_0 (f, y'))) = (((f, y) *_0 (x', \psi)) *_1 (f, g')) $$

for $\phi: f \Rightarrow f'$: $x \to x'$ and $\psi: g \Rightarrow g'$: $y \to y'$, i.e., graphically,

$$ (x, y) \underset{(x,g)}{\overset{(f,y)}{\rightleftharpoons}} (x', y) \underset{(x,g)}{\overset{(f,y)}{\rightleftharpoons}} (x', y') \underset{(x,g)}{\overset{(f',y)}{\rightleftharpoons}} (x', y') = (x, y) \underset{(x,g)}{\overset{(f, y)}{\rightleftharpoons}} (x', y) \underset{(x,g)}{\overset{(f',y)}{\rightleftharpoons}} (x', y') $$
$$ (x, y) \xrightarrow{(f, y)} (x', y) \qquad (x, y) \xrightarrow{(f, y)} (x', y) \\ (x, g') \underset{(x, y)}{\overset{(x, \psi)}{\rightleftharpoons}} (x, g) \quad (f, g) \underset{(f, y)}{\overset{(f, g)}{\rightleftharpoons}} (x', g') \qquad (x, g') \underset{(f, y)}{\xrightarrow{\hspace{2.5cm}}} (x', y') \qquad (x, y') \underset{(f, y)}{\xrightarrow{\hspace{2.5cm}}} (x', y') \\ (x, g') \underset{(f, y)}{\xrightarrow{\hspace{2.5cm}}} (x', y') \qquad (x, g') \underset{(f, y)}{\xrightarrow{\hspace{2.5cm}}} (x', y') \qquad (x, g') \underset{(f, y)}{\xrightarrow{\hspace{2.5cm}}} (x', y') $$

The construction extends to a bifunctor $\mathbf{Cat}_2 \times \mathbf{Cat}_2 \to \mathbf{Cat}_2$ by defining, for $F: C \to C'$ and $G: D \to D'$, $F \boxtimes^{\text{lax}} G$ as the unique functor mapping

$$ (\phi, y) \mapsto (F(\phi), G(y)) $$

$$ (x, \psi) \mapsto (F(x), G(\psi)) $$

$$ (f, g) \mapsto (F(f), G(g)) $$

for all $x \in C_0$, $y \in D_0$, $\phi \in C_2$, $\psi \in D_2$, $f \in C_1$ and $g \in D_1$.

For $C, D, E \in \mathbf{Cat}_2$, there is a 2-functor

$$ \alpha_{C,D,E}^{\text{lax}} : (C \boxtimes^{\text{lax}} D) \boxtimes^{\text{lax}} E \xrightarrow{\sim} C \boxtimes^{\text{lax}} (D \boxtimes^{\text{lax}} E) $$

which is an isomorphism natural in $C, D, E$ and uniquely defined by the following mappings on generators

$$ ((\phi, y), z) \mapsto (\phi, (y, z)) $$

$$ ((f, g), z) \mapsto (f, (g, z)) $$

$$ ((x, \psi), z) \mapsto (x, (\psi, z)) $$

$$ ((f, y), h) \mapsto (f, (y, h)) $$

$$ ((x, y), \gamma) \mapsto (x, (y, \gamma)) $$

$$ ((x, g), h) \mapsto (x, (g, h)) $$

for $\phi: f \Rightarrow f': x \to x' \in C_2$, $\psi: g \Rightarrow g': y \to y' \in D_2$ and $\gamma: h \Rightarrow h': z \to z' \in E_2$.

For $C \in \mathbf{Cat}_2$, there are two 2-functors

$$ \lambda_C^{\text{lax}} : 1 \boxtimes^{\text{lax}} C \to C \quad \text{and} \quad \rho_C^{\text{lax}} : C \boxtimes^{\text{lax}} 1 \to C $$

which are isomorphisms, natural in $C$, and uniquely defined by the mappings

$$ \lambda^{\text{lax}}((*, \psi)) = \psi \quad \text{and} \quad \rho^{\text{lax}}((\psi, *)) = \psi $$

for $\psi \in C_2$. By checking coherence conditions between $\alpha^{\text{lax}}$, $\lambda^{\text{lax}}$ and $\rho^{\text{lax}}$, we get that:

**Proposition 2.1.1.** The bifunctor $\boxtimes^{\text{lax}}$ together with the unit 1 and the natural isomorphisms $\alpha^{\text{lax}}$, $\lambda^{\text{lax}}$ and $\rho^{\text{lax}}$ equip $\mathbf{Cat}_2$ with a structure of a monoidal category.

The monoidal structure $(\mathbf{Cat}_2, \boxtimes^{\text{lax}}, 1, \alpha^{\text{lax}}, \lambda^{\text{lax}}, \rho^{\text{lax}})$ is called the lax Gray tensor product.

A variant of the Gray tensor is called the pseudo Gray tensor product is the monoidal structure $(\mathbf{Cat}_2, \boxtimes, 1, \alpha, \lambda, \rho)$ where, given $C, D \in \mathbf{Cat}_2$, $C \boxtimes D$ is defined the same way as $C \boxtimes^{\text{lax}} D$, except that we moreover require that the 2-cells $(f, g)$ of $C \boxtimes D$ be invertible. The natural isomorphisms $\alpha, \lambda, \rho$ are uniquely defined by similar mappings than those defining $\alpha^{\text{lax}}, \lambda^{\text{lax}}, \rho^{\text{lax}}$, and we have:

**Proposition 2.1.2.** The bifunctor $\boxtimes$ together with the unit 1 and the natural isomorphisms $\alpha, \lambda, \rho$ equip $\mathbf{Cat}_2$ with a structure of a monoidal category.

## 2.2 Gray categories

For each of the two variants of Gray tensor product defined in the previous section, there is an associated notion of 3-dimensional category as we now describe here.

A lax Gray category [12, I,4.25] is a category enriched in the category of 2-categories equipped with the lax Gray tensor product. A more explicit definition using generators and relations can be given as follows. A Gray category is a 3-precategory $C$ together with, for all every 0-composable
pair of 2-cells $\phi: f \Rightarrow f': x \to y$ and $\psi: g \Rightarrow g': y \to z$, a 3-cell

$$X_{\phi, \psi}:(\phi *_0 g) *_1 (f' *_0 \psi) \Rightarrow (f *_0 \psi) *_1 (\phi *_0 g')$$

which can be represented using string diagrams by

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

called *interchanger* and satisfying the following sets of axioms:

(i) compatibility with compositions and identities: for $\phi: f \Rightarrow f'$, $\phi': f' \Rightarrow f''$, $\psi: g \Rightarrow g'$, $\psi': g' \Rightarrow g''$ in $C_2$ and $e, h$ in $C_1$ such that $e, \phi, \psi$ and $h$ are 0-composable, we have

$$X_{\mathrm{id}_f, \psi} = \mathrm{id}_{f *_0 \psi}$$

$$X_{\phi_1 \phi_1 \psi, \psi} = ((\phi *_0 g) *_1 X_{\phi', \psi}) *_2 (X_{\phi, \psi} *_1 (\phi' *_0 g'))$$

$$X_{\phi, \mathrm{id}_g} = \mathrm{id}_{\phi *_0 g}$$

$$X_{\phi, \psi *_1 \psi'} = (X_{\phi, \psi} *_1 (f' *_0 \psi')) *_2 ((f *_0 \psi) *_1 X_{\phi, \psi'})$$

and

$$X_{e *_0 \phi, \psi} = e *_0 X_{\phi, \psi}$$

$$X_{\phi, \psi *_0 h} = X_{\phi, \psi} *_0 h.$$

Moreover, given $\phi, \psi \in C_2$ and $f \in C_1$ such that $\phi, f$ and $\psi$ are 0-composable, we have

$$X_{\phi *_0 f, \psi} = X_{\phi, f *_0 \psi}$$

(ii) exchange law for 3-cells: for all $A: \phi \Rightarrow \psi \in C_3$ and $B: \psi \Rightarrow \psi' \in C_3$ such that $A$ and $B$ are 1-composable, we have

$$(A *_1 \psi) *_2 (\phi' *_1 B) = (\phi *_1 B) *_2 (A *_1 \psi')$$

(iii) compatibility between interchangers and 3-cells: given

$$A: \phi \Rightarrow \phi': u \Rightarrow u' \in C_3 \quad \text{and} \quad B: \psi \Rightarrow \psi': v \Rightarrow v' \in C_3,$$

such that $A, B$ are 0-composable, we have

$$((A *_0 v) *_1 (u' *_0 \psi)) *_2 X_{\phi', \psi} = X_{\phi, \psi} *_2 ((u *_0 \psi) *_1 (A *_0 v'))$$

$$((\phi *_0 v) *_1 (u' *_0 B)) *_2 X_{\phi, \psi'} = X_{\phi, \psi} *_2 ((u *_0 B) *_1 (\phi *_0 v')).$$

A morphism between two lax Gray categories $C$ and $D$ is a 3-prefunctor $F: C \to D$ such that $F(X_{\phi, \psi}) = X_{F(\phi), F(\psi)}$.

We similarly have a notion of pseudo Gray category which is a category enriched in the category of 2-categories equipped with the pseudo Gray tensor product. In terms of generators and relations, a pseudo Gray category is a lax Gray category $C$ where the 3-cell $X_{\phi, \psi}$ is invertible for every 0-composable 2-cells $\phi, \psi \in C_2$. A morphism between two pseudo Gray categories $C, D$ is a morphism of lax Gray categories between $C$ and $D$.

In the following, a (3,2)-Gray category is a lax Gray category whose underlying 3-precategory is a (3,2)-precategory. Note that it is then also a pseudo Gray category. As one can expect, a localization of a lax Gray category gives a (3,2)-Gray category:

**Proposition 2.2.1.** If $C$ is a lax Gray category, then $C^\top$ is canonically a (3,2)-Gray category.

*Proof.* Given 1-composable 3-cells $F: \phi \Rightarrow \phi'$ and $G: \psi \Rightarrow \psi' \in C_3$, by the exchange law for 3-cells, we have, in $C_3^\top$,

$$(F *_1 \psi) *_2 (\phi' *_1 G) = (\phi *_1 G) *_2 (F *_1 \psi').$$
By inverting $F *_1 \psi$ and $F *_1 \psi'$, we obtain

$$ (\phi' *_1 G) *_2 (F^{-1} *_1 \psi') = (F^{-1} *_1 \psi) *_2 (\phi *_1 G). $$

Similarly,

$$ (\phi *_1 G^{-1}) *_2 (F *_1 \psi) = (F *_1 \psi') *_2 (\phi' *_1 G^{-1}) $$

and

$$ (F^{-1} *_1 \psi') *_2 (\phi *_1 G^{-1}) = (\phi' *_1 G^{-1}) *_2 (F^{-1} *_1 \psi). $$

Now, given general 1-composable $F: \phi \Rightarrow \phi', G: \psi \Rightarrow \psi' \in C_3^\top$, we have that

$$ F = F_1 *_2 F_2^{-1} *_2 \cdots *_2 F_{2k-1} *_2 F_{2k}^{-1} $$

and

$$ G = G_1 *_2 G_2^{-1} *_2 \cdots *_2 G_{2l-1} *_2 G_{2l}^{-1} $$

for some $k,l \ge 1$ and $F_i, G_j \in C_3$ for $1 \le i \le 2k$ and $1 \le j \le 2l$. By applying the formulas above $4kl$ times to exchange the $F_i$'s with the $G_j$'s, we get

$$ (F *_1 \psi) *_2 (\phi' *_1 G) = (\phi *_1 G) *_2 (F *_1 \psi'). $$

A similar argument gives the compatibility between interchangers and 3-cells of $C^\top$. Thus, $C^\top$ is a (3, 2)-Gray category. $\square$

## 2.3 Gray presentations

Starting from a 3-prepolygraph $P$, such as the one of Example 2.3.1, we want to add 3-generators to $P$ and relations on the 3-cells of $P_3^*$ in order to obtain a presentation of a lax Gray category. This can of course be achieved naively by adding, for each pair of 0-composable 2-cells $\phi, \psi$ in $P_2^*$, a 3-generator corresponding to the interchanger "$X_{\phi, \psi}$", together with the relevant relations, but the resulting presentation has a large number of generators, and we detail below a more economical way of proceeding in order to present lax Gray categories.

A *Gray presentation* is a 4-prepolygraph $P$ containing the following distinguished generators:

(i) for 0-composable $\alpha, g, \beta$ with $\alpha: f \Rightarrow f', \beta: g \Rightarrow g' \in P_2, g \in P_1^*$, a 3-generator $X_{\alpha,g,\beta} \in P_3$ called *interchange generator*, which is of type

$$ X_{\alpha,g,\beta}: (\alpha *_0 g *_0 h) *_1 (f' *_0 g *_0 \beta) \Rightarrow (f *_0 g *_0 \beta) *_1 (\alpha *_0 g *_0 h') $$

which can be represented using string diagrams by

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

(ii) for every pair of 3-generators $A, B \in P_3$ and $e, e', h, h' \in P_1^*$ and $\chi \in P_2^*$ as in

<figure><img src="image_13.png" /></figure>
in $(\phi \sqcup \psi)_1$, we define the 3-cell

$$[X_{u,v}]_{\phi,\psi} : [ul_i r_j v]_{\phi,\psi}^{1,1} \Rightarrow [ur_j l_i v]_{\phi,\psi}^{1,1}$$

in $P_3^*$ by

$$[X_{u,v}]_{\phi,\psi} = [u]_{\phi,\psi}^{1,1} *_1 (f_i *_0 X_{\alpha_i, g_i *_0 f'_j, \alpha'_j} *_0 g'_j) *_1 [v]_{\phi,\psi}^{i+1, j+1}.$$

We thus obtain a functor

$$[-]_{\phi,\psi} : (\phi \sqcup \psi)^* \to \mathbf{P}^*(\partial_1^-(\phi) *_0 \partial_1^-(\psi), \partial_1^+(\phi) *_0 \partial_1^+(\psi))$$

where $(\phi \sqcup \psi)^*$ is the free 1-category on $\phi \sqcup \psi$ considered as a 1-prepolygraph, and where $[-]_{\phi,\psi}$ is defined by the mappings

$$\begin{gathered} u \in (\phi \sqcup \psi)_0 \mapsto [u]_{\phi,\psi}^{1,1} \in \mathbf{P}_2^* \\ X_{u,v} \in (\phi \sqcup \psi)_1 \mapsto [X_{u,v}]_{\phi,\psi} \in \mathbf{P}_3^* \end{gathered}$$

For example, for $\mathcal{Q}$ defined as above and $\phi = \psi = \tau *_1 \tau$, $[l_1 l_2 r_1 r_2]_{\phi,\psi}$ and $[l_1 r_1 l_2 r_2]_{\phi,\psi}$ are respectively the 2-cells of $\mathcal{Q}_2^*$

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

and

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

and $[X_{l_1,r_2}]_{\phi,\psi}$ and $[X_{l_1 r_1, \epsilon}]_{\phi,\psi}$ are respectively the 3-cells of $\mathcal{Q}_3^*$

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

and

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

We write $X_{\phi,\psi}$ for the path

$$X_{u_1,v_1} *_1 \cdots *_1 X_{u_{kk'},v_{kk'}} \in (\phi \sqcup \psi)^* (l_1 \cdots l_k r_1 \cdots r_{k'}, r_1 \cdots r_{k'} l_1 \cdots l_k)$$

defined by induction by

$$u_1 = l_1 \cdots l_{k-1}$$

and

$$v_1 = r_2 \cdots r_{k'}$$

and where $u_{i+1}, v_{i+1}$ are the unique words of $\Sigma_{\phi,\psi}^*$ such that

$$\partial_0^+(X_{u_i, v_i}) = u_{i+1} l_p r_q v_{i+1}$$

with

$$v_{i+1} = r_{q+1} \cdots r_{k'} l_{p+1} \cdots l_k$$

for some $p, q \in \mathbb{N}$. We can finally end the definition of Gray presentations by putting

$$X_{\phi,\psi} = [X_{\phi,\psi}]_{\phi,\psi}.$$

For example, for $\mathcal{Q}$ defined as above, $X_{\tau *_1 \tau, \tau *_1 \tau}$ is the composite of 3-cells of $\mathcal{Q}_3^*$ given by (8).

**Example 2.3.1.** We define the Gray presentation of pseudomonoids as the 4-prepolygraph obtained by extending the 3-prepolygraph for pseudomonoids $\mathbf{P}$ seen in Example 1.5.1. First, we add to $\mathbf{P}_3$ the 3-generators

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

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

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

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

for $n \in \mathbb{N}$. Second, we define $\mathbf{P}_4$ as a minimal set of 4-generators such that, given a configuration of cells of $(\mathbf{P}_{\le 3})^*$ as in (6), there is a corresponding independence generator in $\mathbf{P}_4$, and given a configuration of cells of $(\mathbf{P}_{\le 3})^*$ as in the first or the second line of (7), there is a corresponding interchange naturality generator in $\mathbf{P}_4$.
Our notion of Gray presentation is correct, in the sense that:

**Theorem 2.3.2.** Given a Gray presentation P, the presented precategory $\bar{P}$ is canonically a lax Gray category.

*Proof.* See Appendix B. □

**Corollary 2.3.3.** Given a Gray presentation P, $\bar{P}^\top$ is canonically a (3, 2)-Gray category.

*Proof.* By Theorem 2.3.2 and Proposition 2.2.1. □

# 3 Rewriting

In this section, we get to the heart of the matter and introduce our tools in order to show coherence results for presented Gray categories. These are obtained as generalizations of techniques developed in rewriting theory by rewriting morphisms in free precategories, and having a relation $\equiv$ on pairs of parallel rewriting 3-cells which plays the role of witness for confluence. We first define coherence and show how coherence can be obtained from a property of confluence on 3-precategories (Section 3.1). Then, we adapt the elementary notions of rewriting to the setting of 3-prepolygraphs (Section 3.2) together with classical results: a criterion for termination based on reduction orders (Section 3.3), a critical pair lemma together with a finiteness property on the number of critical branchings (Section 3.4). Our main result of this section is a coherence theorem for Gray presentations (Theorem 3.4.4), together with an associated coherence criterion (Theorem 3.4.5) that will be our main tool for the examples of the next section.

## 3.1 Coherence in Gray categories

The aim of this article is to provide tools to study the coherence of presented Gray categories, by which we mean the following. A 3-precategory *C* is coherent when, for every pair of parallel 3-cells $F_1, F_2: \phi \Rightarrow \psi \in C_3$, we have $F_1 = F_2$. By extension, a Gray presentation P is coherent when the underlying (3,2)-precategory of the (3,2)-Gray category $\bar{P}^\top$ is coherent (remember that $\bar{P}$ is a lax Gray category by Theorem 2.3.2, which implies that $\bar{P}^\top$ is a (3,2)-Gray category by Proposition 2.2.1). Gray presentations P with no other 4-generators than the independence generators and the interchange naturality generators are usually not coherent. For example, in the Gray presentation P of pseudomonoids given in Example 2.3.1, we do not expect the following parallel 3-cells

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

to be equal in $\bar{P}^\top$. For coherence, we need to add “tiles” in $P_4$ to fill the “holes” created by parallel 3-cells as the ones above. A trivial way to do this is to add a 4-generator $R: F_1 \Rightarrow F_2$ for every pair of parallel 3-cells $F_1$ and $F_2$ of $P^*$. However, this method gives quite big presentations, whereas we aim at small ones, so that the number of axioms to verify in concrete instances is as little as possible. We expose a better method in Section 3.4, in the form of Theorem 3.4.5: we will see that it is enough to add a tile of the form

<figure><img src="image_23.png" /></figure>
for every critical branching $(S_1, S_2)$ of P for which we chose 3-cells $F_1, F_2$ that make the branching $(S_1, S_2)$ joinable (definitions are introduced below).

We now show how the coherence property can be obtained starting from a 3-precategory whose 3-cells satisfy a property of confluence, motivating the adaptation of rewriting theory to 3-prepo-lygraphs in later sections in order to study the coherence of Gray presentations. In fact, we can already prove an analogous of the Church-Rosser property coming from rewriting theory in the context of confluent categories.

A 3-precategory C is confluent when, for 2-cells $\phi, \phi_1, \phi_2 \in C_2$ and 3-cells

$$F_1: \phi \Rightarrow \phi_1 \quad \text{and} \quad F_2: \phi \Rightarrow \phi_2$$

of C, there exist a 2-cell $\psi \in C_2$ and 3-cells

$$G_1: \phi_1 \Rightarrow \psi \in C_3 \quad \text{and} \quad G_2: \phi_2 \Rightarrow \psi \in C_3$$

of C such that $F_1 *_2 G_1 = F_2 *_2 G_2$:

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

The 3-cells of a (3,2)-precategory associated to a confluent 3-precategory admits a simple form, as in:

**Proposition 3.1.1.** Given a confluent 3-precategory C, every 3-cell $F: \phi \Rightarrow \phi' \in C^\top$ can be written $F = G*_2 H^{-1}$ for some $G: \phi \Rightarrow \psi \in C_3$ and $H: \phi' \Rightarrow \psi \in C_3$.

The above property says that confluent categories satisfy a “Church-Rosser property” ([2, Def. 2.1.3], for example), and is analogous to the classical result stating that confluent rewriting systems are Church-Rosser ([2, Thm. 2.1.5], for example).

*Proof.* By the definition of $C^\top$, a 3-cell $F: \phi \Rightarrow \phi' \in C^\top$ can be written

$$F = G_1^{-1} *_2 H_1 *_2 \cdots *_2 G_k^{-1} *_2 H_k$$

for some $k \ge 0$, $G_i: \chi_i \Rightarrow \phi_{i-1}$ and $H_i: \chi_i \Rightarrow \phi_i$ for $1 \le i \le k$ with $\phi_0 = \phi$ and $\phi_k = \phi'$, as in

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

We prove the property by induction on $k$. If $k = 0$, $F$ is an identity and the result follows. Otherwise, since C is confluent, there exists $\psi_k, G'_k: \phi_{k-1} \Rightarrow \psi_k$ and $H'_k: \phi_k \Rightarrow \psi_k$ with

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

By induction, the morphism

$$G_1^{-1} *_2 H_1 *_2 \cdots *_2 G_{k-2}^{-1} *_2 H_{k-2} *_2 G_{k-1}^{-1} *_2 (H_{k-1} *_2 G'_k)$$

can be written $G*_2 H^{-1}$ for some $\psi$ in $C_2$ and $G: \phi_0 \Rightarrow \psi, H: \psi_k \Rightarrow \psi$ in $C_3$. Since $G*_2 G'_k = H*_2 H'_k$, we have $G_k^{-1} *_2 H_k = G'_k *_2 H'_k^{-1}$. Hence,

$$F = G*_2 H^{-1} *_2 H_k^{-1} = G*_2 (H'_k *_2 H)^{-1}$$

which is of the wanted form. $\square$
Starting from a confluent 3-precategory, we have the following simple criterion to deduce the coherence of the associated (3, 2)-precategory:

**Proposition 3.1.2.** Let $C$ be a confluent 3-precategory which moreover satisfies that, for every $F_1, F_2$: $\phi \Rightarrow \phi' \in C_3$, we have $F_1 = F_2$ in the localization $C^\top$. Then, $C^\top$ is coherent. In particular, if $C$ is a confluent 3-precategory satisfying that, for every $F_1, F_2$: $\phi \Rightarrow \phi' \in C_3$, there is $G$: $\phi' \Rightarrow \phi'' \in C_3$ such that $F_1 *_2 G = F_2 *_2 G$ in $C_3$, then $C^\top$ is coherent.

*Proof.* Let $F_1, F_2$: $\phi \Rightarrow \phi' \in C_3^\top$. By Proposition 3.1.1, for $i \in \{1, 2\}$, we have $F_i = G_i *_2 H_i^{-1}$ for some $\psi_i \in C_2$, $G_i$: $\phi \Rightarrow \psi_i \in C_3$ and $H_i$: $\phi' \Rightarrow \psi_i \in C_3$, as in

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

By confluence, there are $\psi \in C_2$ and $K_i$: $\psi_i \Rightarrow \psi \in C_3$ for $i \in \{1, 2\}$, such that $G_1 *_2 K_1 = G_2 *_2 K_2$. By the second hypothesis, we have $H_1 *_2 K_1 = H_2 *_2 K_2$ so that

$$ 
\begin{align*}
G_1 *_2 H_1^{-1} &= G_1 *_2 K_1 *_2 (H_1 *_2 K_1)^{-1} \\
&= G_2 *_2 K_2 *_2 (H_2 *_2 K_2)^{-1} \\
&= G_2 *_2 H_2^{-1}.
\end{align*}
$$

Hence, $F_1 = F_2$. For the last part, note that if $F_1 *_2 G = F_2 *_2 G$, then $\eta(F_1) = \eta(F_2)$, where $\eta$ is the canonical 3-prefunctor $C \to C^\top$. $\square$

## 3.2 Rewriting on 3-prepolygraphs

As we have seen in the previous section, coherence can be deduced from a confluence property on the 3-cells of 3-precategories. Since confluence of classical rewriting systems is usually shown using tools coming from rewriting theory, it motivates an adaptation of it in the context of 3-prepolygraphs for the aim of studying the coherence of Gray presentations.

Given a 3-prepolygraph $P$, a *rewriting step of* $P$ is a 3-cell $S \in P_3^*$ of the form

$$ \lambda *_1 (l *_0 A *_0 r) *_1 \rho $$

for some $l, r \in P_1^*$, $\lambda, \rho \in P_2^*$ and $A \in P_3$, with $l, A, r$ 0-composable and $\lambda, l *_0 A *_0 r, \rho$ 1-composable. For such $S$, we say that $A$ is the *inner 3-generator of* $S$. A *rewriting path* is a 3-cell $F$: $\phi \Rightarrow \phi'$ in $P_3^*$. Such a rewriting path has a length $|F| \in \mathbb{N}$ which is defined as in Section 1.8. Also, by Theorem 1.8.3, it can be uniquely written as a composite of rewriting steps $S_1 *_2 \cdots *_2 S_{|F|}$, since rewriting steps are exactly 3-dimensional whiskers. Given $\phi, \psi \in P_2^*$, $\phi$ *rewrites to* $\psi$ when there exists a rewriting path $F$: $\phi \Rightarrow \psi$. A *normal form* is a 2-cell $\phi \in P_2^*$ such that for all $\psi \in P_2^*$ and $F$: $\phi \Rightarrow \psi$, we have $F = \text{id}_\phi$. $P$ is *terminating* when there does not exist an infinite sequence of rewriting steps $F_i$: $\phi_i \Rightarrow \phi_{i+1}$ for $i \ge 0$;

A *branching* is a pair rewriting paths $F_1$: $\phi \Rightarrow \phi_1$ and $F_2$: $\phi \Rightarrow \phi_2$ with the same source. The *symmetric branching* of a branching $(F_1, F_2)$ is $(F_2, F_1)$. A branching $(F_1, F_2)$ is *local* when both $F_1$ and $F_2$ are rewriting steps. A branching $(F_1, F_2)$ is *joinable* when there exist rewriting paths $G_1$: $\phi_1 \Rightarrow \psi$ and $G_2$: $\phi_2 \Rightarrow \psi$; moreover, given a congruence $\equiv$ on $P^*$, if we have that $F_1 *_2 G_1 \equiv F_2 *_2 G_2$, as in

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

we say that the branching is *confluent* (for $\equiv$).

A *rewriting system* $(P, \equiv)$ is the data of a 3-prepolygraph $P$ together with a congruence $\equiv$ on $P^*$. $(P, \equiv)$ is (*locally*) *confluent* when every (local) branching is confluent. It is *convergent* when it is
locally confluent and P is terminating. Given a 4-prepolygraph P, there is a canonical rewriting system ($P_{\le 3}, \sim P$) (recall the definition of $\sim P$ given in Section 1.6) where $\sim P$ intuitively witnesses that the “space” between two parallel 3-cells can be filled with elementary tiles that are the elements of $P_4$. In the following, most of the concrete rewriting systems we study are of this form.

The analogues of several well-known properties of abstract rewriting systems can be proved in our context. In particular, the classical proof by well-founded induction of Newman’s lemma ([2, Lem. 2.7.2], for example), can be directly adapted in order to show that:

**Theorem 3.2.1.** *A rewriting system which is convergent is confluent.*

*Proof.* Let $(P, \equiv)$ be a rewriting system which is convergent. Let $\Rightarrow^+ \subseteq P_2^* \times P_2^*$ be the partial order such that $\phi \Rightarrow^+ \psi$ if there exists a rewriting path $F: \phi \Rightarrow \psi \in P_3^*$ with $|F| > 0$. Since the underlying rewriting system is terminating, $\Rightarrow^+$ is well-founded. Thus, we can prove the theorem by induction on $\Rightarrow^+$. Suppose given a branching $F_1: \phi \Rightarrow \phi_1 \in P_3^*$ and $F_2: \phi \Rightarrow \phi_2 \in P_3^*$. If $|F_1| = 0$ or $|F_2| = 0$, then the branching is confluent. Otherwise, $F_i = S_i*_2 F'_i$ with $S_i: \phi \Rightarrow \phi'_i$ a rewriting step and $F'_i: \phi'_i \Rightarrow \phi_i$ a rewriting path for $i \in \{1, 2\}$. Since the rewriting system is locally confluent, there are $\psi \in P_2^*$ and rewriting paths $G_i: \phi'_i \Rightarrow \psi$ for $i \in \{1, 2\}$ such that $S_1*_2 G_1 \equiv S_2*_2 G_2$. Since the rewriting system is terminating and $\equiv$ is stable by composition, by composing the $G_i$'s with a path $G: \psi \Rightarrow \psi'$ where $\psi'$ is a normal form, we can suppose that $\psi$ is a normal form. By induction on $\phi'_1$ and $\phi'_2$, there are rewriting paths $H_i: \phi_i \Rightarrow \psi'_i$ and $F_i'': \psi \Rightarrow \psi'_i$ such that $F'_i*_2 H_i \equiv G_i*_2 F_i''$ for $i \in \{1, 2\}$. Since $\psi$ is in normal form, $F_i'' = \mathrm{id}_\psi$ and we have $H_i: \phi_i \Rightarrow \psi$ for $i \in \{1, 2\}$ as in

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

Moreover,

$$ \begin{align*} F_1*_2 H_1 &\equiv S_1*_2 (F'_1*_2 H_1) \\ &\equiv S_1*_2 G_1 \\ &\equiv S_2*_2 G_2 \\ &\equiv S_2*_2 (F'_2*_2 H_2) \\ &\equiv F_2*_2 H_2. \end{align*} $$

□

Theorem 3.2.1 implies that, up to post-composition, all the parallel paths of a convergent rewriting system are equivalent. Later, this will allow us to apply Proposition 3.1.2 for showing the coherence of Gray presentations.

**Lemma 3.2.2.** *Given a convergent rewriting system $(P, \equiv)$ and two rewriting paths $F_1, F_2: \phi \Rightarrow \phi' \in P_3^*$ as in*

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

there exists $G: \phi' \Rightarrow \psi \in P_3^*$ such that $F_1*_2 G \equiv F_2*_2 G$, i.e.,

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

*Proof.* Given $F_1, F_2$ as above, since the rewriting system is terminating, there is a rewriting path $G: \phi' \Rightarrow \psi$ where $\psi$ is a normal form. By confluence, there exist $G_1: \psi \Rightarrow \psi'$ and $G_2: \psi \Rightarrow \psi'$ such that $F_1*_2 G*_2 G_1 \equiv F_2*_2 G*_2 G_2$. Since $\psi$ is a normal form, we have $G_1 = G_2 = \mathrm{id}_\psi$. Hence, $F_1*_2 G \equiv F_2*_2 G$. □
Note that, in Lemma 3.2.2, we do not necessarily have

$$F_1(\phi) F_2(\equiv) F_2(\phi')$$

which explains why the method we develop in this section for showing coherence will only apply to (3, 2)-precategories, but not to general 3-precategories.

## 3.3 Termination

Here, we show a termination criterion for rewriting systems $(P, \equiv)$ based on a generalization of the notion of reduction order in classical rewriting theory where we require a compatibility between the order and the composition operations of cells.

A reduction order for a 3-prepolygraph $P$ is a well-founded partial order < on $P_2^*$ such that:

- given $A: \phi \Rightarrow \phi' \in P_3$, we have $\phi > \phi'$,

- given $l, r \in P_1^*$ and parallel $\phi, \phi' \in P_2^*$ such that $l, \phi, r$ are 0-composable and $\phi > \phi'$, we have
$$l *_0 \phi *_0 r > l *_0 \phi' *_0 r,$$

- given 1-composable $\lambda, \phi, \rho \in P_2^*$, and $\phi' \in P_2^*$ parallel to $\phi$ such that $\phi > \phi'$, we have

$$\lambda *_1 \phi *_1 \rho > \lambda *_1 \phi' *_1 \rho.$$

The termination criterion is then:

**Proposition 3.3.1.** If $(P, \equiv)$ is a rewriting system such that there exists a reduction order for $P$, then $(P, \equiv)$ is terminating.

*Proof.* The definition of a reduction order implies that, given a rewriting step $\lambda *_1 (l *_0 A *_0 r) *_1 \rho$ with $l, r \in P_1^*$, $\lambda, \rho \in P_2^*$ and $A: \phi \Rightarrow \phi' \in P_3$ suitably composable, we have

$$\lambda *_1 (l *_0 \phi *_0 r) *_1 \rho > \lambda *_1 (l *_0 \phi' *_0 r) *_1 \rho.$$

So, given a sequence of 2-composable rewriting steps $(F_i)_{i<k}$, where $k \in \mathbb{N} \cup \{\infty\}$, $F_i: \phi_i \Rightarrow \phi_{i+1} \in P_3$ for $i < k$, we have $\phi_i > \phi_{i+1}$ for $i < k$. Since $>$ is well-founded, it implies that $k \in \mathbb{N}$ Hence, the rewriting sytem $(P, \equiv)$ is terminating. $\square$

In order to build a reduction order for a Gray presentation $P$, we have to build in particular a reduction order for the subset of $P_3$ made of interchange generators. We introduce below a sufficient criterion for the existence of such a reduction order. The idea is to consider the lengths of the 1-cells of the whiskers in the decompositions of 2-cells and show that they are decreasing in some way when an interchange generator is applied.

Let $\mathbb{N}^<^\omega$ be the set of finite sequences of elements of $\mathbb{N}$. We order $\mathbb{N}^<^\omega$ by $<_\omega$ where

$$(a_1, \dots, a_k) <_\omega (b_1, \dots, b_l)$$

when $k = l$ and there exists $i \in \mathbb{N}$ with $1 \le i \le k$ such that $a_j = b_j$ for some $j < i$ and $a_i < b_i$. Note that $<_\omega$ is well-founded. Given a 2-prepolygraph $P$, there is a function $N_{\text{int}}: P_2^* \to \mathbb{N}^<^\omega$ such that, given $\phi \in P_2^*$, decomposed uniquely (using Theorem 1.8.3) as

$$\phi = (l_1 *_0 \alpha_1 *_0 r_1) *_1 \cdots *_1 (l_k *_0 \alpha_k *_0 r_k)$$

for some $k \in \mathbb{N}$, $l_i, r_i \in P_1^*$ and $\alpha_i \in P_2$ for $i \in \{1, \dots, k\}$, $N_{\text{int}}(\phi)$ is defined by

$$N_{\text{int}}(\phi) = (|l_k|, |l_{k-1}|, \dots, |l_1|).$$

Then, $N_{\text{int}}$ induces a partial order $<_{\text{int}}$ on $P_2^*$ by putting $\phi <_{\text{int}} \psi$ when $\partial_1^\epsilon(\phi) = \partial_1^\epsilon(\psi)$ for $\epsilon \in \{-, +\}$ and $N_{\text{int}}(\phi) <_\omega N_{\text{int}}(\psi)$ for $\phi, \psi \in P_2^*$.

Given a Gray presentation $P$, we say that $P$ is *positive* when $|\partial_1^+(\alpha)| > 0$ for all $\alpha \in P_2$. Under positiveness, the order $<_{\text{int}}$ can be considered as a reduction order for the subset of 3-generators of a Gray presentation made of interchangers, as in
**Proposition 3.3.2.** Let P be a positive Gray presentation. The partial order $<_{\text{int}}$ has the following properties:

(i) for every $\alpha, \beta \in P_2$ and $f \in P_1^*$ such that $\alpha, f, \beta$ are 0-composable,

$$ \partial_2^-(X_{\alpha,f,\beta}) >_{\text{int}} \partial_2^+(X_{\alpha,f,\beta}), $$

(ii) for $\phi, \phi' \in P_2^*$ and $l, r \in P_1^*$ such that $l, \phi, r$ are 0-composable, if $\phi >_{\text{int}} \phi'$, then

$$ l *_0 \phi *_0 r >_{\text{int}} l *_0 \phi' *_0 r, $$

(iii) for $\phi, \phi', \lambda, \rho \in P_2^*$ such that $\lambda, \phi, \rho$ are 1-composable, if $\phi >_{\text{int}} \phi'$, then

$$ \lambda *_1 \phi *_1 \rho >_{\text{int}} \lambda *_1 \phi' *_1 \rho. $$

*Proof.* Given $\alpha, \beta \in P_2$ and $f \in P_1^*$ with $\alpha, f, \beta$ are 0-composable, recall that $X_{\alpha,f,\beta}$ is such that

$$ X_{\alpha,f,\beta}: (\alpha*_0 f*_0 \partial_1^-(\beta))*_1 (\partial_1^+(\alpha)*_0 f*_0 \beta) \Rightarrow (\partial_1^-(\alpha)*_0 f*_0 \beta)*_1 (\alpha*_0 f*_0 \partial_1^+(\beta)) $$

Then, we have

$$ N_{\text{int}}(\partial_2^-(X_{\alpha,f,\beta})) = (|\partial_1^+(\alpha)| + |f|, 0) \quad \text{and} \quad N_{\text{int}}(\partial_2^+(X_{\alpha,f,\beta})) = (0, |\partial_1^-(\alpha)| + |f|). $$

Since P is positive, we have $|\partial_1^+(\alpha)| > 0$ so that $N_{\text{int}}(\partial_2^-(X_{\alpha,f,\beta})) >_{\text{int}} N_{\text{int}}(\partial_2^+(X_{\alpha,f,\beta})).$ Now, (ii) and (iii) can readily be obtained by considering the whisker representations of $\phi$ and $\phi'$ and observing the action of $l*_0 -*_0 r$ and $\lambda*_1 -*_1 \rho$ on these representations and the definition of $N_{\text{int}}$. $\square$

The positiveness condition is required to prevent 2-cells with “floating components”, since Gray presentations with such 2-cells might not terminate. For example, given a Gray presentation P where $P_0$ and $P_1$ have one element and $P_2$ has two 2-generators $\circled{\circled{\circ}}$ and $\circled{\circ}$, there are 2-cells of $P^*$ with “floating bubbles” which induce infinite reduction sequence with interchange generators as the following one:

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

## 3.4 Critical branchings

In term rewriting systems, a classical result called the “critical pair lemma” states that local confluence is a consequence of the confluence of a subset of local branchings, called *critical branchings*. The latter can be described as pairs of rewrite rules that are minimally overlapping, see [2, Sec. 6.2] for details. Note that we used this result earlier in the proof of Lemma 1.8.2.

Here, we show a similar result for rewriting on Gray presentations (introduced in Section 2.3). For this purpose, we give a definition of critical branchings which is similar to term rewriting systems, i.e., as minimally overlapping local branchings, where we moreover filter out some branchings that involve interchange generators and that are automatically confluent by our definition of Gray presentation. Then, we give a coherence theorem for Gray presentation based on the analysis critical branchings together with an associated coherence criterion, and we finish the section by stating a finiteness property on the critical branchings.

Let P be a 3-prepolygraph. Given a local branching $(S_1: \phi \Rightarrow \phi_1, S_2: \phi \Rightarrow \phi_2)$ of P, we say that the branching $(S_1, S_2)$ is

- trivial when $S_1 = S_2$,

- minimal when for all other local branching $(S'_1, S'_2)$ such that

$$ S_i = \lambda *_1 (l*_0 S'_i *_0 r) *_1 \rho $$

for $i \in \{1, 2\}$ for some 1-cells $l, r$ and 2-cells $\lambda, \rho$, we have that $l, r, \lambda, \rho$ are all identities,
- *independent* when

$$S_1 = ((l_1 *_0 A_1 *_0 r_1) *_1 \chi *_1 (l_2 *_0 \phi_2 *_0 r_2))$$

and

$$S_2 = ((l_1 *_0 \phi_1 *_0 r_1) *_1 \chi *_1 (l_2 *_0 A_2 *_0 r_2))$$

for some $l_i, r_i \in P_1^*$ and $A_i: \phi_i \Rightarrow \phi'_i \in P_3$ for $i \in \{1, 2\}$ and $\chi \in P_2^*$.

If moreover $P = Q_{\le 3}$, where $Q$ is a Gray presentation, we say that the the branching $(S_1, S_2)$ is

- *natural* when

$$S_1 = ((A *_0 g *_0 h) *_1 (f' *_0 g *_0 \psi))$$

for some $A: \phi \Rightarrow \phi'$: $f \Rightarrow f' \in P_3$, $\psi: h \Rightarrow h' \in P_2^*$ and $g \in P_1^*$, and

$$S_2 = [X_{u,v}]_{\phi,g*_0\psi} \quad \text{with} \quad u = l_1 \dots l_{|\phi|-1} \quad \text{and} \quad v = r_2 \dots r_{|\psi|}$$

and similarly for the situation on the second line of (7),

- *critical* when it is minimal, and both its symmetrical branching and it are neither trivial nor independent nor natural.

In the following, we suppose given a Gray presentation $Q$ and we write $(P, \equiv)$ for $(Q_{\le 3}, \sim^Q)$. Our next goal is to show an adapted version of the critical pair lemma. We start by two technical lemmas:

**Lemma 3.4.1.** For every local branching $(S_1, S_2)$ of $P$, there is a minimal branching $(S'_1, S'_2)$ and 1-cells $l, r \in P_1^*$ and 2-cells $\lambda, \rho \in P_2^*$ such that $S_i = \lambda *_1 (l*_0 S'_i *_0 r) *_1 \rho$ for $i \in \{1, 2\}$.

*Proof.* We show this by induction on $N(S_1)$ where $N(S_1) = |\partial_2^-(S_1)| + |\partial_1^-(S_1)|$. Suppose that the property is true for all local branchings $(S'_1, S'_2)$ with $N(S'_1) < N(S_1)$. If $(S_1, S_2)$ is not minimal, then there are rewriting steps $S'_1, S'_2 \in P_3$, $l, r \in P_1^*$ and $\lambda, \rho \in P_2^*$ such that $S_i = \lambda*_1 (l*_0 S'_i *_0 r) *_1 \rho$ for $i \in \{1, 2\}$, such that $l, r, \lambda, \rho$ are not all identities. Since

$$|\partial_1^-(S_1)| = |l| + |\partial_1^-(S'_1)| + |r| \quad \text{and} \quad |\partial_2^-(S_1)| = |\lambda| + |\partial_2^-(S'_1)| + |\rho|,$$

we have $N(S'_1) < N(S_1)$ so there is a minimal branching $(S''_1, S''_2)$ and $l', r' \in P_1^*, \lambda', \rho' \in P_2^*$ such that $S'_i = \lambda'_1 *_1 (l'*_0 S''_i *'_0 r') *'_1 \rho'$ for $i \in \{1, 2\}$. By composing with $\lambda, \rho, l, r$ and normalizing as in Theorem 1.8.3, we obtain the conclusion of the lemma. $\square$

**Lemma 3.4.2.** A local branching of $P$ which is either trivial or independent or natural is confluent.

*Proof.* A trivial branching is, of course, confluent. Independent and natural branching are confluent thanks respectively to the independence generators and interchange naturality generators of a Gray presentation. $\square$

The critical pair lemma adapted to our context is then:

**Theorem 3.4.3 (Adapted critical pair lemma).** The rewriting system $(P, \equiv)$ is locally confluent if and only if every critical branching is confluent.

*Proof.* If the rewriting system is locally confluent, then, in particular, every critical branching is confluent. For the converse implication, by Lemma 3.4.1, to check that all local branchings are confluent, it is enough to check that all minimal local branchings are confluent. Among them, by Lemma 3.4.2, it is enough to check the confluence of the critical branchings. $\square$

We now state the main result of this section, namely a coherence theorem for Gray presentations based on the analysis of the critical branchings:

**Theorem 3.4.4 (Coherence).** Let $Q$ be a Gray presentation and $(P, \equiv) = (Q_{\le 3}, \sim^Q)$ be the associated rewriting system. If $P$ is terminating and all the critical branchings of $(P, \equiv)$ are confluent, then $Q$ is a coherent Gray presentation.
*Proof.* By Theorem 3.4.3, the rewriting system $(\mathbb{P}, \equiv)$ is locally confluent, and by Theorem 3.2.1 it is confluent. Since $\overline{\mathbb{Q}} = \mathbb{P}^*/\equiv$, it implies that $\overline{\mathbb{Q}}$ is a confluent 3-precategory. To conclude, it is sufficient to show that the criterion in the last part of Proposition 3.1.2 is satisfied. But the latter is a consequence of Lemma 3.2.2. $\square$

Note that Theorem 3.4.4 requires the rewriting system $(\mathbb{P}, \equiv)$ to be confluent. If it is not the case, one can try to first apply a modified version of the classical Knuth-Bendix completion procedure [18] (see also [2, Sec. 7]) which, in addition to adding new 3-generators in order to make the system confluent, also adds 4-generators in order to make it confluent up to $\equiv$, in order to hopefully obtain a confluent Gray presentation. Such a procedure is detailed in the closely related setting of coherent presentations of monoids in [16], where it is called the Knuth-Bendix-Squier completion procedure.

Our coherence theorem implies a coherence criterion similar to the ones shown by Squier, Otto and Kobayashi [27, Thm. 5.2] and Guiraud and Malbos [13, Prop. 4.3.4], which states that adding a tile for each critical branching is enough to ensure coherence:

**Theorem 3.4.5.** Let $\mathbb{Q}$ be a Gray presentation, such that $\mathbb{Q}_{\le 3}$ is terminating and, for every critical branching $(S_1: \phi \Rightarrow \phi_1, S_2: \phi \Rightarrow \phi_2)$ of $\mathbb{Q}_{\le 3}$, there exist $\psi \in \mathbb{Q}_2^*$, $F_i: \phi_i \Rightarrow \psi \in \mathbb{Q}_3^*$ for $i \in \{1, 2\}$ and $G: S_1 *_2 F_1 \Rightarrow^* S_2 *_2 F_2 \in \mathbb{Q}_4$. Then, $\mathbb{Q}$ is a coherent Gray presentation.

*Proof.* The definition of $\mathbb{Q}_4$ ensures that all the critical branchings are confluent, so that Theorem 3.4.4 applies. $\square$

Note that, in Theorem 3.4.5, we do not need to add a 4-generator $G$ as in the statement for a critical branching $(S_1, S_2)$ if there is already a generator $G'$ for the symmetrical branching $(S_2, S_1)$, so that a stronger statement holds.

To finish this section, we mention a finiteness property for critical branchings of Gray presentations. This property contrasts with the case of strict $n$-categories, where finite presentations can have an infinite number of critical branchings [21, 13].

**Theorem 3.4.6.** Given a Gray presentation $\mathbb{Q}$ where $\mathbb{Q}_2$ and $\mathbb{Q}_3$ are finite and $|\partial_2^-(A)| > 0$ for every $A \in \mathbb{Q}_3$, there is a finite number of local branchings $(S_1, S_2)$ with rewriting steps $S_1, S_2 \in \mathbb{Q}_3^*$ such that $(S_1, S_2)$ is a critical branching.

*Proof.* See Appendix C. $\square$

The proof of Theorem 3.4.6 happens to be constructive, so that we can extract an algorithm to compute the critical branchings for such Gray presentations. An implementation of this algorithm was used to compute the critical branchings of the examples of the next section.

# 4 Applications

We now illustrate the techniques of the previous section and show the coherence of Gray presentations corresponding to several well-known algebraic structures. For each structure, we introduce a Gray presentation and study the confluence of the critical branchings of the associated rewriting system. Then, when the rewriting system is terminating, we can directly apply Theorem 3.4.5 to deduce the coherence of the presentation. This will be the case for pseudomonoids, pseudoadjunctions and Frobenius pseudomonoids. We moreover study the example of self-dualities, where the associated rewriting system is not terminating, for which we use specific techniques in order to prove a weak coherence result.

## 4.1 Pseudomonoids

In Example 2.3.1, we introduced a Gray presentation $\mathbb{P}$ for the theory of pseudomonoids. The set $\mathbb{P}_4$ of 4-generators contains only the required ones in a Gray presentation, so that we do not expect $\mathbb{P}$ to be coherent (see (9) for an example). We will show that the rewriting system is terminating and thus, Theorem 3.4.5, adding a 4-generator corresponding to each critical branching will turn the presentation into a coherent one. Those branchings can be computed as in the proof
of Theorem 3.4.6, which is constructive: we obtain, up to symmetrical branchings, five critical branchings:

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

We observe that each of these branchings is joinable, and we define formal new 4-generators $R_1, R_2, R_3, R_4, R_5$ that fill the holes:

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

We then define $\mathbf{PMon}$ as the Gray presentation obtained from $\mathbf{P}$ of Example 2.3.1 by adding $R_1, \dots, R_5$ to $\mathbf{P}_4$.

As claimed above, in order to deduce coherence, we need to show the termination of $\mathbf{PMon}$. For this purpose, we use the tools of Section 3 and build a reduction order. We split the task in two and define a first order that handles the termination of the $A, L, R$ generators, and then a second one that handles the termination of interchange generators. For the first task, we use a technique similar to the one used in [19]. Given $n \in \mathbb{N}$, we write $\langle \cdot \rangle_{\text{ex}}$ for the partial order on $\mathbb{N}^n$ such that, given $a, b \in \mathbb{N}^n$, $a \le \langle \cdot \rangle_{\text{ex}} b$ when $a_i \le b_i$ for all $i \in \{1, \dots, n\}$ and there exists $j \in \{1, \dots, n\}$ such that $a_j < b_j$. Let $\mathbf{MFun}$ be the 2-precategory

- which has only one 0-cell: $\mathbf{MFun}_0 = \{\ast\}$,

- whose 1-cells are the natural numbers: $\mathbf{MFun}_1 = \mathbb{N}$,

- whose 2-cells $m \Rightarrow n$ for $m, n \in \mathbb{N}$ are the strictly monotone functions

$$ \phi: (\mathbb{N}^m, \langle \cdot \rangle_{\text{ex}}) \to (\mathbb{N}^n, \langle \cdot \rangle_{\text{ex}}). $$
Moreover, $\mathrm{id}_* = 0$ and composition of 1-cells is given by addition. Given $m \in \mathrm{MFun}_1$, $\mathrm{id}_m$ is the identity function on $\mathbb{N}^m$, and given $m, n, k, k' \in \mathbb{N}$ and $\chi: k \to k' \in \mathrm{MFun}_2$, the 2-cell

$$m *_0 \chi *_0 n: m + k + n \Rightarrow m + k' + n$$

is the function $\chi': \mathbb{N}^{m+k+n} \to \mathbb{N}^{m+k'+n}$ such that, for $x = (x_1, \dots, x_{m+k+n}) \in \mathbb{N}^{m+k+n}$, for $i \in \{1, \dots, m+k'+n\}$,

$$\chi'(x)_i = \begin{cases} x_i & \text{if } i \le m \\ \chi(x_{m+1}, \dots, x_{m+k})_{i-m} & \text{if } m < i \le m+k' \\ x_{i-k'+k} & \text{if } i > m+k' \end{cases}$$

and, given $m, n, p \in \mathbb{N}$, $\phi: m \Rightarrow n \in \mathrm{MFun}_2$ and $\psi: n \Rightarrow p \in \mathrm{MFun}_2$, $\phi*_1 \psi$ is defined as $\psi \circ \phi$ and one shows readily that these operations indeed give strictly monotone functions. One easily checks that MFun is a strict 2-category. Given $m, m', n, n' \in \mathbb{N}$ and $\phi: m \Rightarrow n, \psi: m' \Rightarrow n' \in \mathrm{MFun}$, we write $\phi <^2_{\mathrm{ex}} \psi$ when $m = m', n = n'$ and $\phi(x) <^1_{\mathrm{ex}} \psi(x)$ for all $x \in \mathbb{N}^m$. We have that:

**Proposition 4.1.1.** $<^2_{\mathrm{ex}}$ is well-founded on $\mathrm{MFun}_2$.

*Proof.* We define a function $N: \mathrm{MFun}_2 \to \mathbb{N}$ by

$$N(\phi) = \phi(z)_1 + \dots + \phi(z)_n \quad \text{for } \phi: m \Rightarrow n \in \mathrm{MFun}_2$$

where $z = (0, \dots, 0)$. Now, if $\psi: m \Rightarrow n \in \mathrm{MFun}_2$ is such that $\psi <^2_{\mathrm{ex}} \phi$, then $\psi(z) <^1_{\mathrm{ex}} \phi(z)$ so that $N(\psi) < N(\phi)$. Thus, $<^2_{\mathrm{ex}}$ on $\mathrm{MFun}_2$ is well-founded. $\square$

We observe that the order $<^2_{\mathrm{ex}}$ is compatible with the structure of MFun:

**Proposition 4.1.2.** Given $m, n, m', n', k, k' \in \mathbb{N}$, $\mu: m' \Rightarrow m$, $\nu: n \Rightarrow n'$, and $\phi, \phi': k \Rightarrow k' \in \mathrm{MFun}_2$ such that $\phi >^2_{\mathrm{ex}} \phi'$, we have

$$(i) m *_0 \phi *_0 n >^2_{\mathrm{ex}} m *_0 \phi' *_0 n,$$

$$(ii) \mu *_1 \phi *_1 \nu >^2_{\mathrm{ex}} \mu *_1 \phi' *_1 \nu.$$

*Proof.* Given $x \in \mathbb{N}^{m+k+n}$, we have $\phi(x_{m+1}, \dots, x_{m+k}) >^1_{\mathrm{ex}} \phi'(x_{m+1}, \dots, x_{m+k})$ so

$$(m *_0 \phi *_0 n)(x) >^1_{\mathrm{ex}} (m *_0 \phi' *_0 n)(x).$$

Thus, (i) holds. Moreover, given $y \in \mathbb{N}^{m'}$, we have $\phi(\mu(y)) >^1_{\mathrm{ex}} \phi'(\mu(y))$. Since $\nu$ is monotone, we have $\nu(\phi(\mu(y))) >^1_{\mathrm{ex}} \nu(\phi'(\mu(y)))$. Thus, (ii) holds. $\square$

We define a 2-prefunctor $F: \mathrm{PMon}_2^* \to \mathrm{MFun}$ by the universal property of the 2-prepolygraph $\mathrm{PMon}_{\le 2}$, i.e., $F$ is the unique functor such that $F(*) = *, F(\bar{1}) = 1$, $F(\mu) = f_\mu$ and $F(\eta) = f_\eta$ where

$$f_\mu: \mathbb{N}^2 \to \mathbb{N}^1 \qquad f_\eta: \mathbb{N}^0 \to \mathbb{N}^1$$

are defined by $f_\mu(x, y) = 2x + y + 1$ for all $x, y \in \mathbb{N}$ and $f_\eta(1) = 1$. The interpretation exhibits the 3-generators A, L and R of $\mathrm{PMon}$ as decreasing operations:

**Proposition 4.1.3.** The following hold:

$$(i) F(\partial_2^-(A)) >^2_{\mathrm{ex}} F(\partial_2^+(A)),$$

$$(ii) F(\partial_2^-(L)) >^2_{\mathrm{ex}} F(\partial_2^+(L)),$$

$$(iii) F(\partial_2^-(R)) >^2_{\mathrm{ex}} F(\partial_2^+(R)),$$

$$(iv) F(\partial_2^+(X_{\alpha,m,\beta})) = F(\partial_2^-(X_{\alpha,m,\beta})) \text{ for } \alpha, \beta \in \mathrm{PMon}_2 \text{ and } m \in \mathbb{N}.$$

*Proof.* Let $\phi = F(\partial_2^-(A))$ and $\psi = F(\partial_2^+(A))$. By calculations, we get that

$$\phi(x, y, z) = (4x + 2y + z + 3) \quad \text{and} \quad \psi(x, y, z) = (2x + 2y + z + 1)$$

for $x, y, z \in \mathbb{N}$, so $\phi(x, y, z) >^1_{\mathrm{ex}} \psi(x, y, z)$ for all $x, y, z \in \mathbb{N}$. The cases (ii) and (iii) are shown similarly. (iv) is a consequence of the fact that MFun is a strict 2-category. $\square$
We define a partial order < on $\mathbf{PMon}_2^*$ by putting, for $\phi, \psi \in \mathbf{PMon}_2^*$,

$$ \phi < \psi \text{ when } F(\phi) <_{\text{ex}}^2 F(\psi) \text{ or } [F(\phi) = F(\psi) \text{ and } N_{\text{int}}(\phi) <_{\omega} N_{\text{int}}(\psi)]. $$

**Proposition 4.1.4.** *The partial order < on $\mathbf{PMon}_2^*$ is a reduction order for $\mathbf{PMon}$.*

*Proof.* Let $G \in \mathbf{PMon}_3$. If $G \in \{\mathbf{A}, \mathbf{L}, \mathbf{R}\}$, then, by Proposition 4.1.3, $\partial_2^+(G) < \partial_2^-(G)$. Otherwise, if $G = X_{\alpha, u, \beta}$ for some $\alpha, \beta \in \mathbf{PMon}_2$ and $u \in \mathbf{PMon}_1^*$, then, by Proposition 4.1.3(iv),

$$ F(\partial_2^+(G)) = F(\partial_2^-(G)) \quad \text{and} \quad N_{\text{int}}(\partial_2^+(G)) <_{\omega} N_{\text{int}}(\partial_2^-(G)). $$

So $\partial_2^+(G) < \partial_2^-(G)$. The other requirements for < to be a reduction order are consequences of Proposition 4.1.2 and Proposition 3.3.2(ii)(iii). $\square$

Finally, we can use our coherence criterion to show that:

**Theorem 4.1.5.** *$\mathbf{PMon}$ is a coherent Gray presentation.*

*Proof.* By Proposition 4.1.4, $\mathbf{PMon}$ has a reduction order, so the rewriting system $\mathbf{PMon}$ is terminating by Proposition 3.3.1. Since $R_1, \dots, R_5 \in \mathbf{PMon}_4$, by Theorem 3.4.5, $\overline{\mathbf{PMon}}^\top$ is a coherent (3, 2)-Gray category. $\square$

## 4.2 Pseudoadjunctions

We now show the coherence of the Gray presentation of pseudoadjunctions introduced below. The way we do this is again by using Theorem 3.4.5. However, we need a specific argument to show the termination of the interchange generators on the associated rewriting system. For this, we introduce a notion of “connected” diagrams and we use a result of [9] stating that interchange generators terminate on such connected diagrams.

We define the 3-prepolygraph for pseudoadjunctions as the 3-prepolygraph P such that

$$ P_0 = \{x, y\} \quad \text{and} \quad P_1 = \{f: x \to y, g: y \to x\} \quad \text{and} \quad P_2 = \{\eta: \mathrm{id}_x \Rightarrow f *_0 g, \varepsilon: g *_0 f \Rightarrow \mathrm{id}_y\} $$

where $\eta$ and $\varepsilon$ are pictured as $\frown$ and $\frown$ respectively, and $P_3$ is defined by $P_3 = \{\mathbf{N}, \mathbf{U}\}$, where

$$ \mathbf{N}: (\eta *_0 f) *_1 (f *_0 \varepsilon) \Rightarrow \mathrm{id}_f \quad \text{and} \quad \mathbf{U}: (g *_0 \eta) *_1 (\varepsilon *_0 b) \Rightarrow \mathrm{id}_g $$

which can be represented by

$$ \frown \quad \mathbf{N} \quad \frown \quad \text{and} \quad \frown \quad \mathbf{U} \quad \frown $$

We then extend P to a Gray presentation by adding 3-generators corresponding to interchange generators and 4-generators corresponding to independence generator and interchange naturality generator, just like we did for pseudomonoids in Example 2.3.1. For coherence, we need to add other 4-generators to $P_4$. Provided that P is terminating, by Theorem 3.4.5, adding 4-generators that fill the holes created by critical branchings is enough, just like for pseudomonoids.

Using the constructive proof of Theorem 3.4.6, we compute all the critical branchings of P. We then obtain, up to symmetrical branchings, two critical branchings:

<figure><img src="image_35.png" /></figure>
We observe that each of these branchings is joinable, and we define formal new 4-generators $R_1, R_2$ that fill the holes:

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

We then define $\mathcal{P}\mathrm{Adj}$ as the Gray presentation obtained from $\mathcal{P}$ by adding $R_1$ and $R_2$ to $\mathcal{P}_4$.

We aim at showing that this rewriting system is terminating by exhibiting a reduction order. However, we cannot use Proposition 3.3.2 to handle interchangers (as for the case of pseudomonoids) since $\mathcal{P}$ is not positive. Instead, we invoke the result of [9] which states the termination of interchangers on “connected diagrams”. Given a 2-prepolygraph $\mathcal{Q}$, a 2-cell of $\mathcal{Q}_2^*$ is connected when, intuitively, each 2-generator on its graphical representation is accessible by a path starting from a top or bottom input. For example, given $\mathcal{Q}$ such that $\mathcal{Q}_0 = \{*\}$, $\mathcal{Q}_1 = \{\bar{1}\}$ and $\mathcal{Q}_2 = \{\frown: \bar{0} \Rightarrow \bar{2}, \frown: \bar{2} \Rightarrow \bar{0}\}$, we can build the following two 2-cells of $\mathcal{Q}_2^*$:

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

where the one on the left is connected whereas the one on the right is not, since the two generators of the “bubble” cannot be accessed from the top or bottom border.

A more formal definition can be obtained by computing the “connected components” of the diagram, together with a map between the top and bottom inputs of the diagram to the associated connected components. This is adequately represented by cospans of **Set**. Based on this idea, we define a 2-precategory that allows us to compute the connected components of a 2-cell of $\mathcal{Q}^*$. Let $\mathbb{N}_m$ be the set $\{1, \dots, m\}$ for $m \ge 0$.

We define the 2-precategory **CoSpan** as the 2-precategory such that:

- it has a unique 0-cell, denoted $*$,

- the 1-cells are the natural numbers, with 0 as unit and addition as composition,

- the 2-cells $m \Rightarrow n$ are the classes of equivalent cospans $\mathbb{N}_m \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_n$ in **Set**,

where two cospans $A \xrightarrow{f} S \xleftarrow{g} B$ and $A \xrightarrow{f'} S' \xleftarrow{g'} B$ are said equivalent when there exists an isomorphism $h: S \to S' \in \mathbf{Set}$ such that $f' = h \circ f$ and $g' = h \circ g$. The unit of $m \in \mathbf{CoSpan}_1$ is the cospan $\mathbb{N}_m \xrightarrow{1_{\mathbb{N}_m}} \mathbb{N}_m \xleftarrow{1_{\mathbb{N}_m}} \mathbb{N}_m$, and, given $\phi: m_1 \Rightarrow m_2 \in \mathbf{CoSpan}_2$ and $\psi: m_2 \Rightarrow m_3 \in \mathbf{CoSpan}_2$, represented by the cospans

$$ \mathbb{N}_{m_1} \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_{m_2} \quad \text{and} \quad \mathbb{N}_{m_2} \xrightarrow{f'} S' \xleftarrow{g'} \mathbb{N}_{m_3} $$

respectively, their composite is represented by the cospan

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

where the middle square is a pushout. Given $\phi: m \Rightarrow n \in \mathbf{CoSpan}_2$ represented by

$$ \mathbb{N}_m \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_n $$
and $p, q \in \text{CoSpan}_1$, the 2-cell $p *_0 \phi *_0 q$ is represented by the cospan

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

where $\theta_{p,r,q}: \mathbb{N}_{p+r+q} \to \mathbb{N}_p \sqcup \mathbb{N}_r \sqcup \mathbb{N}_q$, for $r \in \mathbb{N}$, is the obvious bijection. One easily verifies that **CoSpan** is in fact a 2-category (fact that will be useful when dealing with interchange generators later).

Given a 2-prepolygraph $\mathcal{Q}$, by the universal property of 2-prepolygraphs, we define a 2-prefunctor $\text{Con}_{\mathcal{Q}}: \mathcal{Q}^* \to \text{CoSpan}$ such that

- the image of $x \in \mathcal{Q}_0$ is $*$,

- the image of $a \in \mathcal{Q}_1$ is 1,

- the image of $\alpha: f \Rightarrow g \in \mathcal{Q}_2$ is represented by the unique cospan $\mathbb{N}_{|f|} \xrightarrow{*} \{*\} \leftarrow \mathbb{N}_{|g|}$

We can now give our definition for connectedness: a 2-cell $\phi \in \mathcal{Q}_2^*$ is connected when $\text{Con}_{\mathcal{Q}}(\phi)$ is represented by a cospan $\mathbb{N}_m \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_n$, with $m = |\partial_1^-(\phi)|$ and $n = |\partial_1^+(\phi)|$, such that $f, g$ are jointly epimorphic. Since the latter property is invariant by equivalences of cospan, if $\phi$ is connected, then for every representative $\mathbb{N}_m \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_n$ of $\text{Con}_{\mathcal{Q}}(\phi)$, $f, g$ are jointly epimorphic.

In the case of $\text{PAdj}$, as one can expect, the 3-generators $\mathbb{N}$ and $\mathbb{U}$ do not change connectivity:

**Lemma 4.2.1.** We have

$$ \text{Con}_{\text{PAdj}}((\eta *_0 f) *_1 (f *_0 \varepsilon)) = \text{Con}_{\text{PAdj}}(\text{id}_f) $$

and

$$ \text{Con}_{\text{PAdj}}((g *_0 \eta) *_1 (\varepsilon *_0 g)) = \text{Con}_{\text{PAdj}}(\text{id}_g). $$

*Proof.* By calculations, we verify that

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

is a representative of both $\text{Con}_{\text{PAdj}}((\eta *_0 f) *_1 (f *_0 \varepsilon))$ and $\text{Con}_{\text{PAdj}}(\text{id}_f)$, so that

$$ \text{Con}_{\text{PAdj}}((\eta *_0 f) *_1 (f *_0 \varepsilon)) = \text{Con}_{\text{PAdj}}(\text{id}_f) $$

and similarly,

$$ \text{Con}_{\text{PAdj}}((g *_0 \eta) *_1 (\varepsilon *_0 g)) = \text{Con}_{\text{PAdj}}(\text{id}_g). \quad \square $$

Moreover, connectivity is preserved by interchangers in general:

**Lemma 4.2.2.** Let $\mathcal{P}$ be a 2-prepolygraph. Let $\alpha, \beta \in \mathcal{P}_2$ and $g \in \mathcal{P}_1^*$ such that $\alpha, g, \beta$ are 0-composable. Then,

$$ \text{Con}_{\mathcal{P}}((\alpha *_0 g *_0 \partial_1^-(\beta)) *_1 (\partial_1^+(\alpha) *_0 g *_0 \beta)) = \text{Con}_{\mathcal{P}}((\partial_1^-(\alpha) *_0 g *_0 \beta) *_1 (\alpha *_0 g *_0 \partial_1^+(\beta))) $$

*Proof.* This is a direct consequence of the fact that **CoSpan** is a strict 2-category. $\square$

We now prove a technical lemma that we will use to show the connectivity of the 2-cells in $\text{PAdj}_2^*$:

**Lemma 4.2.3.** Let $\mathcal{P}$ be a 2-prepolygraph and $\phi, \phi' \in \mathcal{P}_2^*$ and $\mathbb{N}_{n_1} \xrightarrow{f} S \xleftarrow{g} \mathbb{N}_{n_2}$ be a representative of $\text{Con}_{\mathcal{P}}(\phi)$ for some $n_1, n_2 \in \mathbb{N}$ such that $\phi, \phi'$ are 1-composable and $f$ is surjective. Then, $\phi *_1 \phi'$ is connected if and only if $\phi'$ is connected.
Proof. Let $N_{n_2} \xrightarrow{f'} S' \stackrel{g'}{\hookrightarrow} N_{n_3}$ be a representative of $\text{Con}_P(\phi')$ for some $n_2, n_3 \in \mathbb{N}$. Then, $\text{Con}_P(\phi_*1\phi')$ is represented by $N_{n_1} \xrightarrow{f'' \circ f} S'' \stackrel{g'' \circ g'}{\hookrightarrow} N_{n_3}$ where $S'', f''$ and $g''$ are defined by the pushout of $g$ and $f'$ as in

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

Suppose that $\phi'$ is connected, i.e., $f'$ and $g'$ are jointly surjective. Since $f$ is surjective by hypothesis and $f''$ and $g''$ are jointly surjective (by the universal property of pushout), we have that $f'' \circ f, g'' \circ f', g'' \circ g'$ are jointly surjective. Moreover,

$$g'' \circ f' = f'' \circ g = f'' \circ f \circ h$$

where $h$ is a factorization of $g$ through $f$ (that exists, since $f$ is supposed surjective). Thus, we conclude that $f'' \circ f, g'' \circ g'$ are jointly surjective.

Conversely, suppose that $f'' \circ f$ and $g'' \circ g'$ are jointly surjective and let $y \in S'$. We have to show that $y$ is in the image of $f'$ or $g'$. Recall that

$$S'' \cong (S \sqcup S') / \sim$$

where $\sim$ is the equivalence relation induced by $g(x) \sim f'(x)$ for $x \in N_{n_2}$: either $y$ is in the image of $f'$, or we have both that $y$ is the only preimage of $g''(y)$ by $g''$ and $g''(y)$ is not in the image of $f''$. In the former case, we conclude directly, and in the latter, since $f'' \circ f$ and $g'' \circ g'$ are jointly surjective, there is $x \in N_{n_3}$ such that $g'' \circ g'(x) = g''(y)$, so that $g'(x) = y$, which is what we wanted. Thus, $f'$ and $g'$ are jointly surjective, i.e., $\phi'$ is connected. $\square$

We can now prove our connectedness result for pseudoadjunctions:

**Proposition 4.2.4.** For every $\phi \in \text{PAdj}_2^*$, $\phi$ is connected.

Proof. Assume by contradiction that it is not true and let $N \in \mathbb{N}$ be the smallest natural number such that the set $S = \{\phi \in \text{PAdj}_2^* | |\phi| = N \text{ and } \phi \text{ is not connected}\}$ is not empty. Given $\phi \in S$, let

$$(f_1 *_0 \alpha_1 *_0 h_1) *_1 \cdots *_1 (f_N *_0 \alpha_N *_0 h_N)$$

be a decomposition of $\phi$.

Note that there is at least one $i \in \{1, \dots, N\}$ such that $\alpha_i = \varepsilon$. Indeed, given $f, h \in \text{PAdj}_1^*$ such that $f, \eta, h$ are 0-composable, a representative $N_m \xrightarrow{u} T \xleftarrow{v} N_n$ of $\text{Con}_Q(f*_0 \eta*_0 h)$ has the property that $v$ is an epimorphism. Since epimorphisms are stable by pushouts, given $\phi' \in \text{PAdj}_2^*$ such that $\phi' = (f'_1 *_0 \eta*_0 h'_1) *_1 \cdots *_1 (f'_k *_0 \eta*_0 h'_k)$ with $f'_i, h'_i \in \text{PAdj}_1^*$ for $i \in \{1, \dots, k\}$, a representative $N_{m'} \xrightarrow{u'} T' \xleftarrow{v'} N_{n'}$ of $\text{Con}_{\text{PAdj}}(\phi')$ has the property that $v'$ is an epimorphism (by induction on $k$), and in particular, $\phi'$ is connected. Consider the minimal index $i_0$ such that there is $\phi \in S$ with $\alpha_{i_0} = \varepsilon$.

Suppose first that $i_0 = 1$. Then, given a representative $N_{m_1} \xrightarrow{u_1} T_1 \xleftarrow{v_1} N_{m_2}$ of $\text{Con}_{\text{PAdj}}(f_1*_0 \alpha_1*_0 h_1)$, we easily check that $u_1$ is an epimorphism. By Lemma 4.2.3, we deduce that

$$(f_2 *_0 \alpha_2 *_0 h_2) *_1 \cdots *_1 (f_k *_0 \alpha_k *_0 h_k)$$

is not connected, contradicting the minimality of $N$.

Suppose $i_0 > 1$. By the definition of $i_0$, we have $\alpha_{i_0-1} = \eta$. There are different cases depending on $|f_{i_0-1}|$ (see Figure 1):

$$- \text{ if } |f_{i_0-1}| \le |f_{i_0}| - 2, \text{ then, since } \partial_1^+(f_{i_0-1} *_0 \alpha_{i_0-1} *_0 h_{i_0-1}) = \partial_1^-(f_{i_0} *_0 \alpha_{i_0} *_0 h_{i_0}), \text{ we have}$$

$$f_{i_0} = f_{i_0-1} *_0 \partial_1^+(\eta) *_0 g \quad \text{and} \quad h_{i_0-1} = g *_0 \partial_1^-(\varepsilon) *_0 h_{i_0}$$
<figure><img src="image_42.png" /><figcaption>Figure 1: The different cases</figcaption></figure>

for some $g \in \mathrm{PAdj}_1^*$. By Lemma 4.2.2, we have

$$ \mathrm{Con}_{\mathrm{PAdj}}((\eta *_0 g *_0 \partial_1^-(\varepsilon)) *_1 (\partial_1^+(\eta) *_0 g *_0 \varepsilon)) = \mathrm{Con}((\partial_1^-(\eta) *_0 g *_0 \varepsilon) *_1 (\eta *_0 g *_0 \partial_1^+(\varepsilon))) $$

thus, by functoriality of $\mathrm{Con}_{\mathrm{PAdj}}$, the morphism $\phi'$ defined by

$$ \phi' = (f_1 *_0 \alpha_1 *_0 h_1) *_1 \cdots *_1 (f_{i_0-2} *_0 \alpha_{i_0-2} *_0 h_{i_0-2}) \\ *_1 (f_{i_0-1} *_0 g *_0 \varepsilon *_0 h_{i_0}) *_1 (f_{i_0-1} *_0 \eta *_0 g *_0 h_{i_0}) \\ *_1 (f_{i_0+1} *_0 \alpha_{i_0+1} *_0 h_{i_0+1}) *_1 \cdots *_1 (f_k *_0 \alpha_k *_0 h_k) $$

satisfies that $\mathrm{Con}_{\mathrm{PAdj}}(\phi) = \mathrm{Con}_{\mathrm{PAdj}}(\phi')$. So $\phi'$ is not connected, and the $(i_0-1)$-th 2-generator in the decomposition of $\phi'$ is $\varepsilon$, contradicting the minimality of $i_0$;

- if $|f_{i_0-1}| \ge |f_{i_0}| + 2$, then the case is similar to the previous one;

- if $|f_{i_0-1}| = |f_{i_0}| - 1$, then, since $\mathrm{Con}_{\mathrm{PAdj}}((\eta *_0 f) *_1 (f *_0 \varepsilon)) = \mathrm{Con}_{\mathrm{PAdj}}(\mathrm{id}_f)$ by Lemma 4.2.1, the 2-cell $\phi'$ defined by

$$ \phi' = (f_1 *_0 \alpha_1 *_0 h_1) *_1 \cdots *_1 (f_{i_0-2} *_0 \alpha_{i_0-2} *_0 h_{i_0-2}) \\ *_1 (f_{i_0+1} *_0 \alpha_{i_0+1} *_0 h_{i_0+1}) *_1 \cdots *_1 (f_k *_0 \alpha_k *_0 h_k) $$

satisfies $\mathrm{Con}_{\mathrm{PAdj}}(\phi) = \mathrm{Con}_{\mathrm{PAdj}}(\phi')$ (by functoriality of $\mathrm{Con}_{\mathrm{PAdj}}$), so that $\phi'$ is not connected, contradicting the minimality of $N$;

- if $|f_{i_0-1}| = |f_{i_0}| + 1$, then the situation is similar to the previous one, since, by Lemma 4.2.1,

$$ \mathrm{Con}_{\mathrm{PAdj}}((g *_0 \eta) *_1 (\varepsilon *_0 g)) = \mathrm{Con}_{\mathrm{PAdj}}(\mathrm{id}_g); $$

- finally, the case $|f_{i_0-1}| = |f_{i_0}|$ is impossible since

$$ f_{i_0-1} *_0 \partial_1^+(\alpha_{i_0-1}) *_0 h_{i_0-1} = f_{i_0} *_0 \partial_1^-(\alpha_{i_0}) *_0 h_{i_0} $$

and

$$ \partial_1^+(\alpha_{i_0-1}) = f *_0 g \neq g *_0 f = \partial_1^-(\alpha_{i_0}). \quad \square $$

We are now able to prove termination:

**Proposition 4.2.5.** *The rewriting system PAdj is terminating.*

*Proof.* Suppose by contradiction that there is an infinite sequence $S_i$: $\phi_i \Rightarrow \phi_{i+1}$ for $i \ge 0$ with $S_i$ a rewriting step in $\mathrm{PAdj}_3^*$. Since

$$ |\partial_2^-(N)| = |\partial_2^-(\mathcal{U})| = 2 \quad \text{and} \quad |\partial_2^+(N)| = |\partial_2^+(\mathcal{U})| = 0, $$

if the inner 3-generator of $S_i$ is $\mathcal{N}$ or $\mathcal{U}$, for some $i \ge 0$, then $|\phi_{i+1}| = |\phi_i| - 2$. Since

$$ \partial_2^-(X_{\alpha,f,\beta}) = \partial_2^+(X_{\alpha,f,\beta}) = 2 $$

for 0-composable $\alpha \in \mathrm{PAdj}_2$, $f \in \mathrm{PAdj}_1^*$, $\beta \in \mathrm{PAdj}_2$, it means that there is $i_0 \ge 0$ such that for $i \ge i_0$, the inner generator of $S_i$ is an interchanger. By [9, Thm. 16], there is no infinite sequence of rewriting steps made of interchangers. Thus, by Proposition 4.2.4, there is no infinite sequence of rewriting steps whose inner 3-generator is an interchanger of $\mathrm{PAdj}$, contradicting the existence of $(S_i)_{i \ge 0}$. Thus, $\mathrm{PAdj}$ is terminating. $\square$
Finally, we can apply our coherence criterion and show that:

**Theorem 4.2.6.** PAdj is a coherent Gray presentation.

*Proof.* By Proposition 4.2.5, PAdj$_{≤}$$_{3}$ is terminating. Since $R_1, R_2 ∈ PAdj_4$, by Theorem 3.4.5, the conclusion follows. □

## 4.3 Self-dualities

We consider a variant of the preceding example, by considering the theory corresponding to pseudoadjunctions between an endofunctor and itself. This new example requires a special treatment since the underlying rewriting system is not terminating, and, more fundamentally, the induced (3, 2)-Gray category is not expected to be fully coherent. We show instead a partial coherence result.

We define the 3-prepolygraph for self-dualities as the 3-prepolygraph P such that

$$P_0 = \{*\} \text{ and } P_1 = \{\bar{1}: * \to *\} \text{ and } P_2 = \{\eta: \mathrm{id}_* \to \bar{2}, \varepsilon: \bar{2} \to \mathrm{id}_*\}$$

where we write $\bar{n}$ for $\bar{1}_{*0} \cdots \bar{1}_{*0}$ for $n \in \mathbb{N}$. The 2-generators $\eta$ and $\varepsilon$ are pictured as $\frown$ and $\frown$ respectively, and $P_3$ is defined by $P_3 = \{\mathbb{N}, \mathbb{U}\}$ where

$$\mathbb{N}: (\eta *_0 \bar{1}) *_1 (\bar{1} *_0 \varepsilon) \Rightarrow \mathrm{id}_{\bar{1}} \quad \text{and} \quad \mathbb{U}: (\bar{1} *_0 \eta) *_1 (\varepsilon *_0 \bar{1}) \Rightarrow \mathrm{id}_{\bar{1}}$$

which is pictured again by

$$\frown \xrightarrow{\mathbb{N}} \frown \quad \text{and} \quad \frown \xrightarrow{\mathbb{U}} \frown$$

As before, we then extend P to a Gray presentation by adding 3-generators corresponding to interchange generators and 4-generators corresponding to independence generators and interchange naturality generators. We also add the same 4-generators that we added for pseudoadjunctions

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

to P and we denote SD the resulting Gray presentation. Here, it is not possible to apply Theorem 3.4.5 to obtain a coherence result, as in previous section. Indeed, SD is not terminating, since we have the reduction

$$\begin{array}{ccc} \circ & \Rightarrow & \circ \\ \circ & & \circ \end{array} \Rightarrow \begin{array}{ccc} \circ & \Rightarrow & \circ \\ \circ & & \circ \end{array} \Rightarrow \begin{array}{ccc} \circ & \Rightarrow & \circ \\ \circ & & \circ \end{array} \Rightarrow \circ$$

Moreover, this endomorphism 3-cell is not expected to be an identity, discarding hopes for the presentation to be coherent. Following [10], we can still aim at showing a partial coherence result by restricting to 2-cells which are connected, in the sense of the previous section. In this case, termination can actually be shown by using the same arguments as for pseudoadjunctions. However, the critical pairs are not joinable either since, for instance, we have

$$\frown \quad \frown \quad \frown \quad \frown \quad \frown$$
for which there is little hope that a Knuth-Bendix completion will provide a reasonably small
presentation. However, one can obtain a rewriting system, introduced below, which is terminating
on connected 2-cells and confluent by orienting the interchangers. Using this rewriting system, we
are able to show a partial coherence result.

We define an alternate rewriting system $\mathcal{Q}$ where

$$
\mathcal{Q}_i = \mathcal{P}_i \text{ for } i \in \{0, 1, 2\} \quad \text{and} \quad \mathcal{Q}_3 = \{\mathbb{N}, \mathbb{U}\} \sqcup \mathcal{Q}_3^{\text{int}}
$$

where $\mathcal{Q}_3^{\text{int}}$ contains the following 3-generators, called $\mathcal{Q}$-interchange generators:

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
X'_{\eta, \bar{n}, \eta} \arrow[r, "\bigcup"] \arrow[d, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] \\
X'_{\varepsilon, \bar{n}, \eta} \arrow[r, "\bigcup"] \arrow[d, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"]
\end{tikzcd}
\qquad
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
X'_{\eta, \bar{n}, \varepsilon} \arrow[r, "\bigcup"] \arrow[d, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] \\
X'_{\varepsilon, \bar{n}, \varepsilon} \arrow[r, "\bigcup"] \arrow[d, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"] & |\cdots| \arrow[d] \arrow[r] \arrow[dl, "\bigcup"]
\end{tikzcd}
$$

for $n \in \mathbb{N}$.

There is a morphism of 3-precategories $\Gamma: \mathcal{Q}^* \to \bar{\mathcal{P}}^\top$ uniquely defined by $\Gamma(u) = u$ for $u \in \mathcal{Q}_i^*$ with $i \in \{0, 1, 2\}$ and mapping the 3-generators as follows:

$$
\begin{array}{l@{\quad}l}
\mathbb{N} \mapsto \mathbb{N} & \mathbb{U} \mapsto \mathbb{U} \\[1.5ex]
X'_{\eta, \bar{n}, \eta} \mapsto X^{-1}_{\eta, \bar{n}, \eta} & X'_{\eta, \bar{n}, \varepsilon} \mapsto X_{\eta, \bar{n}, \varepsilon} \\[1.5ex]
X'_{\varepsilon, \bar{n}, \eta} \mapsto X^{-1}_{\varepsilon, \bar{n}, \varepsilon} & X'_{\varepsilon, \bar{n}, \varepsilon} \mapsto X_{\varepsilon, \bar{n}, \varepsilon}
\end{array}
$$

for $n \in \mathbb{N}$. We get a rewriting system $(\mathcal{Q}, \equiv)$ by putting $F \equiv F'$ if and only if $\Gamma(F) = \Gamma(F')$ for parallel $F, F' \in \mathcal{Q}_3^*$. By inspecting the 3-generators of $\mathcal{Q}_3$, we can show that, given $F: \phi \Rightarrow \phi' \in \mathcal{Q}_3^*$, $\phi$ is connected if and only if $\phi' \text{ is connected.}$ Indeed, one easily checks that for every $A \in \mathcal{Q}_3$, we have $\mathrm{Con}_\mathcal{Q}(\partial_2^-(A)) = \mathrm{Con}_\mathcal{Q}(\partial_2^+(A))$, so that $\mathrm{Con}_\mathcal{Q}(\phi) = \mathrm{Con}_\mathcal{Q}(\phi')$.

We first show a weak termination property for $\mathcal{Q}$, stating that it is terminating on connected 2-cells:

**Proposition 4.3.1.** *Given a connected 2-cell $\phi$ in $\mathcal{Q}_2^*$, there is no infinite sequence $F_i$: $\phi_i \Rightarrow \phi_{i+1}$ of rewriting steps where $\phi_0 = \phi$.*

*Proof.* Since any rewriting step whose inner 3-generator is $\mathbb{N}$ or $\mathbb{U}$ decreases by two the number of 2-generators in a diagram, it is enough to show that there is no infinite sequence of composable rewriting steps made of elements of $\mathcal{Q}_3^{\text{int}}$. For this purpose, we combine several counting functions: a function $N_1$ which counts the potential number of rules $X'_{\eta,-,\epsilon}$ and $X'_{\epsilon,-,\eta}$ which can be applied, and functions $N_2^{\eta}$ and $N_2^{\epsilon}$ which counts the potential number of rules $X'_{\eta,-,\eta}$ and $X'_{\epsilon,-,\epsilon}$ which can be applied respectively. Given a 2-cell

$$
\phi = (\bar{m}_1 *_0 \alpha_1 *_0 \bar{n}_1) *_1 \cdots *_1 (\bar{m}_k *_0 \alpha_k *_0 \bar{n}_k)
$$

of $\mathcal{Q}_2^*$, with $\alpha_i \in \mathcal{Q}_2$ and $m_i, n_i \in \mathbb{N}$ for $i \in \{1, \dots, k\}$, we define $N_1(\phi) \in \mathbb{N}$ by

$$
N_1(\phi) = |\{(i, j) \in \mathbb{N}^2 \mid 1 \le i < j \le k \text{ and } \alpha_i = \eta \text{ and } \alpha_j = \epsilon\}|.
$$

Moreover, if we write $p, q \in \{0, \dots, k\}$ and $i_1, \dots, i_p, j_1, \dots, j_q \in \mathbb{N}$ for the unique integers such that

$$
1 \le i_1 < \dots < i_p \le k \quad 1 \le j_1 < \dots < j_q \le k \quad \{i_1, \dots, i_p, j_1, \dots, j_q\} = \{1, \dots, k\}
$$

and $\alpha_{i_r} = \eta$ and $\alpha_{j_s} = \epsilon$ for $r \in \{1, \dots, p\}$ and $s \in \{1, \dots, q\}$, we define $N_2^\eta(\phi) \in \mathbb{N}^p$ and $N_2^\epsilon(\phi) \in \mathbb{N}^q$ by

$$
N_2^{\eta}(\phi) = (n_{i_p}, \dots, n_{i_1}) \quad \text{and} \quad N_2^{\epsilon}(\phi) = (n_{j_1}, \dots, n_{j_q}).
$$

Finally, we define $N(\phi) \in \mathbb{N}^{1+p+q}$ by

$$
N(\phi) = (N_1(\phi), N_2^{\eta}(\phi), N_2^{\epsilon}(\phi))
$$

and we equip $\mathbb{N}^p$, $\mathbb{N}^q$ and $\mathbb{N}^{1+p+q}$ with the lexicographical ordering $<_{\text{lex}}$. Now, keeping $\phi$ as above, let

$$
\lambda *_1 (l *_0 A *_0 r) *_1 \rho : \phi \Rightarrow \phi' \in \mathcal{Q}_3^*
$$
be a rewriting step for some $l, r \in \mathbb{Q}_1^*$, $\lambda, \rho, \phi' \in \mathbb{Q}_2^*$ and $A \in \mathbb{Q}_3$ with

$$ \phi' = (\bar{m}'_1 *_0 \alpha'_1 *_0 \bar{n}'_1) *_1 \cdots *_1 (\bar{m}'_k *_0 \alpha'_k *_0 \bar{n}'_k) $$

for some $\alpha'_i \in \mathbb{Q}_2$ and $m'_i, n'_i \in \mathbb{N}$ for $i \in \{1, \dots, k\}$. We distinguish the three following cases.

- If $A = X'_{\eta, \bar{u}, \varepsilon}$ or $A = X'_{\varepsilon, \bar{u}, \eta}$ for some $u \in \mathbb{N}$, then $N_1(\phi') = N_1(\phi) - 1$.

- Otherwise, if $A = X_{\eta, \bar{u}, \eta}$ for some $u \in \mathbb{N}$, then we have $N_1(\phi) = N_1(\phi')$ and, writing $r$ for $|\lambda|+1$, we have $n_s = n'_s$ for $s \in \{1, \dots, k\} \setminus \{r, r+1\}$. Moreover, we have $n'_{r+1} \le n_{r+1} - 2$, so that $N_2^\eta(\phi') <_{\text{lex}} N_2^\eta(\phi)$. For example, consider the application of $X'_{\eta, \bar{n}, \eta}$ on $\partial_2^-(X'_{\eta, \bar{n}, \eta})$ without additional whiskering. In this case, we have that $N_2^\eta(\partial_2^-(X'_{\eta, \bar{n}, \eta})) = (n+2, 0)$ while $N_2^\eta(\partial_2^+(X'_{\eta, \bar{n}, \eta})) = (0, n)$, so that the value of $N_2^\eta(-)$ is decreased with respect to $<_{\text{lex}}$ by the application of $X'_{\eta, \bar{n}, \eta}$.

- Otherwise, $A = X'_{\varepsilon, \bar{u}, \varepsilon}$ for some $u \in \mathbb{N}$. Then $N_2^\eta(\phi) = N_2^\eta(\phi')$ and, by a similar argument as before, $N_2^\varepsilon(\phi') <_{\text{lex}} N_2^\varepsilon(\phi)$.

In any case, we get that $N(\phi) <_{\text{lex}} N(\phi')$. Since $<_{\text{lex}}$ is well-founded, we conclude that there is no infinite sequence of rewriting steps $R_i: \phi_i \Rightarrow \phi_{i+1}$ for $i \in \mathbb{N}$ with $\phi_0$ connected. $\square$

We now aim at showing the confluence of the branchings of $\mathbb{Q}$. The idea is to use a critical pair lemma and a Newman's lemma adapted to the specific setting of $\mathbb{Q}$ where the notion of critical branching is different and where we only consider connected 2-cells as sources. We say that a branching $(S_1, S_2)$ of $\mathbb{Q}$ is *connected* when $\partial_2^-(S_1)$ is connected. We say that it is *Q-critical* when it is local, minimal, not trivial and not independent. We first state adapted versions of the critical pair lemma and Newman's lemma to the setting of $\mathbb{Q}$:

**Lemma 4.3.2.** If all connected Q-critical branchings $(S_1, S_2)$ of $(\mathbb{Q}, \equiv)$ are confluent, then all connected local branchings of $(\mathbb{Q}, \equiv)$ are confluent.

*Proof.* By a direct adaptation of the proof of Theorem 3.4.3 to connected 2-cells and rewriting steps between connected 2-cells. $\square$

**Lemma 4.3.3.** If all connected local branchings of $(\mathbb{Q}, \equiv)$ are confluent, then all connected branchings of $(\mathbb{Q}, \equiv)$ are confluent.

*Proof.* By a direct adaptation of Theorem 3.2.1 to connected 2-cells and rewriting steps between connected 2-cells, using Proposition 4.3.1. $\square$

By the above properties, in order to deduce the confluence of the branchings of $\mathbb{Q}$, it is enough to check that the critical branchings of $\mathbb{Q}$ are confluent, fact that we verify in the following property:

**Lemma 4.3.4.** The connected Q-critical branchings of $(\mathbb{Q}, \equiv)$ are confluent.

*Proof.* We first consider the Q-critical branchings $(S_1, S_2)$ that are structural-structural, i.e., such that the inner 3-generators of $S_1$ and $S_2$ are Q-interchange generators. We classify them as separated and half-separated and non-separated. There are eight kinds of separated structural-structural Q-critical branchings listed below:

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

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

<figure><img src="image_46.png" /></figure>
Proof. Let $\Gamma'$: $\overline{\mathbb{Q}}^{\top} \to \overline{\mathbb{SD}}^{\top}$ be the 3-prefunctor which is the factorization of $\Gamma$ through the canonical 3-prefunctor $(\mathbb{Q}_{\le 3})^* \to \overline{\mathbb{Q}}^{\top}$. By definition of $\overline{\mathbb{SD}}^{\top}$, for $i \in \{1, 2\}$, we have

$$F_i = G_{i,1} *_2 H_{i,1}^{-1} *_2 \cdots *_2 G_{i,k_i} *_2 H_{i,k_i}^{-1}$$

for some $k_i \in \mathbb{N}$, 2-cells $\phi_{i,0}, \dots, \phi_{i,k_i}$, $\psi_{i,1}, \dots, \psi_{i,k_i} \in \mathbb{Q}_2^*$ such that $\phi_{i,0} = \phi$ and $\phi_{i,k_i} = \phi'$, and, for $j \in \{1, \dots, k_i\}$, 3-cells

$$G_{i,j}: \phi_{i,j-1} \Rightarrow \psi_{i,j} \quad \text{and} \quad H_{i,j}: \phi_{i,j} \Rightarrow \psi_{i,j}$$

of $\overline{\mathbb{SD}}_3$. Since either $\phi$ or $\phi'$ is connected, we have that all the $\phi_{i,j}$'s and the $\psi_{i,j}$'s are connected. Moreover, all the $G_{i,j}$'s and the $H_{i,j}$'s are in the image of $\Gamma'$. So, for $i \in \{1, 2\}$, $F_i = \Gamma'(F'_i)$ for some $F'_i: \phi \Rightarrow \phi' \in \overline{\mathbb{Q}}^{\top}$. By Lemma 4.3.8, we have $F'_1 = F'_2$, so that $F_1 = F_2$. $\square$

## 4.4 Frobenius pseudomonoids

We now consider the example of Frobenius pseudomonoids [30], which categorifies the classical notion of Frobenius monoids. Sadly, it is only a partial example since we were not able to handle the units of the structure (if we add them, the critical branchings are not confluent) and to show that our presentation is terminating, even though we believe that the latter is true. We nevertheless give the computation of critical branchings for this example, hoping that a termination argument will be found later.

We define the 3-prepolygraph P for (non-unitary) Frobenius pseudomonoids as follows. We put

$$P_0 = \{*\} \quad \text{and} \quad P_1 = \{\bar{1}\} \quad \text{and} \quad P_2 = \{\mu: \bar{2} \to \bar{1}, \delta: \bar{1} \to \bar{2}\}$$

where we denote $\bar{n}$ by $\underbrace{\bar{1} *_0 \cdots *_0 \bar{1}}_{n}$ for $n \in \mathbb{N}$. We picture $\mu$ and $\delta$ by $\triangleright$ and $\triangleleft$ respectively, and we define $P_3$ by $P_3 = \{\mathbb{N}, \mathbb{U}, \mathbb{A}, \mathbb{A}^{\mathrm{co}}, \mathbb{M}, \mathbb{M}^{\mathrm{co}}\}$ where

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

As before, we then extend P to a Gray presentation by adding 3-generators corresponding to interchange generators and 4-generators corresponding to independence generators and interchange naturality generators.

Using the constructive proof of Theorem 3.4.6, we find 19 critical branchings, and we use them to define a set of nineteen 4-generators $R_1, \dots, R_{19}$ that we add to $P_4$. These critical branchings are shown in Figure 2. We then define PFrob as the Gray presentation obtained from P by adding the 4-generators $R_1, \dots, R_{19}$ from above. Since we were not able to show termination, we conjecture it:

**Conjecture 4.4.1.** PFrob is terminating.

From this assumption, we deduce that:

**Theorem 4.4.2.** If PFrob is terminating, then PFrob is a coherent Gray presentation.

*Proof.* This is a consequence of Theorem 3.4.5. $\square$
<figure><img src="image_48.png" /><figcaption>Figure 2a: The critical branchings for Frobenius pseudomonoids</figcaption></figure>
<figure><img src="image_49.png" /><figcaption>Figure 2b: The critical branchings for Frobenius pseudomonoids</figcaption></figure>
<figure><img src="image_50.png" /><figcaption>Figure 2c: The critical branchings for Frobenius pseudomonoids</figcaption></figure>
References

[1] Jiří Adámek and Jiří Rosický. *Locally presentable and accessible categories*, volume 189. Cambridge University Press, 1994.

[2] Franz Baader and Tobias Nipkow. *Term rewriting and all that*. Cambridge university press, 1999.

[3] 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.

[4] Krzysztof Bar and Jamie Vicary. Data structures for quasidistrict higher categories. In *Logic in Computer Science (LICS)*, 32nd Annual Symposium on, pages 1–12. IEEE, 2017.

[5] Michael Barr and Charles Wells. Topos, triples and theories, 2005.

[6] Michael A Batanin. Computads for finitary monads on globular sets. *Contemporary Mathematics*, 230:37–58, 1998.

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

[8] Max Dehn. Über unendliche diskontinuierliche gruppen. *Mathematische Annalen*, 71(1):116–144, 1911.

[9] Antonin Delpeuch and Jamie Vicary. Normalization for planar string diagrams and a quadratic equivalence algorithm. *arXiv preprint arXiv:1804.07832*, 2018.

[10] Lawrence Dunn and Jamie Vicary. Coherence for Frobenius pseudomonoids and the geometry of linear proofs. Preprint, 2016.

[11] Robert Gordon, John Power, and Ross Street. *Coherence for tricategories*, volume 558. American Mathematical Society, 1995.

[12] John W Gray. *Formal category theory: adjointness for 2-categories*, volume 391. Springer, 1974.

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

[14] Yves Guiraud and Philippe Malbos. Coherence in monoidal track categories. *Mathematical Structures in Computer Science*, 22(6):931–969, 2012.

[15] Yves Guiraud and Philippe Malbos. Polygraphs of finite derivation type. *Mathematical Structures in Computer Science*, pages 1–47, 2016.

[16] 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.

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

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

[19] Yves Lafont. Penrose diagrams and 2-dimensional rewriting. *Applications of Categories in Computer Science*, 177:191–201, 1992.

[20] Yves Lafont. A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier). *Journal of Pure and Applied Algebra*, 98(3):229–244, 1995.

[21] Yves Lafont. Towards an algebraic theory of boolean circuits. *Journal of Pure and Applied Algebra*, 184(2):257–310, 2003.
[22] Saunders MacLane. Natural associativity and commutativity. *Rice Institute Pamphlet-Rice University Studies*, 49(4), 1963.

[23] Michael Makkai. The word problem for computads. Available on the author's web page http://www.math.mcgill.ca/makkai/, 2005.

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

[25] François Métayer. Cofibrant objects among higher-dimensional categories. *Homology, Homotopy and Applications*, 10(1):181-203, 2008.

[26] Craig C Squier. Word problems and a homological finiteness condition for monoids. *Journal of Pure and Applied Algebra*, 49(1-2):201-217, 1987.

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

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

[29] Ross Street. Categorical structures. *Handbook of algebra*, 1:529-577, 1996.

[30] Ross Street. Frobenius monads and pseudomonoids. *Journal of Mathematical Physics*, 45(10):3930-3948, 2004.

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

[32] Axel Thue. *Probleme über Veränderungen von Zeichenreihen nach gegebenen Regeln*, volume 10. 1914.

[33] Mark Weber. Free products of higher operad algebras. *arXiv preprint arXiv:0909.4722*, 2009.
# A Equivalence between definitions of precategories

We prove the equivalence between the equational and the enriched definition of precategories:

**Proposition 1.4.5.** There is an equivalence of categories between $(n+1)$-precategories and categories enriched in $n$-precategories with the funny tensor product.

*Proof.* Given $C \in \mathbf{PCat}_{n+1}$, we define an associated object $D \in (\mathbf{PCat}_n)$-Cat as follows. We put

$$D_0 = C_0 \quad \text{and} \quad D(x, y) = C_{\uparrow(x, y)}$$

where $C_{\uparrow(x,y)}$ is the $n$-precategory such that

$$(C_{\uparrow(x,y)})_i = \{u \in C_{i+1} \mid \partial_0^-(u) = x \text{ and } \partial_0^+(u) = y\}$$

for $i \in \{0, \dots, n\}$ and whose composition operation $*_k$ is the operation $*_{k+1,l+1}$ on $C$ for $k, l \in \{1, \dots, n\}$. Given $x \in D_0$, we define the identity morphism

$$i_x: 1 \to D(x, x)$$

as the morphism which maps the unique 0-cell $*$ of 1 to $\mathrm{id}_x \in C_1$. Given $x, y, z \in C_0$, we define the composition morphism

$$c_{x,y,z}: D(x, y) \sqcap D(y, z) \to D(x, z) \in \mathbf{PCat}_n$$

as the unique morphism such that $l_{x,y,z} = c_{x,y,z} \circ l_{D(x,y),D(y,z)}$ is the composite

$$D(x, y) \times D(y, z)_{(0)} \cong \coprod_{g \in D(y, z)_0} D(x, y) \xrightarrow{[(-)*_0 g]_{g \in D(y, z)_0}} D(x, z)$$

and $r_{x,y,z} = c_{x,y,z} \circ r_{D(x,y),D(y,z)}$ is the composite

$$D(x, y)_{(0)} \times D(y, z) \cong \coprod_{f \in D(x, y)_0} D(y, z) \xrightarrow{[f*_0(-)]_{f \in D(x, y)_0}} D(x, z).$$

We verify that the composition morphism is left unital, i.e., given $x, y \in D_0$, the diagram

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

commutes. We compute that

$$
\begin{align*}
c_{x,x,y} \circ (i_x \sqcap D(x,y)) \circ l_{1,D(x,y)} &= c_{x,x,y} \circ l_{D(x,x),D(x,y)} \circ (i_x \times D(x,y)_{(0)}) \tag{by definition of \square} \\
&= l_{x,x,y} \circ (i_x \times D(x,y)_{(0)}) \tag{by unitality of $\mathrm{id}_x$} \\
&= j_{D(x,y)} \circ \pi_2 \tag{by unitality of $\mathrm{id}_x$} \\
&= \lambda_{D(x,y)}^f \circ l_{1,D(x,y)}
\end{align*}
$$

and

$$
\begin{align*}
c_{x,x,y} \circ (i_x \sqcap D(x,y)) \circ r_{1,D(x,y)} &= c_{x,x,y} \circ r_{D(x,x),D(x,y)} \circ ((i_x)_{(0)} \times D(x,y)) \tag{by definition of \square} \\
&= r_{x,x,y} \circ ((i_x)_{(0)} \times D(x,y)) \tag{by unitality of $\mathrm{id}_x$} \\
&= \pi_2 \tag{by unitality of $\mathrm{id}_x$} \\
&= \lambda_{D(x,y)}^f \circ r_{1,D(x,y)}
\end{align*}
$$
Thus, by the colimit definition of $1 \square D(x, y)$, the above triangle commutes. Similarly, the triangle

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

commutes, so that the composition morphism is right unital. We now verify that it is associative, i.e., given $w, x, y, z \in D_0$, that the diagram

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

commutes. By a colimit definition analogous to (2), it is enough to show the commutation of the diagram when precomposing with the morphisms $\varpi_1, \varpi_2, \varpi_3$ where

$$ 
\begin{align*}
\varpi_1 &= l_{D(w,x) \square D(x,y), D(y,z)} \circ (l_{D(w,x), D(x,y)} \times D(y,z)_{(0)}), \\
\varpi_2 &= l_{D(w,x) \square D(x,y), D(y,z)} \circ (r_{D(w,x), D(x,y)} \times D(y,z)_{(0)}), \\
\varpi_3 &= r_{D(w,x) \square D(x,y), D(y,z)}.
\end{align*}
$$

Writing $D^1, D^2, D^3$ for $D(w, x), D(x, y), D(y, z)$, we compute that

$$ 
\begin{align*}
c_{w,x,z} \circ (D^1 \square c_{x,y,z}) \circ \alpha_{D^1, D^2, D^3} \circ \varpi_1 \\
&= c_{w,x,z} \circ (D^1 \square c_{x,y,z}) \circ \alpha_{D^1, D^2, D^3} \circ l_{D^1 \square D^2, D^3} \circ (l_{D^1, D^2} \times D^3_{(0)}) \\
&= c_{w,x,z} \circ (D^1 \square c_{x,y,z}) \circ l_{D^1, D^2 \square D^3} \circ \alpha_{D^1, D^2_{(0)}, D^3_{(0)}} \\
&= c_{w,x,z} \circ l_{D^1, D(x,z)} \circ (D^1 \times ((-)*_0(-))) \circ \alpha_{D^1, D^2_{(0)}, D^3_{(0)}} \\
&= ((-)*_0(-)) \circ (D^1 \times ((-)*_0(-))) \circ \alpha_{D^1, D^2_{(0)}, D^3_{(0)}} \\
&= ((-)*_0(-)) \circ (((-)*_0(-)) \times D^3_{(0)}) \tag{by associativity of *0} \\
&= c_{w,y,z} \circ l_{D(w,y), D^3} \circ (((-)*_0(-)) \times D^3_{(0)}) \\
&= c_{w,y,z} \circ l_{D(w,y), D^3} \circ (c_{w,x,y} \times D^3_{(0)}) \circ (l_{D^1, D^2} \times D^3_{(0)}) \\
&= c_{w,y,z} \circ (c_{w,x,y} \square D^3) \circ l_{D^1 \square D^2, D^3} \circ (l_{D^1, D^2} \times D^3_{(0)}) \\
&= c_{w,y,z} \circ (c_{w,x,y} \square D^3) \circ \varpi_1
\end{align*}
$$

so that the diagram (10) commutes when precomposed with $\varpi_1$ and, similarly, it commutes when precomposed with $\varpi_2$ and $\varpi_3$. Thus, (10) commutes. Hence, $D$ is a category enriched in $n$-precategories. The operation $C \mapsto D$ can easily be extended to morphisms of $(n+1)$-precategories, giving a functor

$$ F: \mathbf{PCat}_{n+1} \to (\mathbf{PCat}_n)\text{-Cat.} $$

Conversely, given $C \in (\mathbf{PCat}_n)\text{-Cat}$, we define an associated object $D \in \mathbf{PCat}_{n+1}$. We put

$$ D_0 = C_0 \quad \text{and} \quad D_{i+1} = \coprod_{x,y \in C_0} C(x,y)_i $$

for $i \in \{0, \dots, n\}$. In the following, given $x, y \in C_0$, we write $\iota_{x,y}: C(x, y)_i \to D_{i+1}$ for the canonical coprojection. Given $k \in \mathbb{N}$ with $k \le n$, $\iota_{x,y}(u) \in D_{k+1}$ and $\epsilon \in \{-, +\}$, we put

$$ \partial_k^\epsilon(\iota_{x,y}(u)) = \begin{cases} x & \text{if } k=0 \text{ and } \epsilon=-, \\ y & \text{if } k=0 \text{ and } \epsilon=+, \\ \iota_{x,y}(\partial_{k-1}^\epsilon(u)) & \text{if } k>0, \end{cases} $$
so that the operations $\partial^-$, $\partial^+$ equips $D$ with a structure of $(n+1)$-globular set. Given $x \in D_0$, we put

$$ \mathrm{id}_x = \iota_{x,x}(i_x(\ast)) $$

and, given $k \in \mathbb{N}$ with $k \le n-1$ and $\iota_{x,y}(u) \in D_{k+1}$, we put

$$ \mathrm{id}_{\iota_{x,y}(u)}^{k+2} = \iota_{x,y}(\mathrm{id}_u^{k+1}). $$

Given $i, k_1, k_2 \in \{0, \dots, n\}$ with $i = \min(k_1, k_2) - 1$, and $u = \iota_{x,y}(\tilde{u}) \in D_{k_1}, v = \iota_{x',y'}(\tilde{v}) \in D_{k_2}$ that are $i$-composable, we put

$$ u *_{i} v = \begin{cases} \iota_{x,y}(\tilde{u} *_{i} \tilde{v}) & \text{if } i > 0 \\ \iota_{x,y'}(l_{x,y,y'}(\tilde{u}, \mathrm{id}_{\tilde{v}}^{k_1-1})) & \text{if } i = 0 \text{ and } k_2 = 1 \\ \iota_{x,y'}(r_{x,y,y'}(\mathrm{id}_{\tilde{u}}^{k_2-1}, \tilde{v})) & \text{if } i = 0 \text{ and } k_1 = 1 \end{cases} $$

where $l_{x,y,z}$ is the composite

$$ C(x, y) \times C(y, z)_{(0)} \xrightarrow{\mathrm{l}_{C(x,y),C(y,z)}} C(x, y) \boxtimes C(y, z) \xrightarrow{\mathrm{c}_{x,y,z}} C(x, z) $$

and $r_{x,y,z}$ is the composite

$$ C(x, y)_{(0)} \times C(y, z) \xrightarrow{\mathrm{r}_{C(x,y),C(y,z)}} C(x, y) \boxtimes C(y, z) \xrightarrow{\mathrm{c}_{x,y,z}} C(x, z). $$

We now have to show that the axioms of $(n+1)$-precategories are satisfied. Note that, by the definition of $D$, it is enough to prove the axioms for the $\mathrm{id}^1$ and $\ast_0$ operations. Given $x \in D_0$ and $\epsilon \in \{-, +\}$, we have

$$ \partial_0^\epsilon(\mathrm{id}_x) = \partial_0^\epsilon(\iota_{x,x}(i_x(\ast))) = x $$

so that Axiom (i) holds. For $k \in \{1, \dots, n+1\}$, given $u = \iota_{x,y}(\tilde{u}) \in D_k$ and $v = \iota_{y,z}(\tilde{v}) \in D_1$ such that $u, v$ are 0-composable, if $k=1$, then

$$ \partial_0^-(u *_0 v) = \partial_0^-(\iota_{x,z}(l_{x,y,z}(\tilde{u}, \tilde{v}))) = x, $$

and, similarly, $\partial_0^+(u *_0 v) = z$. Otherwise, if $k > 1$, then, for $\epsilon \in \{-, +\}$,

$$ \begin{aligned} \partial_{k-1}^{\epsilon}(u *_0 v) &= \partial_{k-1}^{\epsilon}(\iota_{x,z}(l_{x,y,z}(\tilde{u}, \mathrm{id}_{\tilde{v}}^{k-1}))) \\ &= \iota_{x,z}(\partial_{k-2}^{\epsilon}(l_{x,y,z}(\tilde{u}, \mathrm{id}_{\tilde{v}}^{k-1}))) \\ &= \iota_{x,z}(l_{x,y,z}(\partial_{k-2}^{\epsilon}(\tilde{u}), \mathrm{id}_{\tilde{v}}^{k-2})) \\ &= \iota_{x,y}(\partial_{k-2}^{\epsilon}(\tilde{u})) *_0 \iota_{y,z}(\tilde{v}) \\ &= \partial_{k-1}^{\epsilon}(u) *_0 v. \end{aligned} $$

Analogous equalities are satisfied for 0-composable $u \in D_1$ and $v \in D_k$, so that Axiom (ii) holds. Given $k \in \{1, \dots, n+1\}$ and $u = \iota_{x,y}(\tilde{u}) \in D_k$, we have

$$ \begin{aligned} u *_0 \mathrm{id}_y &= \iota_{x,y}(l_{x,y,y}(\tilde{u}, \mathrm{id}_{\tilde{u}}^{k-1})) \\ &= \iota_{x,y}(c_{x,y,y} \circ (C(x,y) \boxtimes i_y) \circ \mathrm{l}_{C(x,y),1}(\tilde{u}, \mathrm{id}_*^{k-1})) \\ &= \iota_{x,y}(\rho_{C(x,y)}^f \circ \mathrm{l}_{C(x,y),1}(\tilde{u}, \mathrm{id}_*^{k-1})) \quad \text{(by the axioms of enriched categories)} \\ &= \iota_{x,y}(\pi_1(\tilde{u}, \mathrm{id}_*^{k-1})) \quad \text{(by definition of $\rho^f$)} \\ &= u. \end{aligned} $$

Moreover, given $k \in \{1, \dots, n\}$ and 0-composable $u = \iota_{x,y}(\tilde{u}) \in D_1$ and $v = \iota_{y,z}(\tilde{v}) \in D_k$, we have

$$ \begin{aligned} u *_0 \mathrm{id}_v^{k+1} &= \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^k, \mathrm{id}_v^k)) \\ &= \iota_{x,z}(\mathrm{id}_k^k(r_{x,y,z}(\mathrm{id}_u^{k-1}, \tilde{v}))) \\ &= \mathrm{id}^{k+1}(\iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k-1}, \tilde{v}))) \end{aligned} $$
$$= \mathrm{id}_{u*_{0}v}^{k+1}.$$

Analogous equalities hold when composing with identities on the left, so that Axiom (iii) holds. Given $k \in \{1, \dots, n+1\}$ and 0-composable $u_1 = \iota_{w,x}(\tilde{u}_1) \in D_k$, $u_2 = \iota_{x,y}(\tilde{u}_2) \in D_1$ and $u_3 = \iota_{y,z}(\tilde{u}_3) \in D_1$, we have

$$(u_1 *_0 u_2) *_0 u_3 = \iota_{w,z}(l_{w,y,z}(l_{w,x,y}(\tilde{u}_1, \mathrm{id}_{\tilde{u}_2}^{k-1}), \mathrm{id}_{\tilde{u}_3}^{k-1})).$$

Writing $C^1, C^2, C^3$ for $C(w, x), C(x, y), C(y, z)$, we compute that

$$
\begin{align*}
& l_{w,y,z} \circ (l_{w,x,y} \times C_{(0)}^3) \\
&= c_{w,y,z} \circ l_{C(w,y),C^3} \circ (c_{w,x,y} \times C_{(0)}^3) \circ (l_{C^1,C^2} \times C_{(0)}^3) \\
&= c_{w,y,z} \circ (c_{w,x,y} \Box C^3) \circ l_{C^1 \Box C^2, C^3} \circ (l_{C^1,C^2} \times C_{(0)}^3) \tag*{(by definition of \square)} \\
&= c_{w,x,z} \circ (C^1 \Box c_{x,y,z}) \circ \alpha_{C^1,C^2,C^3} \circ l_{C^1 \Box C^2, C^3} \circ (l_{C^1,C^2} \times C_{(0)}^3) \tag*{(by the axioms of enriched categories)} \\
&= c_{w,x,z} \circ (C^1 \Box c_{x,y,z}) \circ l_{C^1,C^2 \Box C^3} \circ \alpha_{C^1,C^2_{(0)},C^3_{(0)}} \tag*{(by definition of \alpha)} \\
&= c_{w,x,z} \circ l_{C^1,C(x,z)} \circ (C^1 \times (c_{x,y,z})_{(0)}) \circ \alpha_{C^1,C^2_{(0)},C^3_{(0)}} \\
&= l_{w,x,z} \circ (C^1 \times (l_{x,y,z})_{(0)}) \circ \alpha_{C^1,C^2_{(0)},C^3_{(0)}}.
\end{align*}
$$

Thus,

$$
\begin{align*}
(u_1 *_0 u_2) *_0 u_3 &= \iota_{w,z}(l_{w,x,z}(\tilde{u}_1, (l_{x,y,z})_{(0)}(\mathrm{id}_{\tilde{u}_2}^{k-1}, \mathrm{id}_{\tilde{u}_3}^{k-1}))) \\
&= \iota_{w,z}(l_{w,x,z}(\tilde{u}_1, \mathrm{id}_{(l_{x,y,z})_{(0)}(\tilde{u}_2, \tilde{u}_3)}^{k-1})) \\
&= u_1 *_0 \iota_{x,z}((l_{x,y,z})_{(0)}(\tilde{u}_2, \tilde{u}_3)) \\
&= u_1 *_0 \iota_{x,z}(l_{x,y,z}(\tilde{u}_2, \tilde{u}_3)) \\
&= u_1 *_0 (u_2 *_0 u_3)
\end{align*}
$$

and similar equalities can be shown for $(u_1, u_2, u_3) \in (D_1 \times_0 D_k \times_0 D_1) \sqcup (D_1 \times_0 D_1 \times_0 D_k)$, so that Axiom (iv) holds. Finally, for $i, k_1, k_2, k \in \{1, \dots, n+1\}$ such that $i = \min(k_1, k_2) - 1$, $k = \max(k_1, k_2)$, given $u = \iota_{x,y}(\tilde{u}) \in D_1$ and $i$-composable $v_1 = \iota_{y,z}(\tilde{v}_1) \in D_{k_1}$, $v_2 = \iota_{y,z}(\tilde{v}_2) \in D_{k_2}$, we have

$$
\begin{align*}
u *_0 (v_1 *_i v_2) &= u *_0 \iota_{y,z}(\tilde{v}_1 *_{i-1} \tilde{v}_2) \\
&= \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k-1}, \tilde{v}_1 *_{i-1} \tilde{v}_2)) \\
&= \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k_1-1} *_{i-1} \mathrm{id}_u^{k_2-1}, \tilde{v}_1 *_{i-1} \tilde{v}_2)) \\
&= \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k_1-1}, \tilde{v}_1) *_{i-1} r_{x,y,z}(\mathrm{id}_u^{k_2-1}, \tilde{v}_2)) \\
&= \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k_1-1}, \tilde{v}_1)) *_i \iota_{x,z}(r_{x,y,z}(\mathrm{id}_u^{k_2-1}, \tilde{v}_2)) \\
&= (u *_0 v_1) *_i (u *_0 v_2)
\end{align*}
$$

and an analogous equality can be shown for $((u_1, u_2), v) \in ((D_{k_1} \times_i D_{k_2}) \times_0 D_1)$, so that Axiom (v) holds. Hence, $D$ is an $(n+1)$-precategory. The construction $C \mapsto D$ extends naturally to enriched functors, giving a functor $G: (\mathbf{PCat}_{n+1})\text{-}\mathbf{Cat} \to \mathbf{PCat}_{n+1}$.

Given $C \in \mathbf{PCat}_{n+1}$ and $C' = G \circ F(C)$, there is a morphism $\alpha_C: C \to C'$ which is the identity between $C_0$ and $C'_0$ and, for $k \in \mathbb{N}$ with $k \le n$, maps $u \in C_{k+1}$ to $\iota_{x,y}(u)$ where $x = \partial_0^-(u)$ and $y = \partial_0^+(u)$, and one can verify that it is an isomorphism which is natural in $C$.

Conversely, given $C \in (\mathbf{PCat}_n)\text{-}\mathbf{Cat}$ and $C' = F \circ G(C)$, there is a morphism $\beta: C \to C'$ which is the identity between $C_0$ and $C'_0$, and, for $x, y \in C_0$, maps $u \in C(x, y)$ to $\iota_{x,y}(u) \in C'(x, y)$, and one can verify that it is an isomorphism which is natural in $C$. Hence, $F$ is an equivalence of categories. $\square$
B Gray presentations induce Gray categories

Until the end of this section, we suppose fixed a Gray presentation P. Our goal is to prove Theorem 2.3.2, i.e., that $\bar{P}$ is a lax Gray category. We start by the exchange law for 3-cells that we prove first on rewriting steps:

**Lemma B.1.** Given rewriting steps $R_i: \phi_i \Rightarrow \phi'_i \in \mathbb{P}_3^*$ for $i \in \{1,2\}$, such that $R_1, R_2$ are 1-composable, we have, in $\bar{\mathbb{P}}_3$,

$$ (R_1 *_1 \phi_2) *_2 (\phi'_1 *_1 R_2) = (\phi_1 *_1 R_2) *_2 (R_1 *_1 \phi'_2). $$

*Proof.* Let $l_i, r_i \in \bar{\mathbb{P}}_1$, $\lambda_i, \rho_i \in \bar{\mathbb{P}}_2$, $A_i \in \mathbb{P}_3$ such that $R_i = \lambda_i *_0 (l_i *_0 A_i *_0 r_i) *_i \rho_i$ for $i \in \{1,2\}$, and $\mu_i, \mu'_i \in \bar{\mathbb{P}}_2$ such that $A_i: \mu_i \Rightarrow \mu'_i$ for $i \in \{1,2\}$. In $\bar{\mathbb{P}}_3$, we have

$$
\begin{align*}
(R_1 *_1 \phi_2) *_2 (\phi'_1 *_1 R_2) &= \lambda_1 \\
&\quad [(l_1 *_0 A_1 *_0 r_1) *_1 \rho_1 *_1 \lambda_2 *_1 (l_2 *_0 \mu_2 *_0 r_2)] \\
&\quad *_2 ((l_1 *_0 \mu'_1 *_0 r_1) *_1 \rho_1 *_1 \lambda_2 *_1 (l_2 *_0 A_2 *_0 r_2))] \\
&= \lambda_1 \\
&\quad [(l_1 *_0 \mu_1 *_0 r_1) *_1 \rho_1 *_1 \lambda_2 *_1 (l_2 *_0 A_2 *_0 r_2)] \\
&\quad *_2 ((l_1 *_0 A_1 *_0 r_1) *_1 \rho_1 *_1 \lambda_2 *_1 (l_2 *_0 \mu'_2 *_0 r_2))] \\
&\quad *_1 \rho_2 \\
&= (\phi_1 *_1 R_2) *_2 (R_1 *_1 \phi'_2) \tag*{\text{(by the axioms of precategories)}} \\
&= (\phi_1 *_1 R_2) *_2 (R_1 *_1 \phi'_2) \tag*{\text{(by independence generator)}}
\end{align*}
$$

We can now conclude that the exchange law for 3-cells holds:

**Lemma B.2.** Given $F_i: \phi_i \Rightarrow \phi'_i \in \bar{\mathbb{P}}_3$ for $i \in \{1,2\}$ such that $F_1, F_2$ are 1-composable, we have, in $\bar{\mathbb{P}}_3$,

$$ (F_1 *_1 \phi_2) *_2 (\phi'_1 *_1 F_2) = (\phi_1 *_1 F_2) *_2 (F_1 *_1 \phi'_2). $$

*Proof.* As an element of $\bar{\mathbb{P}}_3$, $F_i$ can be written $F_i = R_{i,1} *_2 \cdots *_2 R_{i,k_i}$ where

$$ R_{i,j} = \lambda_{i,j} *_1 (l_{i,j} *_0 A_{i,j} *_0 r_{i,j}) *_1 \rho_{i,j} $$

for some $k_i \in \mathbb{N}$, $\lambda_{i,j}, \rho_{i,j} \in \bar{\mathbb{P}}_2$, $l_{i,j}, r_{i,j} \in \bar{\mathbb{P}}_1$, $A_{i,j} \in \mathbb{P}_3$ for $1 \le j \le k_i$, for $i \in \{1,2\}$. Note that

$$ F_1 *_1 \phi_2 = (R_{1,1} *_1 \phi_2) *_2 \cdots *_2 (R_{1,k_1} *_1 \phi_2) $$

and

$$ \phi'_1 *_1 F_2 = (\phi'_1 *_1 R_{2,1}) *_2 \cdots *_2 (\phi'_1 *_1 R_{2,k_2}). $$

Then, by using Lemma B.1 $k_1 k_2$ times as expected to reorder the $R_{1,j_1}$'s after the $R_{2,j_2}$'s for $1 \le j_i \le k_i$ for $i \in \{1,2\}$, we obtain that

$$ (F_1 *_1 \phi_2) *_2 (\phi'_1 *_1 F_2) = (\phi_1 *_1 F_2) *_2 (F_1 *_1 \phi'_2). \quad \square $$

We now prove the various conditions on $X_{-,\cdot}$. First, a technical lemma:

**Proposition B.3.** Given $f \in \mathbb{P}_1^*$, $\phi, \psi \in \mathbb{P}_2^*$ with $f, \phi, \psi$ 0-composable, there is a canonical isomorphism $(f *_0 \phi) \sqcup \psi \cong \phi \sqcup \psi$ and for all $p \in (\phi \sqcup \psi)^*_1$, we have

$$ [p]_{f*_0 \phi, \psi} = f *_0 [p]_{\phi, \psi} $$

Similarly, given $\phi, \psi \in \mathbb{P}_2^*$ and $h \in \mathbb{P}_1^*$ with $\phi, \psi, h$ 0-composable, we have a canonical isomorphism $\phi \sqcup (\psi *_0 h) \cong \phi \sqcup \psi$ and for all $p \in (\phi \sqcup (\psi *_0 h))^*_1$, we have

$$ [p]_{\phi, \psi *_0 h} = [p]_{\phi, \psi} *_0 h. $$

Finally, given $\phi, \psi \in \mathbb{P}_2^*$ and $g \in \mathbb{P}_1^*$ with $\phi, g, \psi$ 0-composable, we have a canonical isomorphism $(\phi *_0 g) \sqcup \psi \cong \phi \sqcup (g *_0 \psi)$ and for all $p \in ((\phi *_0 g) \sqcup \psi)^*_1$, we have

$$ [p]_{\phi *_0 g, \psi} = [p]_{\phi, g *_0 \psi}. $$
Proof. Let $f \in \mathbb{P}_1^*$, $\phi, \psi \in \mathbb{P}_2^*$ with $f, \phi, \psi$ 0-composable and let $r, s \ge 0$, $f_i, g_i \in \mathbb{P}_1^*$, $\alpha_i \in \mathbb{P}_2$ for $i \in \{1, \dots, r\}$ and $f'_j, g'_j \in \mathbb{P}_1^*$, $\alpha'_j \in \mathbb{P}_2$ for $j \in \{1, \dots, s\}$ such that

$$ \phi = (f_1 *_0 \alpha_1 *_0 g_1) *_1 \cdots *_1 (f_r *_0 \alpha_r *_0 g_r) $$

and

$$ \psi = (f'_1 *_0 \alpha'_1 *_0 g'_1) *_1 \cdots *_1 (f'_r *_0 \alpha'_r *_0 g'_r). $$

By contemplating the definitions of $(f*_0 \phi) \sqcup \psi$ and $\phi \sqcup \psi$, we deduce a canonical isomorphism between them. Under this isomorphism, we easily verify that we have $[w]_{f*_0\phi,\psi} = f*_0[w]_{\phi,\psi}$ for $w \in ((f*_0 \phi) \sqcup \psi)_0$. Now, given $u_l, r_j, v \in ((f*_0 \phi) \sqcup \psi)_0$, we have

$$ \begin{aligned} [X_{u,v}]_{f*_0\phi,\psi} &= [u]_{f*_0\phi,\psi} *_1 (f*_0 f_i *_0 X_{\alpha_i, g_i*_0 f_j, \alpha'_j *_0 g_j}) *_1 [v]_{f*_0\phi,\psi} \\ &= f*_0 ([u]_{\phi,\psi} *_1 (f_i*_0 X_{\alpha_i, g_i*_0 f_j, \alpha'_j *_0 g_j}) *_1 [v]_{\phi,\psi}) \\ &= f*_0 [X_{u,v}]_{\phi,\psi}. \end{aligned} $$

By functoriality of $[-]_{f*_0\phi,\psi}$ and $[-]_{\phi,\psi}$, we deduce that, for all $p \in (f*_0 \phi) \sqcup \psi^*$,

$$ [p]_{f*_0\phi,\psi} = f*_0[p]_{\phi,\psi}. $$

The two other properties are shown similarly.

□

We can now conclude the most simple properties of $X_{-, -}$:

**Lemma B.4.** Given $\phi: f \Rightarrow f' \in \bar{\mathbb{P}}_2$ and $\psi: g \Rightarrow g' \in \bar{\mathbb{P}}_2$, we have the following equalities in $\bar{\mathbb{P}}_3$:

(i) $X_{\mathrm{id}_f, \psi} = \mathrm{id}_{f*_0 \psi}$ and $X_{\phi, \mathrm{id}_g} = \mathrm{id}_{\phi*_0 g}$ when $\phi, \psi$ are 0-composable,

(ii) $X_{l*_0 \phi, \psi} = l*_0 X_{\phi, \psi}$ for $l \in \mathbb{P}_1^*$ such that $l, \phi, \psi$ are 0-composable,

(iii) $X_{\phi*_0 m, \psi} = X_{\phi, m*_0 \psi}$ for $m \in \mathbb{P}_1^*$ such that $\phi, m, \psi$ are 0-composable,

(iv) $X_{\phi, \psi*_0 r} = X_{\phi, \psi} *_0 r$ for $r \in \mathbb{P}_1^*$ such that $\phi, \psi, r$ are 0-composable.

**Proof.** (i) is clear, since both $X_{\mathrm{id}_f, \psi}$ and $X_{\phi, \mathrm{id}_g}$ are identity paths on the unique 0-cells of $(\mathrm{id}_f \sqcup \psi)^*$ and $(\phi \sqcup \mathrm{id}_g)^*$ respectively. (ii) is a consequence of Proposition B.3, since $X_{f*_0\phi,\psi}$ is sent to $X_{\phi,\psi}$ by the canonical isomorphism $(f*_0 \phi) \sqcup \psi \cong \phi \sqcup \psi$. (iii) and (iv) follow similarly. □

The last required properties on $X_{-, -}$ are more difficult to prove. In fact, we need a proper coherence theorem showing that, for 0-composable $\phi, \psi \in \bar{\mathbb{P}}_2$, $X_{\phi, \psi} = [p]_{\phi, \psi}$ for all $p \in (\phi \sqcup \psi)^*_1$ parallel to $X_{\phi, \psi}$. We progressively introduce the necessary material to prove this fact below.

Given a word $w \in (\phi \sqcup \psi)_0$, there is a function

$$ \mathrm{l-index}_w: \{1, \dots, |\phi|\} \to \{1, \dots, |\phi| + |\psi|\} $$

defined such that, for $i \in \{1, \dots, |\phi|\}$, if $w = w'l_i w''$, then $\mathrm{l-index}_w(i) = |w'| + 1$. We have that the function $\mathrm{l-index}$ characterizes the existence of path in $(\phi \sqcup \psi)^*$, as in:

**Lemma B.5.** Given 0-composable $\phi, \psi \in \mathbb{P}_2^*$ and $w, w' \in (\phi \sqcup \psi)_0$, there is a path

$$ p: w \to w' \in (\phi \sqcup \psi)^*_1 $$

if and only if $\mathrm{l-index}_w(i) \le \mathrm{l-index}_{w'}(i)$ for $1 \le i \le |\phi|$.

**Proof.** Given $X_{u,v}: \mathrm{ul}_r r_s v \to \mathrm{ur}_s l_r v \in (\phi \sqcup \psi)_1$, it is clear that $\mathrm{l-index}_{\mathrm{ul}_r r_s v}(i) \le \mathrm{l-index}_{\mathrm{ur}_s l_r v}(i)$ for all $1 \le i \le |\phi|$, so that, given a path $p: w \to w' \in (\phi \sqcup \psi)^*_1$, by induction on $p$, we have $\mathrm{l-index}_w(i) \le \mathrm{l-index}_{w'}(i)$ for $1 \le i \le |\phi|$.

Conversely, given $w, w' \in (\phi \sqcup \psi)_0$ such that $\mathrm{l-index}_w \le \mathrm{l-index}_{w'}$, we show by induction on $N(w, w')$ defined by

$$ N(w, w') = \sum_{1 \le i \le |\phi|} \mathrm{l-index}_{w'}(i) - \mathrm{l-index}_w(i) $$
that there is a path $p: w \to w' \in (\phi \sqcup \psi)_1^*$. If $N(w, w') = 0$, then $w = w'$ and $1_w: w \to w'$ is a suitable path. Otherwise, let $i_{\max}$ be the largest $i \le |\phi|$ such that $\text{l-index}_{w'}(i) > \text{l-index}_w(i)$. Then, either $i_{\max} = |\phi|$ or $\text{l-index}_w(i_{\max}) + 1 < \text{l-index}_w(i_{\max} + 1)$ since

$$ 
\begin{aligned}
\text{l-index}_w(i_{\max}) + 1 &\le \text{l-index}_{w'}(i_{\max}) \\
&< \text{l-index}_{w'}(i_{\max} + 1) \\
&= \text{l-index}_w(i_{\max} + 1)
\end{aligned}
$$

So we can write $w = u_1 i_{\max} r_j v$ for some words $u, v$ and $j \in \{1, \dots, |\psi|\}$. We have a path generator $X_{u,v}: w \to \tilde{w} \in (\phi \sqcup \psi)_1$ where $\tilde{w} = u_1 r_j i_{\max} v$. Then,

$$ \text{l-index}_{\tilde{w}}(i) = \begin{cases} \text{l-index}_w(i) & \text{if } i \neq i_{\max} \\ \text{l-index}_w(i_{\max}) + 1 & \text{if } i = i_{\max} \end{cases} $$

so $\text{l-index} \tilde{w} \le \text{l-index} w'$ and $N(\tilde{w}, w') < N(w, w')$. Thus, by induction, we get

$$ p': \tilde{w} \to w' \in (\phi \sqcup \psi)_1^* $$

and we build a path $X_{u,v} *_0 p'$: $w \to w' \in (\phi \sqcup \psi)_1^*$ as wanted. $\square$

Given 0-composable $\phi, \psi \in P_2^*$ and $w = w_1 \dots w_{|\phi|+|\psi|} \in (\phi \sqcup \psi)_0$, we define $\text{Inv}(w)$ as

$$ \text{Inv}(w) = |\{(i, j) \mid 1 \le i < j \le |\phi| + |\psi| \text{ and } w_i = r_{i'} \text{ and } w_j = l_{j'} \text{ for some } i' \in \{1, \dots, |\psi|\} \text{ and } j' \in \{1, \dots, |\phi|\}\}| $$

We have that $\text{Inv}$ characterizes the length of the paths of $(\phi \sqcup \psi)^*$, as in:

**Lemma B.6.** Given 0-composable $\phi, \psi \in P_2^*$ and $p: w \to w' \in (\phi \sqcup \psi)_1^*$, we have

$$ |p| = \text{Inv}(w') - \text{Inv}(w). $$

In particular, given $w, w' \in (\phi \sqcup \psi)_0$, all the paths $p: w \to w' \in (\phi \sqcup \psi)_1^*$ have the same length.

*Proof.* We show this by induction on the length of $p$. If $p = \text{id}_w$, then the conclusion holds. Otherwise, $p = X_{u,u'} *_0 r$ for some $u, u' \in \Sigma_{\phi,\psi}$ and $r: \tilde{w} \to w' \in (\phi \sqcup \psi)_1^*$. Then, by induction hypothesis, $|r| = \text{Inv}(w') - \text{Inv}(\tilde{w})$. Note that, by the definition of $X_{u,u'}$, $w = u_1 r_j u'$ and $\tilde{w} = u_1 r_j l_i r$ for some $i \in \{1, \dots, |\phi|\}$ and $j \in \{1, \dots, |\psi|\}$. Hence,

$$ |p| = |r| + 1 = \text{Inv}(w') - \text{Inv}(\tilde{w}) + \text{Inv}(\tilde{w}) - \text{Inv}(w) = \text{Inv}(w') - \text{Inv}(w). \quad \square $$

Given 0-composable $\phi, \psi \in P_2^*$, we now prove the following coherence property for $(\phi \sqcup \psi)^*$:

**Lemma B.7.** Let $\approx$ be a congruence on $(\phi \sqcup \psi)^*$. Suppose that, for all words $u_1, u_2, u_3 \in \Sigma_{\phi,\psi}$, $i, i' \in \{1, \dots, |\phi|\}$ and $j, j' \in \{1, \dots, |\psi|\}$ such that $u_1 l_i r_j u_2 l_{i'} r_{j'} u_3 \in (\phi \sqcup \psi)_0$, we have

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

then, for all $p_1, p_2: v \to w \in (\phi \sqcup \psi)_1^*$, we have $p_1 \approx p_2$.

*Proof.* We prove this by induction on $|p_1|$. By Lemma B.6, we have $|p_1| = |p_2|$. In particular, if $p_1 = \text{id}_v$, then $p_2 = \text{id}_v$. Otherwise, $p_i = q_i *_0 r_i$ with $q_i: v \to v_i$ and $r_i: v_i \to w$ and $|q_i| = 1$ for $i \in \{1, 2\}$. If $q_1 = q_2$, then we conclude with the induction hypothesis on $r_1$ and $r_2$. Otherwise,
up to symmetry, we have $q_1 = X_{u_1, u_2 l_i r_j u_3}$ and $q_2 = X_{u_1 l_i r_j u_2, u_3}$ for some $u_1, u_2, u_3 \in \Sigma_{\phi, \psi}^*$, $i, i' \in \{1, \dots, |\phi|\}$ and $j, j' \in \{1, \dots, |\psi|\}$. Let

$$q'_1 = X_{u_1 r_j l_i u_2, u_3}, \qquad q'_2 = X_{u_1, u_2 r_j l_i' u_3}, \qquad v' = u_1 r_j l_i u_2 r_j l_i' u_3.$$

Since we have a path $v \xrightarrow{q_1} v_1 \xrightarrow{r_1} w$, by Lemma B.5, we have $l\text{-index}_v(s) \le l\text{-index}_w(s)$ for $s \in \{1, \dots, |\phi|\}$. Moreover,

$$l\text{-index}_v(i) < l\text{-index}_{v_1}(i) \le l\text{-index}_w(i) \quad \text{and} \quad l\text{-index}_v(i') < l\text{-index}_{v_2}(i') \le l\text{-index}_w(i').$$

Also, for $s \in \{1, \dots, |\phi|\}$,

$$l\text{-index}_{v'}(s) = \begin{cases} l\text{-index}_v(s) + 1 & \text{if } s \in \{i, i'\}, \\ l\text{-index}_v(s) & \text{otherwise.} \end{cases}$$

From the preceding properties, we deduce that $l\text{-index}_{v'}(s) \le l\text{-index}_w(s)$ for $s \in \{1, \dots, |\phi|\}$. Thus, by Lemma B.5, there is a path $r'$: $v' \to w \in (\phi \sqcup \psi)_1^*$ as in

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

Since $|r_i| = |p_i| - 1$ for $i \in \{1, 2\}$, by induction hypothesis, we have $r_i \approx q'_i *_0 r'$ for $i \in \{1, 2\}$, which can be extended to $q_i *_0 r_i \approx q_i *'_0 q'_i *'_0 r'$, since $\approx$ is a congruence. By hypothesis, we have $q_1 *'_0 q'_1 \approx q_2 *'_0 q'_2$, which can be extended to $q_1 *'_0 q'_1 *'_0 r' \approx q_2 *'_0 q'_2 *'_0 r'$. By transitivity of $\approx$, we get that $q_1 *'_0 r_1 \approx q_2 *'_0 r_2$, that is, $p_1 \approx p_2$. $\square$

We then apply this coherence property to $[-]_{-,-}$ and get that “all exchange methods are equivalent”, as in:

**Proposition B.8.** Given 0-composable $\phi, \psi \in \bar{P}_2$, for all $p_1, p_2$: $u \to v \in (\phi \sqcup \psi)_1^*$, we have, in $\bar{P}_3$,

$$[p_1]_{\phi, \psi} = [p_2]_{\phi, \psi}.$$

*Proof.* By Lemma B.2, for all words $u_1, u_2, u_3 \in \Sigma_{\phi, \psi}$, $i, i' \in \{1, \dots, |\phi|\}$ and $j, j' \in \{1, \dots, |\psi|\}$ such that $u_1 l_i r_j u_2 l_i' r_j' u_3 \in (\phi \sqcup \psi)_0$, we have

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

Moreover, the relation $\approx$ defined on parallel $p_1, p_2 \in (\phi \sqcup \psi)_1^*$ by $p_1 \approx p_2$ when $[p_1]_{\phi, \psi} = [p_2]_{\phi, \psi}$ is clearly a congruence. Hence, by Lemma B.7, we have that $[p_1]_{\phi, \psi} = [p_2]_{\phi, \psi}$ for all parallel $p_1, p_2 \in (\phi \sqcup \psi)_1^*$. $\square$

The preceding property says in particular that $X_{\phi, \psi} = [p]_{\phi, \psi}$ for all 0-composable $\phi, \psi \in \bar{P}_2^*$ and paths $p \in (\phi \sqcup \psi)_1^*$ parallel to $X_{\phi, \psi}$.

Let $\phi, \psi \in \bar{P}_2^*$ be 0-composable 2-cells, and $\phi', \psi' \in \bar{P}_2^*$ be 0-composable 2-cells such that $\phi, \phi'$ and $\psi, \psi'$ are 1-composable. To obtain the last required properties on $X_{-,-}$, we need to relate $\phi \sqcup \psi$ and $\phi' \sqcup \psi'$ to $(\phi *'_1 \phi') \sqcup (\psi *'_1 \psi')$. Given $w \in (\phi \sqcup \psi)_0$, there is a functor

$$w(-): (\phi' \sqcup \psi')^* \to ((\phi *'_1 \phi') \sqcup (\psi *'_1 \psi'))^*$$
which is uniquely defined by the mappings

$$u \mapsto w\uparrow(u)$$
$$X_{u_1, u_2} \mapsto X_{w\uparrow(u_1), \uparrow(u_2)}$$

for $u \in (\phi' \sqcup \psi')_0$ and $X_{u_1, u_2} \in (\phi' \sqcup \psi')_1$ and where, for $v = v_1 \dots v_k \in \Sigma^*_{\phi', \psi'}$, $\uparrow(v) \in \Sigma^*_{\phi_*1 \phi', \psi_*1 \psi'}$ is defined by

$$\uparrow(v)_r = \begin{cases} l_{|\phi|+i} & \text{if } v_r = l_i \text{ for some } i \in \{1, \dots, |\phi'|\} \\ r_{|\psi|+j} & \text{if } v_r = r_j \text{ for some } j \in \{1, \dots, |\psi'|\} \end{cases}$$

for $r \in \{1, \dots, k\}$. Similarly, given $w \in (\phi' \sqcup \psi')_0$, there is a functor

$$(-) \cdot w: (\phi \sqcup \psi)^* \to ((\phi_*1 \phi') \sqcup (\psi_*1 \psi'))^*$$

which is uniquely defined by the mappings

$$u \mapsto u\uparrow(w)$$
$$X_{u_1, u_2} \mapsto X_{u_1, u_2\uparrow(w)}$$

for $u \in (\phi \sqcup \psi)_0$ and $X_{u_1, u_2} \in (\phi \sqcup \psi)_1$ and where $\uparrow(-)$ is defined as above.

The functors $w \cdot (-)$ and $(-) \cdot w$ satisfy the following compatibility property:

**Lemma B.9.** Let $\phi, \psi \in \mathbb{P}_2^*$ be 0-composable 2-cells, and $\phi', \psi' \in \mathbb{P}_2^*$ be 0-composable 2-cells such that $\phi, \phi'$ and $\psi, \psi'$ are 1-composable. Given $w \in (\phi \sqcup \psi)_0$, we have the following equalities in $\mathbb{P}_3^*$:

$$(i) \quad [w \cdot (u)]_{\phi_*1 \phi', \psi_*1 \psi'} = [w]_{\phi, \psi} *_1 [u]_{\phi', \psi'} \quad \text{for } u \in (\phi' \sqcup \psi')_0,$$

$$(ii) \quad [w \cdot (p)]_{\phi_*1 \phi', \psi_*1 \psi'} = [w]_{\phi, \psi} *_1 [p]_{\phi', \psi'} \quad \text{for } p \in (\phi' \sqcup \psi')_1^*.$$

Similarly, given $w \in (\phi' \sqcup \psi')_0$, we have:

$$(i) \quad [(u) \cdot w]_{\phi_*1 \phi', \psi_*1 \psi'} = [u]_{\phi, \psi} *_1 [w]_{\phi', \psi'} \quad \text{for } u \in (\phi \sqcup \psi)_0,$$

$$(ii) \quad [(p) \cdot w]_{\phi_*1 \phi', \psi_*1 \psi'} = [p]_{\phi, \psi} *_1 [w]_{\phi', \psi'} \quad \text{for } p \in (\phi \sqcup \psi)_1^*.$$

**Proof.** We only prove the first part, since the second part is similar. We start by (i). We have $[w \cdot (u)]_{\phi_*1 \phi', \psi_*1 \psi'} = [w \uparrow(u)]_{\phi_*1 \phi', \psi_*1 \psi'}^{1,1}$. By a simple induction on $w$, we obtain

$$[w \uparrow(u)]_{\phi_*1 \phi', \psi_*1 \psi'}^{1,1} = [w]_{\phi_*1 \phi', \psi_*1 \psi'}^{1,1} *_1 [\uparrow(u)]_{\phi_*1 \phi', \psi_*1 \psi'}^{\phi', |\psi|}$$

and, by other simple inductions on $w$ and $u$, we get

$$[w]_{\phi_*1 \phi', \psi_*1 \psi'}^{1,1} = [w]_{\phi, \psi}^{1,1} = [w]_{\phi, \psi}$$

$$[\uparrow(u)]_{\phi_*1 \phi', \psi_*1 \psi'}^{\phi', |\psi|} = [u]_{\phi', \psi'}^{1,1} = [u]_{\phi, \psi}$$

so that (i) holds.

For (ii), by induction on $p$, it is sufficient to prove the equality for $p = X_{u_1, u_2} \in (\phi \sqcup \psi)_1$. Let $m = |\phi|, n = |\psi|$, and

$$(e_1 *_0 \alpha_1 *_0 f_1) *_1 \cdots *_1 (e_m *_0 \alpha_m *_0 f_m)$$

$$(g_1 *_0 \beta_1 *_0 h_1) *_1 \cdots *_1 (g_m *_0 \beta_m *_0 h_m)$$

be the unique decomposition of $\phi$ and $\psi$ respectively, for some $e_i, f_i, g_j, h_j \in \mathbb{P}_1^*$ and $\alpha_i, \beta_j \in \mathbb{P}_2$ for $i \in \{1, \dots, m\}$ and $j \in \{1, \dots, n\}$. We then have

$$[w \cdot (X_{u_1, u_2})]_{\phi_*1 \phi', \psi_*1 \psi'} = [X_{w\uparrow(u_1), \uparrow(u_2)}]_{\phi_*1 \phi', \psi_*1 \psi'}$$

$$= [w \uparrow(u_1)]_{\phi_*1 \phi', \psi_*1 \psi'}^{1,1} *_1 (e_i *_0 X_{\alpha_i, f_i *_0 g_j, \beta_j *_0 h_j}) *_1 [\uparrow(u_2)]_{\phi_*1 \phi', \psi_*1 \psi'}^{k_l, k_r}$$

where $i, j$ are such that $u_1 l_i r_j u_2 \in (\phi' \sqcup \psi')_0$ and

$$k_l = |\phi| + i + 1$$

$$k_r = |\psi| + j + 1.$$
By simple inductions, we obtain

$$
\begin{align*}
[w\uparrow(u_1)]_{\phi_*1\phi',\psi_*1\psi'}^{1,1} &= [w]_{\phi_*1\phi',\psi_*1\psi'}^{1,1} *_1 [\uparrow(u_1)]_{\phi_*1\phi',\psi_*1\psi'}^{\vert\phi\vert,\vert\psi\vert} \\
&= [w]_{\phi,\psi}^{1,1} *_1 [u_1]_{\phi',\psi'}^{1,1} \\
&= [w]_{\phi,\psi} *_1 [u_1]_{\phi',\psi'}^{1,1}
\end{align*}
$$

and

$$
[\uparrow(u_2)]_{\phi_*1\phi',\psi_*1\psi'}^{k_1,k_r} = [u_2]_{\phi',\psi'}^{i+1,j+1}
$$

so that

$$
\begin{align*}
[w \cdot (X_{u_1, u_2})]_{\phi_*1 \phi', \psi_*1 \psi'} &= [w]_{\phi, \psi} *_1 [u_1]_{\phi', \psi'}^{1,1} *_1 (e_i *_0 X_{\alpha_i, f_i *_0 g_j, \beta_j} *_0 h_j) *_1 [u_2]_{\phi', \psi'}^{i+1, j+1} \\
&= [w]_{\phi, \psi} *_1 [X_{u_1, u_2}]_{\phi', \psi'}.
\end{align*}
\hfill $\square$
$$

We can now conclude the last required properties on $X_{-, -}$:

**Lemma B.10.** Given 1-composable $\phi, \phi' \in \bar{\mathbb{P}}_2$, 1-composable $\psi, \psi' \in \bar{\mathbb{P}}_2$ such that $\phi, \psi$ are 0-composable, we have the following equalities in $\bar{\mathbb{P}}_3$:

$$
X_{\phi_*1\phi',\psi} = ((\phi *_0 \partial_1^-(\psi)) *_1 X_{\phi',\psi}) *_2 (X_{\phi,\psi} *_1 (\phi' *_0 \partial_1^+(\psi)))
$$

and

$$
X_{\phi, \psi_*1\psi'} = (X_{\phi, \psi} *_1 (\partial_1^+(\phi) *_0 \psi')) *_2 ((\partial_1^-(\phi) *_0 \psi) *_1 X_{\phi, \psi'}).
$$

Proof. We only prove the first equality, since the second one is similar. By definition of $X_{\phi_*1\phi',\psi}$, we have $X_{\phi_*1\phi',\psi} = [X_{\phi_*1\phi',\psi}]_{\phi_*1\phi',\psi}$. Moreover, by Proposition B.8, $[X_{\phi_*1\phi',\psi}]_{\phi_*1\phi',\psi} = [p]_{\phi_*1\phi',\psi}$ in $\bar{\mathbb{P}}_3$ for all path $p \in ((\phi *_1 \phi') \sqcup \psi)_1$ parallel to $X_{\phi_*1\phi',\psi}$. In particular,

$$
[\mathbf{X}_{\phi_*1\phi',\psi}]_{\phi_*1\phi',\psi} = [(w \cdot (\mathbf{X}_{\phi',\psi})) *_0 ((\mathbf{X}_{\phi,\psi}) \cdot w')]_{\phi_*1\phi',\psi}
$$

where

$w = l_1 \dots l_{|\phi|}$

$w' = l_1 \dots |_{\phi'}$

are the only 0-cells of $\phi' \sqcup \text{id}_{\partial_-(\phi)}$ and $\phi \sqcup \text{id}_{\partial_+(\psi)}$ respectively. Thus,

$$
\begin{align*}
[\mathbf{X}_{\phi_*1\phi',\psi}]_{\phi_*1\phi',\psi} &= [(w \cdot (\mathbf{X}_{\phi',\psi})) *_0 ((\mathbf{X}_{\phi,\psi}) \cdot w')]_{\phi_*1\phi',\psi} \\
&= [(w \cdot (\mathbf{X}_{\phi',\psi}))]_{\phi_*1\phi',\psi} *_2 [((\mathbf{X}_{\phi,\psi}) \cdot w')]_{\phi_*1\phi',\psi} \tag*{(by functoriality of $[-]_{\phi_*1\phi',\psi}$)} \\
&= ([w]_{\phi,\text{id}_{\partial_-(\psi)}} *_1 [\mathbf{X}_{\phi',\psi}]_{\phi',\psi}) *_2 ([\mathbf{X}_{\phi,\psi}]_{\phi,\psi} *_1 [w']_{\phi',\text{id}_{\partial_+(\psi)}}) \tag*{(by Lemma B.9)} \\
&= ((\phi *_0 \partial_1^-(\psi)) *_1 X_{\phi',\psi}) *_2 (X_{\phi,\psi} *_1 (\phi' *_0 \partial_1^+(\psi))) \tag*{(by definition of $[-]_{-, -}$ and $X_{-, -}$).}
\end{align*}
$$

Hence,

$$
X_{\phi_*1\phi',\psi} = ((\phi *_0 \partial_1^-(\psi)) *_1 X_{\phi',\psi}) *_2 (X_{\phi,\psi} *_1 (\phi' *_0 \partial_1^+(\psi)). \quad \square
$$

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

We now prove the compatibility between 3-cells and interchangers. We start by proving the compatibility with 3-generators:

**Lemma B.11.** Given $A: \phi \Rightarrow \phi': f \Rightarrow f' \in \mathbb{P}_3$ and $\psi: g \Rightarrow g' \in \bar{\mathbb{P}}_2$ such that $A, \psi$ are 0-composable, we have, in $\bar{\mathbb{P}}_3$,

$$
((A *_0 g) *_1 (f' *_0 \psi)) *_2 X_{\phi', \psi} = X_{\phi, \psi} *_2 ((f *_0 \psi) *_1 (A *_0 g)).
$$

Similarly, given $\phi: f \Rightarrow f' \in \bar{\mathbb{P}}_2$ and $B: \psi \Rightarrow \psi': g \Rightarrow g'$ such that $\phi, B$ are 0-composable, we have, in $\bar{\mathbb{P}}$,

$$
X_{\phi, \psi} *_2 ((g *_0 B) *_1 (\phi *_0 f')) = ((\phi *_0 g) *_1 (f *_0 B)) *_2 X_{\phi, \psi'}.
$$
*Proof.* We only prove the first part of the property, since the other one is symmetric, and we do so by an induction on $|\psi|$. If $|\psi| = 0$, $\psi$ is an identity and the result follows. Otherwise, $\tilde{\psi} = w *_1 \tilde{\tilde{\psi}}$ where $w = (l*_0 \alpha*_0 r)$ with $l, r \in \bar{P}_1$, $\alpha: h \Rightarrow h' \in \bar{P}_2$ and $\tilde{\tilde{\psi}} \in \bar{P}_2$ with $|\tilde{\tilde{\psi}}| = |\psi| - 1$. Let $\tilde{g} = \partial_1^+(w)$. By Lemma B.10, we have

$$X_{\phi, \psi} = (X_{\phi, w} *_1 (f' *_0 \tilde{\psi})) *_2 ((f *_0 w) *_1 X_{\phi, \tilde{\psi}}) \quad (11)$$

$$X_{\phi', \psi} = (X_{\phi', w} *_1 (f' *_0 \tilde{\psi})) *_2 ((f *_0 w) *_1 X_{\phi', \tilde{\psi}}). \quad (12)$$

Also, by Lemma B.4(iv), we have

$$X_{\phi,w} = X_{\phi,l*_0\alpha} *_0 r \qquad X_{\phi',w} = X_{\phi',l*_0\alpha} *_0 r \quad (13)$$

so that

$$((A*_0 g) *_1 (f' *_0 w)) *_2 X_{\phi',w} \\
= [((A*_0 l*_0 h) *_1 (f' *_0 l*_0 \alpha)) *_2 X_{\phi',l*_0\alpha}] *_0 r \\
= [X_{\phi,l*_0\alpha} *_2 ((f*_0 l*_0 \alpha) *_1 (A*_0 l*_0 h'))] *_0 r \quad (14)$$

(by interchange naturality generator)

$$= X_{\phi,w} *_2 ((f*_0 w) *_1 (A*_0 g')).$$

Thus,

$$((A*_0 g) *_1 (f' *_0 \psi)) *_2 X_{\phi',\psi} \\
= ((A*_0 g) *_1 (f' *_0 w) *_1 (f' *_0 \tilde{\psi})) \\
\qquad *_2 (X_{\phi',w} *_1 (f' *_0 \tilde{\psi})) *_2 ((f*_0 w) *_1 X_{\phi',\tilde{\psi}}) \quad (\text{by (12)})$$

$$= [(((A*_0 g) *_1 (f' *_0 w)) *_2 X_{\phi',w}) *_1 (f' *_0 \tilde{\psi})] \\
\qquad *_2 ((f*_0 w) *_1 X_{\phi',\tilde{\psi}}) \\
= [(X_{\phi,w} *_2 ((f*_0 w) *_1 (A*_0 \tilde{g}))) *_1 (f' *_0 \tilde{\psi})] \\
\qquad *_2 ((f*_0 w) *_1 X_{\phi',\tilde{\psi}}) \quad (\text{by (14)})$$

$$= (X_{\phi,w} *_1 (f' *_0 \tilde{\psi})) \\
\qquad *_2 ((f*_0 w) *_1 (A*_0 \tilde{g}) *_1 (f' *_0 \tilde{\psi})) *_2 ((f*_0 w) *_1 X_{\phi',\tilde{\psi}}) \\
= (X_{\phi,w} *_1 (f' *_0 \tilde{\psi})) \\
\qquad *_2 [(f*_0 w) *_1 (((A*_0 \tilde{g}) *_1 (f' *_0 \tilde{\psi})) *_2 X_{\phi',\tilde{\psi}})] \\
= (X_{\phi,w} *_1 (f' *_0 \tilde{\psi})) \\
\qquad *_2 [(f*_0 w) *_1 (X_{\phi',\tilde{\psi}} *_2 ((f*_0 \tilde{\psi}) *_1 (A*_0 g')))] \quad (\text{by induction})$$

$$= (X_{\phi,w} *_1 (f' *_0 \tilde{\psi})) *_2 ((f*_0 w) *_1 (X_{\phi',\tilde{\psi}})) \\
\qquad *_2 ((f*_0 w) *_1 (f*_0 \tilde{\psi}) *_1 (A*_0 g')) \\
= X_{\phi,\psi} *_2 ((f*_0 \psi) *_1 (A*_0 g')) \quad (\text{by (11)}). \quad \square$$

Next, we prove the compatibility between interchangers and rewriting steps:

**Lemma B.12.** Given a rewriting step $R: \phi \Rightarrow \phi'$: $f \Rightarrow f' \in \mathbb{P}_3^*$ with $R = \lambda *_1 (l*_0 A*_0 r) *_1 \rho$ for some $l, r \in \mathbb{P}_1^*$, $\lambda, \rho \in \mathbb{P}_2^*$, $A: \mu \Rightarrow \mu' \in \mathbb{P}_3$, and $\psi: g \Rightarrow g' \in \mathbb{P}_2^*$ such that $R, \psi$ are 0-composable, we have, in $\bar{\mathbb{P}}_3$,

$$((R*_0 g) *_1 (f' *_0 \psi)) *_2 X_{\phi', \psi} = X_{\phi, \psi} *_2 ((f*_0 \psi) *_1 (R*_0 g')). \quad (15)$$

Similarly, given $\phi \in \mathbb{P}_2^*$ and a rewriting step $S: \psi \Rightarrow \psi'$: $g \Rightarrow g' \in \mathbb{P}_3^*$ with $S = \lambda *_1 (l*_0 B*_0 r) *_1 \rho$ for some $\lambda, \rho \in \mathbb{P}_2^*$, $l, r \in \mathbb{P}_1^*$, $B: \nu \Rightarrow \nu' \in \mathbb{P}_3$ such that $\phi, S$ are 0-composable, we have, in $\bar{\mathbb{P}}_3$,

$$X_{\phi, \psi} *_2 ((f*_0 B) *_1 (\phi*_0 g')) = ((\phi*_0 g) *_1 (f'*_0 B)) *_2 X_{\phi, \psi'}.$$
Proof. By symmetry, we only prove the first part. Let

$$
\begin{align*}
\tilde{\mu} &= l *_0 \mu *_0 r & h &= \partial_1^- (\tilde{\mu}) & \tilde{h} &= \partial_1^- (\tilde{\mu}) \\
\tilde{\mu}' &= l *_0 \mu' *_0 r & h' &= \partial_1^+ (\mu') & \tilde{h}' &= \partial_1^+ (\tilde{\mu})
\end{align*}
$$

We have

$$
R *_0 g = (\lambda *_0 g) *_1 (l *_0 A *_0 r *_0 g) *_1 (\rho *_0 g)
$$

and, by Lemma B.10,

$$
\begin{equation} \tag{16}
\begin{split}
X_{\phi, \psi} = & (((\lambda *_1 \tilde{\mu}) *_0 g) *_1 X_{\rho, \psi}) \\
& *_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}, \psi} *_1 (\rho *_0 g')) \\
& \phantom{{}*_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}, \psi} *_1 (\rho *_0 g'))} ((X_{\lambda, \psi} *_1 ((\tilde{\mu} *_1 \rho) *_0 g')))
\end{split}
\end{equation}
$$

$$
\begin{equation}
\begin{split}
X_{\phi', \psi} = & (((\lambda *_1 \tilde{\mu}') *_0 g) *_1 X_{\rho, \psi}) \\
& *_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}', \psi} *_1 (\rho *_0 g')) \\
& \phantom{{}*_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}', \psi} *_1 (\rho *_0 g'))} ((X_{\lambda, \psi} *_1 ((\tilde{\mu}' *_1 \rho) *_0 g'))).
\end{split}
\tag{17}
\end{equation}
$$

We start the calculation of the left-hand side of (15), using (17). We get

$$
\begin{align*}
& ((R *_0 g) *_1 (f' *_0 \psi)) *_2 (((\lambda *_1 \tilde{\mu}') *_0 g) *_1 X_{\rho, \psi}) \\
&= (\lambda *_0 g) \\
& \quad *_1 [((l *_0 A *_0 r *_0 g) *_1 (\rho *_0 g) *_1 (f' *_0 \psi)) *_2 ((\mu' *_0 g) *_1 X_{\rho, \psi})] \\
&= (\lambda *_0 g) \\
& \quad *_1 [((\mu *_0 g) *_1 X_{\rho, \psi}) *_2 ((l *_0 A *_0 r *_0 g) *_1 (\tilde{h}' *_0 \psi) *_1 (\rho *_0 g'))] \quad \text{(by Lemma B.2)} \\
&= ((\lambda *_0 g) *_1 (\tilde{\mu} *_0 g) *_1 X_{\rho, \psi}) \\
& \quad *_2 ((\lambda *_0 g) *_1 (l *_0 A *_0 r *_0 g) *_1 (\tilde{h}' *_0 \psi) *_1 (\rho *_0 g')).
\end{align*}
$$

Symmetrically, we do a step of calculation for the right-hand side of (15), using (16). We get

$$
\begin{align*}
& (X_{\lambda, \psi} *_1 ((\tilde{\mu} *_1 \rho) *_0 g')) *_2 ((f *_0 \psi) *_1 (R *_0 g')) \\
&= ((\lambda *_0 g) *_1 (\tilde{h} *_0 \psi) *_1 (l *_0 A *_0 r *_0 g')) *_1 (\rho *_0 g') \\
& \quad *_2 (X_{\lambda, \psi} *_1 (\tilde{\mu}' *_0 g') *_1 (\rho *_0 g')).
\end{align*}
$$

Finally, we do the last step of calculation between the left-hand side and the right-hand side of (15).
Note that

$$
\begin{align*}
& ((l *_0 A *_0 r *_0 g) *_1 (\tilde{h}' *_0 \psi)) *_2 X_{\tilde{\mu}', \psi} \\
&= l *_0 (((A *_0 r *_0 g) *_1 (h' *_0 r *_0 \psi)) *_2 X_{\mu'*_0 r, \psi}) && \text{(by Lemma B.4(ii))} \\
&= l *_0 (((A *_0 r *_0 g) *_1 (h' *_0 r *_0 \psi)) *_2 X_{\mu', r*_0 \psi}) && \text{(by Lemma B.4(iii))} \\
&= l *_0 (X_{\mu, r*_0 \psi} *_2 ((h *_0 r *_0 \psi) *_1 (A *_0 r *_0 g))) && \text{(by Lemma B.11)} \\
&= l *_0 (X_{\mu*_0 r, \psi} *_2 ((h *_0 r *_0 \psi) *_1 (A *_0 r *_0 g))) && \text{(by Lemma B.4(iii))} \\
&= X_{\tilde{\mu}, \psi} *_2 ((\tilde{h} *_0 \psi) *_1 (l *_0 A *_0 r *_0 g')) && \text{(by Lemma B.4(ii))}
\end{align*}
$$

so that

$$
\begin{align*}
& ((\lambda *_0 g) *_1 (l *_0 A *_0 r *_0 g) *_1 (\tilde{h}' *_0 \psi) *_1 (\rho *_0 g')) *_2 ((\lambda *_0 g) *_1 X_{\tilde{\mu}', \psi} *_1 (\rho *_0 g')) \\
&= (\lambda *_0 g) *_1 [(l *_0 A *_0 r *_0 g) *_1 (\tilde{h}' *_0 \psi)) *_2 X_{\tilde{\mu}', \psi}] *_1 (\rho *_0 g') \\
&= (\lambda *_0 g) *_1 [X_{\tilde{\mu}, \psi} *_2 ((\tilde{h} *_0 \psi) *_1 (l *_0 A *_0 r *_0 g'))] *_1 (\rho *_0 g') \\
&= ((\lambda *_0 g) *_1 X_{\tilde{\mu}, \psi} *_1 (\rho *_0 g')) *_2 ((\lambda *_0 g) *_1 (\tilde{h} *_0 \psi) *_1 (l *_0 A *_0 r *_0 g') *_1 (\rho *_0 g')).
\end{align*}
$$

By combining the previous equations, we obtain

$$
((R *_0 g) *_1 (f' *_0 \psi)) *_2 X_{\phi', \psi}
$$
$$
\begin{align*}
&= ((\lambda *_0 g) *_1 (l *_0 A *_0 r *_0 g) *_1 (\rho *_0 g) *_1 (f' *_0 \psi)) \\
&\quad *_2 (((\lambda *_1 \tilde{\mu}') *_0 g) *_1 X_{\rho, \psi}) \\
&\quad *_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}', \psi} *_1 (\rho *_0 g')))) \\
&\quad *_2 ((X_{\lambda, \psi} *_1 ((\tilde{\mu}' *_1 \rho) *_0 g')))) \\
&= (((\lambda *_1 \tilde{\mu}) *_0 g) *_1 X_{\rho, \psi}) \\
&\quad *_2 (((\lambda *_0 g) *_1 X_{\tilde{\mu}, \psi} *_1 (\rho *_0 g')))) \\
&\quad *_2 ((X_{\lambda, \psi} *_1 ((\tilde{\mu} *_1 \rho) *_0 g')))) \\
&\quad *_2 ((f *_0 \psi) *_1 (\lambda *_0 g) *_1 (l *_0 A *_0 r *_0 g) *_1 (\rho *_0 g))) \\
&= X_{\phi, \psi} *_2 ((f *_0 \psi) *_1 (R *_0 g'))
\end{align*}
$$

which is what we wanted.

□

We can deduce the complete compatibility between interchangers and 3-cells:

**Lemma B.13.** Given $F: \phi \Rightarrow \phi': f \Rightarrow f' \in \bar{P}_3$ and $\psi: g \Rightarrow g' \in \bar{P}_2$ such that $F, \psi$ are 0-composable, we have

$$((F *_0 g) *_1 (f' *_0 \psi)) *_2 X_{\phi', \psi} = X_{\phi, \psi} *_2 ((f *_0 \psi) *_1 (F *_0 g')).$$

Similarly, given $\phi: f \Rightarrow f' \in \bar{P}_2$ and $G: \psi \Rightarrow \psi': g \Rightarrow g' \in \bar{P}_3$ such that $\phi, G$ are 0-composable, we have

$$X_{\phi, \psi} *_2 ((f *_0 G) *_1 (\phi *_0 g')) = ((\phi *_0 g) *_1 (f' *_0 G)) *_2 X_{\phi, \psi'}.$$

*Proof.* Remember that each 3-cell $\bar{P}$ can be written as a sequence of rewriting steps of $\bar{P}$. By induction on the length of such a sequence defining $F$ or $G$ as in the statement, we conclude using Lemma B.12. □

We can conclude that:

**Theorem 2.3.2.** Given a Gray presentation $\mathcal{P}$, the presented precategory $\bar{\mathcal{P}}$ is canonically a lax Gray category.

*Proof.* The axioms of lax Gray category follow from Lemma B.4, Lemma B.10, Lemma B.2 and Lemma B.13. □

# C Finiteness of critical branchings

In this section, we give a proof of Theorem 3.4.6, i.e., that Gray presentations, under some reasonable conditions, have a finite number of critical branchings. Our proof is constructive, so that we can extract a program to compute the critical branchings of such Gray presentations. First, we aim at showing that there is no critical branching $(S_1, S_2)$ of a Gray presentation $\mathcal{P}$ where both inner 3-generators of $S_1$ and $S_2$ are interchange generators. We begin with a technical lemma for minimal and independent branchings:

**Lemma C.1.** Given a minimal local branching $(S_1, S_2)$ of a Gray presentation $\mathcal{P}$, with

$$S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i$$

and $l_i, r_i \in \mathbb{P}_1^*$, $\lambda_i, \rho_i \in \mathbb{P}_2^*$, $A_i \in \mathbb{P}_3$ for $i \in \{1, 2\}$, the followings hold:

(i) either $\lambda_1$ or $\lambda_2$ is an identity,

(ii) either $\rho_1$ or $\rho_2$ is an identity,

(iii) $(S_1, S_2)$ is independent if and only if

$$|\partial_2^-(A_1)| + |\partial_2^-(A_2)| \le |\partial_2^-(S_1)| \quad \text{and} \quad |\lambda_1||\rho_1| = |\lambda_2||\rho_2| = 0.$$

If $(S_1, S_2)$ is moreover not independent:
(iv) either $l_1$ or $l_2$ is an identity,

(v) either $r_1$ or $r_2$ is an identity.

*Proof.* Suppose that neither $\lambda_1$ nor $\lambda_2$ are identities. Then, since

$$ \lambda_1 *_1 (l_1 *_0 \partial_2^- (A_1) *_0 r_1) *_1 \rho_1 = \lambda_2 *_1 (l_2 *_0 \partial_2^- (A_2) *_0 r_2) *_1 \rho_2, $$

we have $\lambda_i = w*_1 \lambda'_i$ for some $w \in P_2^*$ and $\lambda'_i \in P_2^*$ for $i \in \{1, 2\}$, such that $|w| \ge 1$, contradicting the minimality of $(S_1, S_2)$. So either $\lambda_1$ or $\lambda_2$ is an identity and similarly for $\rho_1$ and $\rho_2$, which concludes (i) and (ii).

By the definition of independent branching, the first implication of (iii) is trivial. For the converse, suppose that $(S_1, S_2)$ is such that

$$ |\partial_2^-(A_1)| + |\partial_2^-(A_2)| \le |\partial_2^-(S_1)| \quad \text{and} \quad |\lambda_1||\rho_1| = |\lambda_2||\rho_2| = 0. $$

We can suppose by symmetry that $\lambda_1$ is a unit. Since $|\partial_2^-(S_1)| = |\lambda_1| + |\partial_2^-(A_1)| + |\rho_1|$, we have that $|\partial_2^-(A_2)| \le |\rho_1|$.

If $|\rho_1| = 0$, then

$$ S_1 = l_1 *_0 A_1 *_0 r_1 \quad \text{and} \quad |\partial_2^-(A_2)| = 0, $$

thus, since $|\lambda_2||\rho_2| = 0$, we have

$$ \text{either } S_2 = \partial_2^-(S_1) *_1 (l_2 *_2 A_2 *_2 r_2) \text{ or } S_2 = (l_2 *_2 A_2 *_2 r_2) *_1 \partial_2^-(S_1). $$

In both cases, $(S_1, S_2)$ is independent.

Otherwise, $|\rho_1| > 0$ and, by (ii), we have $|\rho_2| = 0$ so that

$$ S_1 = (l_1 *_0 A_1 *_0 r_1) *_1 \rho_1 \quad \text{and} \quad S_2 = \lambda_2 *_1 (l_2 *_0 A_2 *_0 r_2). $$

Since $|\partial_2^-(A_2)| \le |\rho_1|$, we have $\rho_1 = \chi *_1 (l_2 *_0 \partial_2^-(A_2) *_0 r_2)$ for some $\chi \in P_2^*$ and, since $\partial_2^-(S_1) = \partial_2^-(S_2)$, we get

$$ (l_1 *_0 \partial_2^-(A_1) *_0 r_1) *_1 \chi *_1 (l_2 *_0 \partial_2^-(A_2) *_0 r_2) = \lambda_2 *_1 (l_2 *_0 \partial_2^-(A_2) *_0 r_2). $$

So $\lambda_2 = (l_1 *_0 \partial_2^-(A_1) *_0 r_1) *_1 \chi$ and hence $(S_1, S_2)$ is an independent branching, which concludes the proof of (iii).

Finally, suppose that $(S_1, S_2)$ is not independent. By (iii), it implies that

$$ \text{either } |\partial_2^-(A_1)| + |\partial_2^-(A_2)| > |\partial_2^-(S_1)| \quad \text{or} \quad |\lambda_1||\rho_1| > 0 \quad \text{or} \quad |\lambda_2||\rho_2| > 0. $$

If $|\lambda_1||\rho_1| > 0$, then $|\lambda_2| = |\rho_2| = 0$ by (i) and (ii), so that

$$ \lambda_1 *_1 (l_1 *_0 A_1 *_0 r_1) *_1 \rho_1 = l_2 *_0 A_2 *_0 r_2 $$

thus there exists $\lambda'_1, \rho'_1 \in P_2^*$ such that

$$ \lambda_1 = l_2 *_0 \lambda'_1 *_0 r_2 \quad \text{and} \quad \rho_1 = l_2 *_0 \rho'_1 *_0 r_2, $$

and we have

$$ l_2 *_0 \partial_1^+(\lambda'_1) *_0 r_2 = \partial_1^+(\lambda_1) = l_1 *_0 \partial_1^-(A_1) *_0 r_1. $$

Thus, $l_1$ and $l_2$ have the same prefix $l$ of size $k = \min(|l_1|, |l_2|)$ and we can write

$$ S_1 = l *_0 S'_1 $$

$$ S_2 = l *_0 S'_2 $$

for some rewriting steps $S_1, S_2 \in P_3^*$. Since $(S_1, S_2)$ is minimal, we have $k = 0$, so $|l_1||l_2| = 0$. We show similarly that $|r_1||r_2| = 0$. The case where $|\lambda_2||\rho_2| > 0$ is handled similarly.

So suppose that

$$ |\lambda_1||\rho_1| = 0 \quad \text{and} \quad |\lambda_2||\rho_2| = 0 \quad \text{and} \quad |\partial_1^-(A_1)| + |\partial_1^-(A_2)| > |\partial_2^-(S_1)|. \quad (18) $$
In particular, we get that $|\partial_2^-(A_i)| > 0$ for $i \in \{1, 2\}$. Let $u_i, v_i \in P_1^*$ and $\alpha_i \in P_2$ for $i \in \{1, \dots, r\}$ with $r = |\partial_2^-(S_1)|$ such that

$$ \partial_2^-(S_1) = (u_1 *_0 \alpha_1 *_0 v_1) *_1 \cdots *_1 (u_r *_0 \alpha_r *_0 v_r). $$

The condition last part of (18) implies that there is $i_0$ such that $l_1$ and $l_2$ are both prefix of $u_{i_0}$. So, $l_1$ and $l_2$ have the same prefix $l$ of length $k = \min(|l_1|, |l_2|)$.

Now, we prove that $\lambda_1 = l *_0 \lambda'_1$ for some $\lambda'_1 \in P_2^*$. If $|\lambda_1| = 0$, then

$$ \lambda_1 = l_1 *_0 \partial_1^-(S_1) *_0 r_1, $$

so $\lambda = l *_0 \lambda'_1$ for some $\lambda' \in P_2^*$. Otherwise, if $|\lambda_1| > 0$, since $|\lambda_1| |\rho_1| = 0$, we have $|\rho_1| = 0$ and, by (i), $|\lambda_2| = 0$. Also, by the last part of (18), we have $|\lambda_1| < |\partial_2^-(A_2)|$. Thus,

$$ \lambda_1 \text{ is a prefix of } l_2 *_0 \partial_2^-(A_2) *_0 r_2, $$

so $\lambda_1 = l *_0 \lambda'_1$ for some $\lambda_1 \in P_2^*$. Similarly, there are $\rho'_1, \lambda'_2, \rho'_2 \in P_2^*$ such that

$$ \rho_1 = l *_0 \rho'_1 \quad \text{and} \quad \lambda_2 = l *_0 \lambda'_2 \quad \text{and} \quad \rho_2 = l *_0 \lambda'_2. $$

Hence $S_1 = l *_0 S'_1$ and $S_2 = l *_0 S'_2$ for some rewriting steps $S'_1, S'_2 \in P_3^*$. Since $(S_1, S_2)$ is minimal, we have $|l_1| |l_2| = |l| = 0$, which proves (iv). The proof of (v) is similar. $\square$

We now have enough material to show that:

**Proposition C.2.** Given a Gray presentation P, there are no critical branching $(S_1, S_2)$ of P such that both the inner 3-generators of $S_1$ and $S_2$ are interchange generators.

*Proof.* Let $(S_1, S_2)$ be a local minimal branching such that, for $i \in \{1, 2\}$,

$$ S_i = \lambda_i *_1 (l_i *_0 X_{\alpha_i, g_i, \beta_i} *_0 r_i) *_1 \rho_i $$

for some $l_i, r_i, g_i \in P_1^*$, $\lambda_i, \rho_i \in P_2^*$ and $\alpha_i, \beta_i \in P_2$, and let $\phi$ be $\partial_2^-(S_1)$. Since $|\partial_2^-(X_{\alpha_1, g_1, \beta_1})| = 2$, we have $|\phi| \ge 2$.

If $|\phi| = 2$, then $|\lambda_i| = |\rho_i| = 0$ for $i \in \{1, 2\}$. Thus, since $\partial_2^-(S_1) = \partial_2^-(S_2)$, we get

$$ \begin{aligned} & (l_1 *_0 \alpha_1 *_0 g_1 *_0 \partial_1^-(\beta_1) *_0 r_1) *_1 (l_1 *_0 \partial_1^+(\alpha_1) *_0 g_1 *_0 \beta_1 *_0 r_1) \\ & = (l_2 *_0 \alpha_2 *_0 g_2 *_0 \partial_1^-(\beta_2) *_0 r_2) *_1 (l_2 *_0 \partial_1^+(\alpha_2) *_0 g_2 *_0 \beta_2 *_0 r_2). \end{aligned} $$

By the unique decomposition property given by Theorem 1.8.3, we obtain

$$ l_1 = l_2, \quad r_1 = r_2, \quad \alpha_1 = \alpha_2, \quad \beta_1 = \beta_2 \quad \text{and} \quad g_1 *_0 \partial_1^-(\beta_1) *_0 r_1 = g_2 *_0 \partial_1^-(\beta_2) *_0 r_2. $$

So $g_1 *_0 \partial_1^-(\beta_1) *_0 r_1 = g_2 *_0 \partial_1^-(\beta_1) *_0 r_1$, which implies that $g_1 = g_2$. Hence, $(S_1, S_2)$ is trivial.

If $|\phi| = 3$, then $|\lambda_i| + |\rho_i| = 1$ for $i \in \{1, 2\}$, and, by Lemma C.1,

$$ \text{either } |\rho_1| = |\lambda_2| = 1 \quad \text{or} \quad |\lambda_1| = |\rho_2| = 1. $$

By symmetry, we can suppose that $|\rho_1| = |\lambda_2| = 1$, which implies that $|\lambda_1| = |\rho_2| = 0$. By unique decomposition of whiskers, since $\partial_2^-(S_1) = \partial_2^-(S_2)$, we have

$$ \begin{aligned} & l_1 *_0 \alpha_1 *_0 g_1 *_0 \partial_1^-(\beta_1) *_0 r_1 = \lambda_2 \\ & l_1 *_0 \partial_1^+(\alpha_1) *_0 g_1 *_0 \beta_1 *_0 r_1 = l_2 *_0 \alpha_2 *_0 g_2 *_0 \partial_1^-(\beta_2) *_0 r_2 \\ & \rho_1 = l_2 *_0 \partial_1^+(\alpha_2) *_0 g_2 *_0 \beta_2 *_0 r_2 \end{aligned} $$

and the second line implies that $l_1 *_0 \partial_1^+(\alpha_1) *_0 g_1 = l_2$, $\beta_1 = \alpha_2$ and $r_1 = g_2 *_0 \partial_1^-(\beta_2) *_0 r_2$. Since $(S_1, S_2)$ is minimal, we have $|l_1| = |r_2| = 0$. So

$$ \begin{aligned} S_1 &= (X_{\alpha_1, g_1, \beta_1} *_0 g_2 *_0 \partial_1^-(\beta_2)) *_1 (\partial_1^+(X_{\alpha_1, g_1, \beta_1}) *_0 g_2 *_0 \beta_2) \\ S_2 &= (\alpha_1 *_0 g_1 *_0 \partial_1^-(\beta_1) *_0 g_2 *_0 \partial_1^-(\beta_2)) *_1 (\partial_1^+(\alpha_1) *_0 g_1 *_0 X_{\beta_1, g_2, \beta_2}) \end{aligned} $$
thus $(S_1, S_2)$ is a natural branching, hence not a critical one.

Finally, if $|\phi| \ge 4$, then, since $|\lambda_i| + |\rho_i| = |\phi| - 2 \ge 2$ for $i \in \{1, 2\}$, by Lemma C.1, we have that

$$ \text{either } |\lambda_1| = |\rho_2| = |\phi| - 2 \text{ or } |\rho_1| = |\lambda_2| = |\phi| - 2. $$

In either case,

$$ |\lambda_1||\rho_1| = |\lambda_2||\rho_2| = 0 \quad \text{and} \quad |\partial_2^-(X_{\alpha_1,g_1,\beta_1})| + |\partial_2^-(X_{\alpha_2,g_2,\beta_2})| = 4 \le |\phi| $$

so, by Lemma C.1(iii), $(S_1, S_2)$ is independent, hence not critical. □

Until the end of this section, we denote by $\mathbb{P}$ a Gray presentation such that $\mathbb{P}_2$ and $\mathbb{P}_3$ are finite and $|\partial_2^-(A)| > 0$ for every $A \in \mathbb{P}_3$, i.e., a Gray presentation satisfying the hypothesis of Theorem 3.4.6. The next result we prove is a characterization of independent branchings among minimal ones:

**Lemma C.3.** Given a minimal branching $(S_1, S_2)$ of $\mathbb{P}$ with

$$ S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i $$

for some $l_i, r_i \in \mathbb{P}_1^*$, $\lambda_i, \rho_i \in \mathbb{P}_2^*$ and $A_i \in \mathbb{P}_3$ for $i \in \{1, 2\}$, we have that $(S_1, S_2)$ is independent if and only if

$$ \text{either } |\lambda_1| \ge |\partial_2^-(A_2)| \text{ or } |\rho_1| \ge |\partial_2^-(A_2)| \text{ (resp. } |\lambda_2| \ge |\partial_2^-(A_1)| \text{ or } |\rho_2| \ge |\partial_2^-(A_1)|). $$

*Proof.* If $(S_1, S_2)$ is independent, then, by Lemma C.1(iii),

$$ |\partial_2^-(A_1)| + |\partial_2^-(A_2)| \le |\lambda_1| + |\partial_2^-(A_1)| + |\rho_1| = |\lambda_2| + |\partial_2^-(A_2)| + |\rho_2|, $$

that is,

$$ |\partial_2^-(A_1)| \le |\lambda_2| + |\rho_2| \quad \text{and} \quad |\partial_2^-(A_2)| \le |\lambda_1| + |\rho_1|. $$

By hypothesis, we have $|\partial_2^-(A_1)| > 0$, so that $|\lambda_2| + |\rho_2| > 0$. If $|\lambda_2| > 0$, then, by Lemma C.1(i), $|\lambda_1| = 0$ so $|\partial_2^-(A_2)| \le |\rho_1|$. Similarly, if $|\rho_2| > 0$, then $|\partial_2^-(A_2)| \le |\lambda_1|$, which proves the first implication.

Conversely, if $|\lambda_1| \ge |\partial_2^-(A_2)|$, then, since $\partial_2^-(A_2) > 0$ by our hypothesis on $\mathbb{P}$, we have $|\lambda_1| > 0$. By Lemma C.1(i), we get that $|\lambda_2| = 0$. Also,

$$ |\lambda_1| + |\partial_2^-(A_1)| + |\rho_1| = |\partial_2^-(A_2)| + |\rho_2| \le |\lambda_1| + |\rho_2|, $$

so $|\rho_2| \ge |\partial_2^-(A_1)| + |\rho_1|$, thus $|\rho_1| < |\rho_2|$. By Lemma C.1(ii), we have $|\rho_1| = 0$. Moreover,

$$ |\partial_2^-(A_1)| + |\partial_2^-(A_2)| \le |\partial_2^-(A_1)| + |\lambda_1| = |\partial_2^-(S_1)| $$

hence, by Lemma C.1(iii), $(S_1, S_2)$ is independent. □

Then, we prove that minimal non-independent branchings are uniquely characterized by a small amount of information:

**Lemma C.4.** Given a minimal non-independent branching $(S_1, S_2)$ of $\mathbb{P}$ with

$$ S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i $$

for some $l_i, r_i \in \mathbb{P}_1^*$, $\lambda_i, \rho_i \in \mathbb{P}_2^*$ and $A_i \in \mathbb{P}_3$ for $i \in \{1, 2\}$, we have that $(S_1, S_2)$ is uniquely determined by $A_1, A_2, |\lambda_1|$ and $|\lambda_2|$.

*Proof.* Let the unique $k_1, k_2 > 0$, $u_i, u'_i, v_i, v'_i \in \mathbb{P}_1^*$ and $\alpha_i, \beta_i \in \mathbb{P}_2$ such that

$$ \partial_2^-(A_1) = (u_1 *_0 \alpha_1 *_0 u'_1) *_1 \cdots *_1 (u_{k_1} *_0 \alpha_{k_1} *_0 u'_{k_1}) $$

and

$$ \partial_2^-(A_2) = (v_1 *_0 \beta_1 *_0 v'_1) *_1 \cdots *_1 (v_{k_2} *_0 \beta_{k_2} *_0 v'_{k_2}). $$
Let $i_1 = 1 + |\lambda_1|$ and $i_2 = 1 + |\lambda_2|$. Since

$$ \lambda_1 *_1 (l_1 *_0 \partial_2^-(A_1) *_0 r_1) *_1 \rho_1 = \lambda_2 *_1 (l_2 *_0 \partial_2^-(A_2) *_0 r_2) *_1 \rho_2, \quad (19) $$

and, by Lemma C.3, $|\lambda_1| < |\partial_2^-(A_2)|$ and $|\lambda_2| < |\partial_2^-(A_1)|$, we get

$$ l_1 *_0 u_{i_2} *_0 \alpha_{i_2} *_0 u'_{i_2} *_0 r_1 = l_2 *_0 v_{i_1} *_0 \beta_{i_1} *_0 v'_{i_1} *_0 r_2 $$

so that

$$ l_1 *_0 u_{i_2} = l_2 *_0 v_{i_1} \quad \text{and} \quad u'_{i_2} *_0 r_1 = v'_{i_1} *_0 r_2. $$

By Lemma C.1(iv), either $l_1$ or $l_2$ is an identity. Thus, if $|u_{i_2}| \le |v_{i_1}|$, then $|l_1| \ge |l_2|$ so $l_2$ is a unit and $l_2$ is the prefix of $u_{i_2}$ of size $|u_{i_2}| - |v_{i_1}|$. Otherwise, if $|u_{i_2}| \le |v_{i_1}|$, we obtain similarly that $l_1$ is the prefix of $v_{i_1}$ of size $|v_{i_1}| - |u_{i_2}|$ and $l_2$ is a unit. In both cases, $l_1$ and $l_2$ are completely determined by $A_1, A_2, |\lambda_1|$ and $|\lambda_2|$. A similar argument holds for $r_1$ and $r_2$.

Now, if $|\lambda_1| > 0$, by Lemma C.1(i), $|\lambda_2| = 0$. By (19) and since $|\lambda_1| < |\partial_2^-(A_2)|$, $\lambda_1$ is the prefix of $l_2 *_0 \partial_2^-(A_2) *_0 r_2$ of length $|\lambda_1|$. Otherwise, if $|\lambda_1| = 0$, then $\lambda_1 = \text{id}_{l_1 *_0 \partial_1^-(A_1) *_0 r_1}$. In both cases, $\lambda_1$ is completely determined by $A_1, A_2, |\lambda_1|$. A similar argument holds for $\lambda_2$. Note that, if we prove that $|\rho_1|$ and $|\rho_2|$ are completely determined by $A_1, A_2, |\lambda_1|$ and $|\lambda_2|$, the above argument also applies to $\rho_1$ and $\rho_2$ and the lemma is proved. But

$$ |\lambda_1| + |\partial_2^-(A_1)| + |\rho_1| = |\lambda_2| + |\partial_2^-(A_2)| + |\rho_2|, $$

so that if $|\lambda_1| + |\partial_2^-(A_1)| \ge |\lambda_2| + |\partial_2^-(A_2)|$, then, by Lemma C.1(ii), $|\rho_1| = 0$ and

$$ |\rho_2| = |\lambda_1| + |\partial_2^-(A_1)| - |\lambda_2| - |\partial_2^-(A_2)|. $$

Otherwise, if $|\lambda_1| + |\partial_2^-(A_1)| \le |\lambda_2| + |\partial_2^-(A_2)|$, we get similarly that

$$ |\rho_1| = |\lambda_2| + |\partial_2^-(A_2)| - |\lambda_1| - |\partial_2^-(A_1)| $$

and $|\rho_2| = 0$. In both cases, $|\rho_1|$ and $|\rho_2|$ are completely determined by $A_1, A_2, |\lambda_1|$ and $|\lambda_2|$, which concludes the proof. $\square$

Given $A \in \mathbb{P}_3$, we say that $A$ is an *operational* generator if it is not an interchange generator. We now prove that an operational generator can form a critical branching with a finite number of interchange generators:

**Lemma C.5.** Given an operational $A_1 \in \mathbb{P}_3$, there are a finite number of interchange generators $A_2 \in \mathbb{P}_3$ so that there is a critical branching $(S_1, S_2)$ of $\mathbb{P}$ with

$$ S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i $$

for some $l_i, r_i \in \mathbb{P}_1^*$, $\lambda_i, \rho_i \in \mathbb{P}_2^*$ for $i \in \{1, 2\}$.

*Proof.* Let $\alpha, \beta \in \mathbb{P}_2$, $u \in \mathbb{P}_1^*$, $A_2 = X_{\alpha, u, \beta}$, $l_i, r_i \in \mathbb{P}_1^*$, $\lambda_i, \rho_i \in \mathbb{P}_2^*$ for $i \in \{1, 2\}$, so that $(S_1, S_2)$ is a critical branching of $\mathbb{P}$ with

$$ S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i \quad \text{for } i \in \{1, 2\} $$

for $i \in \{1, 2\}$. Let the unique $k \ge 2$, $v_i, v'_i \in \mathbb{P}_1^*$, $\gamma_i \in \mathbb{P}_2$ for $i \in \{1, \dots, k\}$ such that

$$ \partial_2^-(A_1) = (v_1 *_0 \gamma_1 *_0 v'_1) *_1 \cdots *_1 (v_k *_0 \gamma_k *_0 v'_k). $$

By Lemma C.3, since $(S_1, S_2)$ is non-independent,

$$ 2 = |\partial_2^-(X_{\alpha, u, \beta})| > \max(|\lambda_1|, |\rho_1|). $$

Note that we cannot have $|\lambda_1| = |\rho_1| = 1$. Indeed, otherwise, by Lemma C.1, we would have $|\lambda_2| = |\rho_2| = 0$, so that

$$ 2 = |\partial_2^-(X_{\alpha, u, \beta})| = |\lambda_1| + |\partial_2^-(A_1)| + |\rho_1|. $$