2.1 Globular sets

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

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\leq 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\colon C\rightarrow D$ being a family of morphisms $f_i\colon C_i\rightarrow D_i$ , for $0\leq i\leq n$ , such that $\partial^{\epsilon}_i\circ f_{i+1}=f_i\circ \partial^{\epsilon}_i$ for $\epsilon \in\{{-,+}\}$ . Given $m \ge n$ and $C \in \mathbf{Glob}_{m}$ , we denote by $\mathcal{T}^{m}_{n}(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}^{m}_{n}\colon \mathbf{Glob}_{m} \rightarrow \mathbf{Glob}_{n}$ .

For simplicity, we often implicitly suppose that, in an n-globular set C, the sets $C_i$ are pairwise disjoint and write $u\in C$ for $u\in\bigsqcup_i C_i$ . For $\epsilon\in\{{-,+}\}$ and $k\geq 0$ , we write

\begin{equation*} \partial_{i,k}^\epsilon=\partial_{i}^\epsilon\circ\partial_{i+1}^\epsilon\circ\cdots\circ\partial_{i+k-1}^\epsilon\end{equation*}

for the iterated source (when $\epsilon=-$ ) and target (when $\epsilon=+$ ) maps. We generally omit the index k when it is clear from the context. Also, we sometimes simply write $\partial^\epsilon(u)$ for $\partial_{i,1}^\epsilon(u)$ . Given $i,j,k\in \{{0,\ldots,n}\}$ with $k<i$ and $k<j$ , we write $C_i\times_kC_j$ for the pullback:

A sequence of globes $u_1 \in C_{i_1}, \ldots, u_p \in C_{i_p}$ is said i-composable, for some $i < \min\!(i_1,\ldots,i_p)$ , when $\partial^+_{i}(u_j) = \partial^-_i(u_{j+1})$ for $1 \le j < p$ . Given $u,v \in C_{i+1}$ with $i < n$ , u and v are said parallel when $\partial^{\epsilon}(u) =\partial^{\epsilon}(v)$ for $\epsilon \in \{{-,+}\}$ .

For $u\in C_{i+1}$ , we sometimes write $u\colon v\rightarrow w$ to indicate that $\partial^-_i(u)=v$ and $\partial^+_i(u)=w$ . In low dimension, we use n-arrows such as $\Rightarrow$ , $\Rrightarrow$ , $\Rrightarrow$ , etc., to indicate the sources and the targets of n-globes in several dimensions. For example, given a 2-globular set C and $\phi \in C_2$ , we sometimes write

\begin{equation*} \phi\colon f \Rightarrow g \colon x \rightarrow y\end{equation*}

to indicate that $\partial^-_1(\phi) = f$ , $\partial^+_1(\phi) = g$ , $\partial^-_0(\phi) = x$ and $\partial^+_0(\phi)= y$ . We also use these arrows in graphical representations to picture the elements of a globular set C. For example, given an n-globular set C with $n \ge 2$ , the drawing

(1)

figures two 2-globes $\phi,\psi \in C_2$ , four 1-globes $f,g,h,k \in C_1$ , and three 0-globes $x,y,z \in C_0$ such that

\begin{gather*} \partial^-_1(\phi) = f, \qquad \partial^+_1(\phi) = \partial^-_1(\psi)= g, \qquad \partial^+_1(\psi) = h, \\ \partial^-_0(f) = \partial^-_0(g) = \partial^-_0(h) = x, \qquad \partial^+_0(f) = \partial^+_0(g) = \partial^+_0(h) = \partial^-_0(k) = y, \qquad \partial^+_0(k) = 0.\end{gather*}

2.2 n-precategories

Given $n\in\mathbb{N}$ , an n-precategory C is an n-globular set equipped with

• identity functions $\text{id}^{k}\colon C_{k-1}\rightarrow C_{k}$ , for $0< i\le n$ ,

• composition functions ${\ast}_{k,l}\colon C_k\times_{\min\!(k,l)-1}C_l\rightarrow C_{\max(k,l)}$ , for $0<k,l\leq n$ ,

satisfying the axioms below. In this context, the elements of $C_i$ are called i-cells. Since the dimensions of the cells determine the functions to be used, we often omit the indices of id and, given $0 < k,l\le n$ and $i = \min\!(k,l) - 1$ , we often write ${\ast}_{i}$ for ${\ast}_{k,l}$ . For example, in a 2-precategory which has a configuration of cells as in (1), there are, among others, 1-cells $f{\ast}_0k$ , $h{\ast}_0 k$ and 2-cells $\phi{\ast}_1\psi$ and $\psi{\ast}_0k$ given by the composition operations. The axioms of n-precategories are the following:

1. (i) for $k < n$ and $u\in C_k$ ,

   \begin{equation*} \partial^-_k(\text{id})=u=\partial^+_k(\text{id}^), \end{equation*}

2. (ii) for $i,k,l \in \{{0,\ldots,n}\}$ such that $i = \min\!(k,l) -1$ , $(u,v)\in C_k\times_iC_l$ , and ${\epsilon \in \{{-,+}\}}$ ,

   \begin{align*} \partial^{\epsilon}(u {\ast}_i v) &= \begin{cases} u{\ast}_i \partial^{\epsilon}(v)& \text{if $k < l$,}\\ \partial^-(u)&\text{if $k=l$ and $\epsilon = -$,}\\ \partial^+(v)&\text{if $k=l$ and $\epsilon = +$,}\\ \partial^{\epsilon}(u){\ast}_i v&\text{if $k>l$,} \end{cases} \end{align*}

3. (iii) for $i,k,l \in \{{0,\ldots,n}\}$ with $i = \min\!(k,l) - 1$ , given $(u,v)\in C_{k-1}\times_{i}C_l$ ,

   \begin{align*} \text{id}^{}_{u}{\ast}_i v &= \begin{cases} v&\text{if $k \le l$,}\\ \text{id}^{}_{u{\ast}_i v}&\text{if $k > l$,} \end{cases} \end{align*}
   and, given $(u,v) \in C_k \times_i C_{l-1}$ ,
   \begin{align*} u{\ast}_i \text{id}^{}_{v} &= \begin{cases} u&\text{if $l\le k$,}\\ \text{id}^{}_{u{\ast}_i v}&\text{if $l > k$,} \end{cases} \end{align*}

4. (iv) for $i,k,l,m \in \{{0,\ldots,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,

   \begin{equation*} (u{\ast}_iv){\ast}_iw = u{\ast}_i(v{\ast}_iw), \end{equation*}

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

   \begin{equation*} j = \min\!(k,k') - 1 \quad\text{and}\quad i < j{,} \end{equation*}
   given $u \in C_{i+1}$ and $(v,v') \in C_k \times_j C_{k'}$ such that u,v are icomposable,
   \begin{equation*} u {\ast}_i (v {\ast}_j v') = (u {\ast}_i v) {\ast}_j (u {\ast}_i v') \end{equation*}
   and, given $(u,u') \in C_k \times_j C_{k'}$ and $v \in C_{i+1}$ such that u,v are icomposable,
   \begin{equation*} (u {\ast}_j u') {\ast}_i v = (u {\ast}_i v) {\ast}_j (u' {\ast}_i v). \end{equation*}

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 Adámek and Rosický (Reference Adámek and Rosický1994, Thm. 3.36); consequently, it is complete and cocomplete Adámek and Rosický (Reference Adámek and Rosický1994, 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

we can represent the two 2-cells

\begin{equation*} (\phi {\ast}_0 g) {\ast}_1 (f' {\ast}_0 \psi) \qquad\qquad\text{and}\qquad\qquad (f {\ast}_0 \psi) {\ast}_1 (\phi {\ast}_0 g')\end{equation*}

respectively by

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

makes no sense in a generic 2-precategory.

2.3 Truncation functors

Similarly to strict categories (Métayer Reference Métayer2008), the categories $\mathbf{PCat}_{n}$ for $n \ge 0$ can be related by several functors. For $m\geq n$ , we have a truncation functor:

\begin{equation*} {\mathcal{T}}^{m}_{n}\colon \mathbf{PCat}_{m} \rightarrow\mathbf{PCat}_{n}\end{equation*}

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

\begin{equation*} \mathcal{F}^{m}_{n}\colon\mathbf{PCat}_{n}\rightarrow\mathbf{PCat}_{m}\end{equation*}

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

Proposition 2.3.1. For $m > n$ , the functors ${\mathcal{T}}^{m}_{n}$ and $\mathcal{F}^{m}_{n}$ admit both left and right adjoints, that is, we have a sequence of adjunctions:

\begin{equation*} {\mathcal{H}}^{m}_{n}\dashv\mathcal{F}^{m}_{n}\dashv{\mathcal{T}}^{m}_{n}\dashv{\mathcal{R}}^{ }_{n}m. \end{equation*}

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

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

\begin{equation*}\text{j}_{-}\colon(-)_{(n)} \rightarrow \text{1}_{\mathbf{PCat}_{m}}\end{equation*}

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

2.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 (Reference Weber2009) 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:

Since $\mathop{\text{j}}\nolimits_{(\!-\!)}$ is a natural transformation, the funny tensor product can be extended as a functor:

\begin{equation*} (\!-\!)\square(\!-\!)\colon \mathbf{PCat}_{n} \times \mathbf{PCat}_{n} \rightarrow \mathbf{PCat}_{n}.\end{equation*}

We show that it equips $\mathbf{PCat}_{n}$ with a structure of monoidal category. First, we prove several technical lemmas.

Lemma 2.4.1. Given n-precategories C and $(D^i)_{i \in I}$ , the canonical morphism

\begin{equation*} \bigsqcup_{i\in I} (C \times D^i) \rightarrow C \times (\bigsqcup_{i\in I} D^i) \end{equation*}

is an isomorphism.

Proof. Since, by Proposition 2.3.1, $\mathcal{F}^{n}_{0}$ preserves limits and colimits, we have $D_{(0)} \cong \bigsqcup_{x \in D_0} \text{1}$ . Given a diagram $C(\!-\!)\colon I \rightarrow \mathbf{PCat}_{n}$ , by Lemma 2.4.1, we have

Lemma 2.4.3. Given n-precategories C,D,E, there is an isomorphism:

natural in C, D, and E.

Proof. Given n-precategories C, D and E, the precategory $(C \square D) \square E$ is defined by the pushout:

Since, by Lemma 2.4.2, $(\!-\!) \times E_{(0)}$ preserves colimits, the following diagram is also a pushout:

Thus, $(C \square D) \square E$ is the colimit of the diagram:

(2)

The precategory $C \square (D \square E)$ admits a similar diagram, and we deduce easily, using the associativity of $\times$ , a canonical morphism ${\alpha}_{C,D,E}\colon (C \square D) \square E \rightarrow C \square (D \square E)$ , which admits an inverse defined symmetrically. The morphism ${\alpha}_{C,D,E}$ is easily checked to be natural in C, D, and E.

Given an n-precategory, there are canonical morphisms:

where ${\lambda}^{\text{f}}_C$ is defined by:

and ${\rho}^{\text{f}}_C$ is defined similarly. Both are natural in C. We can conclude that:

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

2.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 (Burroni Reference Burroni1993). Polygraphs were also generalized by Batanin to algebras of any finitary monad on globular sets (Batanin Reference Batanin1998), 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}\rightarrow \mathbf{Glob}_{n}$ , we define the category $\mathbf{PCat}_{n}^+$ as the pullback:

and write ${\mathcal{U}}_{n}^+\colon \mathbf{PCat}_{n}^+ \rightarrow \mathbf{Glob}_{n+1}$ for the top arrow of the pullback and ${\mathcal{V}}_{n}\colon \mathbf{PCat}_{n}^+ \rightarrow \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\colon C_{n+1}\rightarrow C_n$ (note however that there is no notion of composition for $(n{+}1)$ -cells). There is a functor ${\mathcal{W}}_{n}\colon \mathbf{PCat}_{n+1} \rightarrow \mathbf{PCat}_{n}^+$ defined as the universal arrow:

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 Barr and Wells Reference Barr and Wells2005, Thm. 4.1 for instance), so that ${\mathcal{W}}_{n}$ admits a left adjoint ${\mathcal{L}}_{n}\colon \mathbf{PCat}_{n}^+ \rightarrow \mathbf{PCat}_{n+1}$ .

We define the category $\mathbf{Pol}_{n}$ of n-prepolygraphs together with a functor ${\mathcal{G}}_{n}\colon \mathbf{Pol}_{n} \rightarrow \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:

and write ${\mathcal{G}}_{n}^+\colon \mathbf{Pol}_{n+1} \rightarrow \mathbf{PCat}_{n}^+$ for the top arrow and ${\mathcal{T}}^{n+1}n$ 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 $\textsf{P}$ consists in a diagram of sets:

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: $\textsf{P}_i$ is the set of i-generators, $d_i,d_i\colon \textsf{P}_{i+1}\rightarrow\textsf{P}_i^*$ , respectively, associate with each $(i{+}1)$ -generator its source and target, and $\textsf{P}_i^*$ is the set of i-cells, that is, formal compositions of i-generators. In line with the latter notation, we will often write $\textsf{P}^*$ for the image of an n-prepolygraph $\textsf{P}$ by ${\mathcal{G}}_{n}$ .

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

Example 2.5.1. We define the 3-prepolygraph $\textsf{P}$ for pseudomonoids as follows. We put

\begin{align*} \textsf{P}_0&= \{{x}\}, & \textsf{P}_1&= \{{a\colon x \rightarrow x}\}, & \textsf{P}_2&= \{{\mu\colon \bar 2 \Rightarrow \bar 1, \eta\colon \bar 0 \Rightarrow \bar 1}\}, \end{align*}

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

Note that we make use of the arrows $\rightarrow$ , $\Rightarrow$ and $\Rrightarrow$ 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 {\ast}_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.

2.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^{\epsilon}_{n-1}(u) = \partial^{\epsilon}_{n-1}(u')$ for $\epsilon \in \{{-,+}\}$ ,

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

  \begin{equation*} v {\ast}_i u {\ast}_i w \sim v {\ast}_i u' {\ast}_i w. \end{equation*}

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:

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

2.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 Métayer (Reference Métayer2008) in the case of polygraphs. This $(n{+}1)$ -precategory has 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 $\text{id}_{u}$ ,

• for every $0\leq i<n$ , for every $u\in C_{i+1}$ and every expression v, there is an expression $u{\ast}_i v$ ,

• for every $0\leq i<n$ , for every expression u and every $v\in C_{i+1}$ , there is an expression $u{\ast}_i v$ ,

• for every pair of expressions u and v, there is an expression $u{\ast}_n v$ .

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

• $\vdash t\colon u\rightarrow 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'\colon u\rightarrow 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$ ,

  

• for every $u\in C_n$ ,

  

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

  

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

  

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

  

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:

(3)

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

The next ones express that composition is associative:

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

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

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

Finally, the last ones express that equality is contextual:

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

A term t is well typed if there are $u,v\in C_n$ such that $\vdash t\colon u\rightarrow v$ is derivable using the above rules. In this case, by Lemma 2.7.1, the types u and v are uniquely determined by t, and we write $\partial^-_n(t)=u$ and $\partial^+_n(t)=v$ . We define $C_{n+1}^*$ to be the set of equivalence classes under $=$ of well-typed expressions. By Lemma 2.7.2, the operations $\partial^-_n$ and $\partial^+_n$ are compatible with the relation $=$ . We finally define ${\mathcal{L}}_{n}(C,C_{n+1})$ as the $(n{+}1)$ -precategory with C as underlying n-precategory, $C_{n+1}^*$ as set of $(n{+}1)$ -cells, with sources and targets given by the maps $\partial^-_n$ and $\partial^+_n$ . 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:

2.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, that is, we write $u_1{\ast}_nu_2{\ast}_n\cdots{\ast}_n u_k$ instead of $u_1{\ast}_n(u_2{\ast}_n(\cdots{\ast}_nu_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{align*} \text{id}_{u} {\ast}_n t &\Rightarrow t & t {\ast}_n \text{id}^{}_{u} &\Rightarrow t \\ (t_1 {\ast}_n t_2) {\ast}_n t_3 & \Rightarrow t_1 {\ast}_n (t_2 {\ast}_n t_3) & (u_1 {\ast}_i t_n) {\ast}_i u_2 &\Rightarrow u_1 {\ast}_i (t_n {\ast}_i u_2) \\ &\cdots & &\cdots\end{align*}

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_1$ , and $t_2$ 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 left) and confluent when for all expressions t, $t_1$ , and $t_2$ 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):

Those notions are introduced in more details in Baader and Nipkow (Reference Baader and Nipkow1999).

• 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(\text{id}_{u}) = l_{i}(\text{id}_{u}) = r_{i}(\text{id}_{u}) = 1$ ,

• if $t = t_1 {\ast}_n t_2$ , we put

  \begin{align*} 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{align*}

• if $t = u {\ast}_j t'$ , we put $c_n(t) = c_n(t')$ and

  \begin{align*} 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} & r_{i}(t)&= \begin{cases} r_{i}(t') & \text{if $j < i$,} \\ r_{i}(t') + 1 & \text{if $j \ge i$,} \end{cases} \end{align*}

• if $t = t' {\ast}_j v$ , we put $c_{n}(t) = c_n(t')$ and

  \begin{align*} l_{i}(t)&= \begin{cases} l_{i}(t') & \text{if $j \le i$,} \\ l_{i}(t') + 1 & \text{if $j > i$,} \end{cases} & 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} \end{align*}

For each expression t, we define

\begin{equation*} N(t) = (c_n(t),l_{n-1}(t),r_{n-1}(t),\ldots,l_{0}(t),r_{0}(t)) \in \mathbb{N}^{2n+1} \end{equation*}

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

• if $t = t_1 {\ast}_n t_2$ and $t' = t'_1 {\ast}_n t_2$ with $N(t_1) <_{\text{lex}} N(t'_1)$ , then $N(t) <_{\text{lex}} N(t')$ ,

• if $t = t_1 {\ast}_n t_2$ and $t' = t_1 {\ast}_n t'_2$ with $N(t'_2) <_{\text{lex}} N(t_2)$ , then $N(t') <_{\text{lex}} N(t)$ ,

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

• if $t = \tilde t {\ast}_i v$ and $t' = \tilde t' {\ast}_i v$ with $N(\tilde t') <_{\text{lex}} N(\tilde t)$ , then $N(t') <_{\text{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{align*} c_n(\text{id}_{u} {\ast}_n t) &= c_n(t) + 3 > c_n(t), \\ c_n((t_1 {\ast}_n t_2) {\ast}_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 {\ast}_n (t_2 {\ast}_n t_3)), \\ l_{i}(u_1 {\ast}_i (u_2 {\ast}_i t)) &= 4l_{i}(t) + 3 > 2l_{i}(t) + 1 = l_{i}((u_1 {\ast}_i u_2) {\ast}_i t), \\ r_{i}((u_1 {\ast}_i t) {\ast}_i u_2) &= 2r_{i}(t) + 3 > 2r_{i}(t) + 2 = r_{i}(u_1 {\ast}_i (t {\ast}_i u_2)), \\ l_{i}(u {\ast}_i (t_1 {\ast}_n t_2)) &= 2l_{i}(t_1) + 2l_{i}(t_2) + 5 \\ &> 2l_{i}(t_1) + 2l_{i}(t_2) + 4 = l_{i}((u {\ast}_i t_1) {\ast}_n (u {\ast}_i t_2)), \\ l_{i}(u {\ast}_i (v {\ast}_j t)) &= 2l_{i}(t) + 3 > 2l_{i}(t) + 2 = l_{i}((u {\ast}_i v) {\ast}_j (u {\ast}_i t)) \text{ for $j > i$.} \end{align*}

Thus, if $t \Rightarrow t'$ , we have $N(t') <_{\text{lex}} N(t)$ . Since the lexicographical order $<_{\text{lex}}$ on $\mathbb{N}^{2n+1}$ is well founded, the reduction rule $\Rightarrow$ is terminating.

Proof. By a direct adaptation of the critical pair lemma (e.g., Baader and Nipkow Reference Baader and Nipkow1999, 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:

\begin{equation*} (t_1 {\ast}_n (t_2 {\ast}_n t_3)) {\ast}_n t_4 \Leftarrow ((t_1 {\ast}_n t_2) {\ast}_n t_3) {\ast}_n t_4 \Rightarrow (t_1 {\ast}_n t_2) {\ast}_n (t_3 {\ast}_n t_4). \end{equation*}

This branching is confluent since

\begin{equation*} (t_1 {\ast}_n (t_2 {\ast}_n t_3)) {\ast}_n t_4 \Rightarrow t_1 {\ast}_n ((t_2 {\ast}_n t_3) {\ast}_n t_4) \Rightarrow t_1 {\ast}_n (t_2 {\ast}_n (t_3 {\ast}_n t_4)) \end{equation*}

and

\begin{equation*} (t_1 {\ast}_n t_2) {\ast}_n (t_3 {\ast}_n t_4) \Rightarrow t_1 {\ast}_n (t_2 {\ast}_n (t_3 {\ast}_n t_4)). \end{equation*}

Another critical branching is given by the reductions:

\begin{equation*} (u_1 {\ast}_i u_2) {\ast}_i (t_1 {\ast}_n t_2) \Leftarrow u_1 {\ast}_i (u_2 {\ast}_i (t_1 {\ast}_n t_2)) \Rightarrow u_1 {\ast}_i ((u_2 {\ast}_i t_1) {\ast}_n (u_2 {\ast}_i t_2)) \end{equation*}

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

\begin{equation*} (u_1 {\ast}_i u_2) {\ast}_i (t_1 {\ast}_n t_2) \Rightarrow ((u_1 {\ast}_i u_2) {\ast}_i t_1) {\ast}_n ((u_1 {\ast}_i u_2) {\ast}_i t_2) \end{equation*}

and

\begin{align*} u_1 {\ast}_i ((u_2 {\ast}_i t_1) {\ast}_n (u_2 {\ast}_i t_2)) &\Rightarrow (u_1 {\ast}_i(u_2 {\ast}_i t_1)) {\ast}_n (u_1 {\ast}_i (u_2 {\ast}_i t_2)) \\ &\Rightarrow ((u_1 {\ast}_iu_2) {\ast}_i t_1) {\ast}_n ((u_1 {\ast}_i u_2) {\ast}_i t_2). \end{align*}

The other cases are similar.

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

\begin{equation*} u=u_1{\ast}_nu_2{\ast}_n\cdots{\ast}_n u_k \end{equation*}

where each $u_i$ decomposes as:

(4) \begin{equation} u_i=v^i_{n}{\ast}_{n-1}(\cdots{\ast}_2(v^i_2{\ast}_1(v^i_1{\ast}_0 A^i{\ast}_0 w^i_1){\ast}_1 w^i_2){\ast}_2\cdots){\ast}_{n-1} w^i_{n} \end{equation}

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

A cell of $C^*_{n+1}$ of the form (4) is called a whisker. By the inductive definition of prepolygraphs from Section 2.5 and Theorem 2.8.3, given an m-prepolygraph $\textsf{P}$ with $m > 0$ , an $(i{+}1)$ -cell $u \in \textsf{P}^*_{i+1}$ with $i \in \{{0,\ldots,m-1}\}$ can be uniquely written as a composite of $(i{+}1)$ -dimensional whiskers $u_1 {\ast}_i\cdots {\ast}_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 2.8.3.

Example 2.8.4. Recall the 3-prepolygraph of pseudomonoids $\textsf{P}$ from Example 2.5.1. Theorem 2.8.3 allows a canonical string diagram representation of the elements of $\textsf{P}^*_2$ : first, we represent the 2-generators $\mu$ and $\eta$ by

and

, respectively. Secondly, we represent the whiskers $\bar m {\ast}_0 \alpha {\ast}_0 \bar n$ for $m,n\in\mathbb{N}$ and $\alpha \in \textsf{P}_2$ by adding m wires on the left and n wires on the right of the representation of $\alpha$ . For example, $\bar 2 {\ast}_0 \mu {\ast}_0 \bar 3$ is represented by:

Finally, a 2-cell of $\textsf{P}^*_2$ , which decomposes as a composite of whiskers $w_1 {\ast}_1 \cdots {\ast}_1 w_k$ , is represented by stacking the representation the whiskers. For example, below are shown two 2-cells with their associated graphical representation:

Note that, contrary to 2-cells of strict 2-categories, these two 2-cells are not equal in $\textsf{P}^*_2$ . The above graphical representation can be used in order to define unambiguously the source and target of 3-cells. Here, the 3-generators $\textsf{A}$ , $\textsf{L}$ , and $\textsf{R}$ can be described graphically by:

2.9 $\mathbf{(3,2)}$ -precategories

In the following sections, we will mostly consider 3-precategories that are generated by 3-prepolygraphs (as the one from Example 2.5.1), whose 3-generators should moreover be thought as “invertible operations” (think of the 3-generators $\textsf{A},\textsf{L},\textsf{R}$ of Example 2.5.1). Thus, we will in fact be dealing with 3-precategories whose 3-cells are all invertible. Such 3-precategories will usually be obtained by applying a localization construction to the 3-precategory $\textsf{P}^*$ for some 3-prepolygraph $\textsf{P}$ , which is a direct adaptation of the one for categories and described below.

Given a 3-precategory C, a 3-cell $F\colon \phi\Rrightarrow\phi' \in C_3$ is invertible when there exists $G\colon \phi'\Rrightarrow \phi$ such that $F {\ast}_2 G = \text{id}_{\phi}$ and $G {\ast}_2 F = \text{id}_{\phi'}$ . In this case, G is unique and we write it as $F^{-1}$ . A (3,2)-precategory is a 3-precategory where every 3-cell is invertible. The (3,2)-precategories form a full subcategory of $\mathbf{PCat}_{3}$ denoted $\mathbf{PCat}_{(3,2)}$ .

There is a forgetful functor:

\begin{equation*} \mathop{\mathcal{U}}\colon \mathbf{PCat}_{(3,2)} \rightarrow \mathbf{PCat}_{3}\end{equation*}

which admits a left adjoint $(\!-\!)^{\top}$ also called localization functor described as follows. Given a 3-precategory C, for every $F\colon\phi\Rightarrow\phi' \in C_3$ , we write $F^+$ for a formal element of source $\phi$ and target $\phi'$ , and $F^-$ for a formal element of source $\phi'$ and target $\phi$ . A zigzag of C is a list:

(5) \begin{equation} (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}\end{equation}

for some $k \ge 0$ , $F_1,\ldots,F_k \in C_{3}$ and $\epsilon_1,\ldots,\epsilon_k \in\{{-,+}\}$ such that $\phi = \partial^-(F_1^{\epsilon_1})$ , $\phi' = \partial^+(F_k^{\epsilon_k})$ and $\partial^+(F_i^{\epsilon_i}) = \partial^-(F_{i+1}^{\epsilon_{i+1}})$ for $1 \le i < k$ (there is one empty list $()_{\phi,\phi}$ for each $\phi \in \textsf{P}^*_2$ , by convention). The source and the target of a zigzag as in (5) are $\phi$ and $\phi'$ respectively. Then, we define the truncation ${\mathcal{T}}^{3}_{2}(C^{\top})$ as ${\mathcal{T}}^{3}_{2}(C)$ and $(C^{\top})_{3}$ as the quotient of the zigzags by the following equalities: for every zigzag $(F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}$ ,

• if $F_i = \text{id}_{\psi}$ for some $i \in \{{1,\ldots,k}\}$ and $\psi \in C_2$ , then

  \begin{equation*} (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'} = (F_1^{\epsilon_1},\ldots,F_{i-1}^{\epsilon_{i-1}},F_{i+1}^{\epsilon_{i+1}},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}, \end{equation*}

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

  \begin{equation*} (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'} = (F_1^{\epsilon_1},\ldots,F_{i-1}^{\epsilon_{i-1}},(F_{i} {\ast}_2 F_{i+1})^{+},F_{i+2}^{\epsilon_{i+2}},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}, \end{equation*}

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

  \begin{equation*} (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'} = (F_1^{\epsilon_1},\ldots,F_{i-1}^{\epsilon_{i-1}},(F_{i+1} {\ast}_2 F_{i})^{-},F_{i+2}^{\epsilon_{i+2}},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}, \end{equation*}

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

  \begin{equation*} (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'} = (F_1^{\epsilon_1},\ldots,F_{i-1}^{\epsilon_{i-1}},F_{i+2}^{\epsilon_{i+2}},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}. \end{equation*}

Since the definitions of source and target of zigzags are compatible with the above equalities, they induce source and target operations $\partial^-,\partial^+\colon(C^{\top})_{3} \rightarrow C_2$ . Given

\begin{equation*} F = (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi_1,\phi_2} \in (C^{\top})_{3} \quad\text{and}\quad G = (G_1^{\delta_1},\ldots,G_l^{\delta_l})_{\phi_2,\phi_3} \in (C^{\top})_{3},\end{equation*}

we define $F {\ast}_2 G$ as:

\begin{equation*} F {\ast}_2 G = (F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k},G_1^{\delta_1},\ldots,G_l^{\delta_l})_{\phi_1,\phi_3}\end{equation*}

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

\begin{equation*} u {\ast}_i F = ((u {\ast}_i F_1)^{\epsilon_1},\ldots,(u {\ast}_i F_k)^{\epsilon_k})_{u {\ast}_i \phi,u {\ast}_i \phi'}\end{equation*}

and, finally, given $\phi \in C_2$ , we define $\text{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\colon C \rightarrow C^{\top}$ sending $F\colon\phi\Rrightarrow\psi\in C_3$ to $(F^+)_{\phi,\psi}$ . Moreover, given a (3,2)-precategory D and a 3-prefunctor $G\colon C \rightarrow D$ , we can define $G'\colon C^{\top} \rightarrow D$ by putting $G'(u) = G(u)$ for $u \in C_i$ with $i \le 2$ and

\begin{equation*} G'((F_1^{\epsilon_1},\ldots,F_k^{\epsilon_k})_{\phi,\phi'}) = G'(F_1^{\epsilon_1}) {\ast}_2 \ldots {\ast}_2 G'(F_k^{\epsilon_k})\end{equation*}

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

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

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 $\mathop{\mathcal{U}}$ . In the following, given a 3-precategory C and $F \in C_3$ , we often write F for H(F).

3.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 Gray (Reference Gray1974, 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)$ ,

\begin{equation*} (\phi {\ast}_0 \partial^-_1(\psi)) {\ast}_1 (\partial^+_1(\phi) {\ast}_0 \psi) = (\partial^-_1(\phi) {\ast}_0 \psi) {\ast}_1 (\phi {\ast}_0 \partial^+_1(\psi)).\end{equation*}

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 ${\ast}$ 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:

  \begin{equation*} (f,y)\colon (x,y) \rightarrow (x',y) \quad\text{and}\quad (x,g)\colon (x,y) \rightarrow (x,y'), \end{equation*}
  for $f\colon x \rightarrow x' \in C_1$ and $g\colon y \rightarrow y' \in C_2$ ,

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

  \begin{equation*} (\phi,y)\colon (f,y) \rightarrow (f',y) \quad\text{and}\quad (x,\psi)\colon (x,g) \rightarrow (x,g') \end{equation*}
  for $\phi\colon f\Rightarrow f' \in C_2$ , $\psi\colon g\Rightarrow g' \in C_2$ and $x,y \in C_0$ , and by the 2-cells:
  
  for $f\colon x \rightarrow x' \in C_1$ and $g\colon y \rightarrow y' \in C_1$ ,

under the conditions that

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

   \begin{align*} (\text{id}_{x},y) &= (x, \text{id}_{y}) = \text{id}_{(x,y)} \\[5pt] (f {\ast}_0 f',y) &= (f,y) {\ast}_0 (f',y)\\[5pt] (x,g {\ast}_0 g') &= (x,g) {\ast}_0 (x,g') \end{align*}
   for all $x \in C_0$ , $y \in D_0$ , 0-composable $f,f' \in C_1$ and 0-composable $g,g' \in D_1$ ,

2. (ii) the 2-generators are compatible with 0-composition, meaning that

   \begin{align*} (\text{id}^{2}_{x},y) &= (x,\text{id}^{2}_{y}) = \text{id}^{2}_{(x,y)} \\[5pt] (\phi_1 {\ast}_0 \phi_2, y) & = (\phi_1,y) {\ast}_0 (\phi_2,y) \\[5pt] (x,\psi_1 {\ast}_0 \psi_2) &= (x,\psi_1) {\ast}_0 (x,\psi_2) \end{align*}
   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$ , that is, graphically,
   

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

   \begin{align*} (\text{id}_{f},y) &= \text{id}_{(f,y)} \\[4pt] (\phi_1 {\ast}_1 \phi_2, y) & = (\phi_1,y) {\ast}_1 (\phi_2,y) \\[4pt] (x, \text{id}_{g}) &= \text{id}_{(x,g)}\\[4pt] (x,\psi_1 {\ast}_1 \psi_2) &= (x,\psi_1) {\ast}_1 (x,\psi_2) \end{align*}
   for all $\phi_i\colon f_{i-1} \Rightarrow f_i \colon x \rightarrow x'$ and $\psi_i\colon g_{i-1} \Rightarrow g_i \colon y \rightarrow y'$ for $i \in \{{1,2}\}$ and $f\colon x \rightarrow x'$ and $g\colon y \rightarrow y'$ , that is, graphically,
   

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

   \begin{align*} (\text{id}_{x},g) &= \text{id}_{(x,g)} \\ (f_1 {\ast}_0 f_2,g) & = ((f_1,y) {\ast}_0 (f_2,g)) {\ast}_1 ((f_1,g) {\ast}_0 (f_2,y')) \\ (f, \text{id}_{y}) &= \text{id}_{(f,y)} \\ (f,g_1 {\ast}_0 g_2) & = ((f,g_1) {\ast}_0 (x',g_2)) {\ast}_1 ((x,g_1) {\ast}_0 (f,g_2)) \end{align*}
   for all $f_i\colon x_{i-1} \rightarrow x_i$ and $g_i\colon y_{i-1} \rightarrow y_i$ for $i \in \{{1,2}\}$ and $f\colon x \rightarrow x'$ and $g\colon y \rightarrow y'$ , that is, graphically,
   

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

   \begin{align*} ((f,g) {\ast}_1 ((x,g) {\ast}_0 (\phi,y'))) &= (( (\phi,y) {\ast}_0 (x',g)) {\ast}_1 (f',g)) \\ ((f,g) {\ast}_1 ((x,\psi) {\ast}_0 (f,y'))) &= (( (f,y) {\ast}_0 (x',\psi)) {\ast}_1 (f,g')) \end{align*}
   for $\phi\colon f\Rightarrow f'\colon x \rightarrow x'$ and $\psi\colon g\Rightarrow g'\colon y \rightarrow y'$ , that is, graphically,
   
   

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

\begin{align*} (\phi,y) &\mapsto (F(\phi),G(y)) \\ (x,\psi) &\mapsto (F(x),G(\psi)) \\ (f,g) &\mapsto (F(f),G(g))\end{align*}

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:

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

\begin{align*} ((\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))\end{align*}

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

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

\begin{equation*} {\lambda}^{\text{lax}}_C\colon \text{1} \boxtimes^{\text{lax}} C \rightarrow C \quad\text{and}\quad {\rho}^{\text{lax}}_C\colon C \boxtimes^{\text{lax}} \text{1} \rightarrow C\end{equation*}

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

\begin{align*} {\lambda}^{\text{lax}}((\ast,\psi)) = \psi \quad\text{and}\quad {\rho}^{\text{lax}}((\psi,\ast)) = \psi\end{align*}

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

A variant of the Gray tensor is called the pseudo Gray tensor product is the monoidal structure $(\mathbf{Cat}_{2},\boxtimes,\text{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:

3.2 Gray categories

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

A lax Gray category Gray (Reference Gray1974, 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 0composable pair of 2-cells $\phi\colon f \Rightarrow f'\colon x \rightarrow y$ and $\psi\colon g \Rightarrow g'\colon y \rightarrow z$ , a 3-cell:

which can be represented using string diagrams by:

called interchanger and satisfying the following sets of axioms:

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

   \begin{align*} X_{\text{id}_{f},\psi} &= \text{id}_{f {\ast}_0 \psi} & X_{\phi {\ast}_1 \phi',\psi} &= ((\phi {\ast}_0 g) {\ast}_1 X_{\phi',\psi}) {\ast}_2 (X_{\phi,\psi} {\ast}_1 (\phi' {\ast}_0 g')) \\ X_{\phi, \text{id}_{g}} &= \text{id}_{\phi {\ast}_0 g} & X_{\phi,\psi {\ast}_1 \psi'} &= (X_{\phi,\psi} {\ast}_1 (f' {\ast}_0 \psi')) {\ast}_2 ((f {\ast}_0 \psi) {\ast}_1 X_{\phi,\psi'}) \end{align*}
   and
   \begin{align*} X_{e {\ast}_0 \phi,\psi} &= e {\ast}_0 X_{\phi,\psi} & X_{\phi, \psi {\ast}_0 h} &= X_{\phi,\psi} {\ast}_0 h. \end{align*}
   Moreover, given $\phi,\psi \in C_2$ and $f \in C_1$ such that $\phi$ , f and $\psi$ are 0-composable, we have
   \begin{equation*} X_{\phi {\ast}_0 f, \psi} = X_{\phi, f {\ast}_0 \psi} \end{equation*}

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

   \begin{equation*} (A {\ast}_1 \psi) {\ast}_2 (\phi' {\ast}_1 B) = (\phi {\ast}_1 B) {\ast}_2 (A {\ast}_1 \psi') \end{equation*}

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

   \begin{equation*} A \colon \phi \Rrightarrow \phi'\colon u\Rightarrow u' \in C_3 \quad\text{and}\quad B\colon\psi\Rrightarrow \psi'\colon v \Rightarrow v' \in C_3, \end{equation*}
   such that A and B are 0-composable, we have
   \begin{align*} ((A {\ast}_0 v) {\ast}_1 (u' {\ast}_0 \psi)) {\ast}_2 X_{\phi',\psi} &= X_{\phi,\psi} {\ast}_2 ((u {\ast}_0 \psi) {\ast}_1 (A {\ast}_0 v')) \\ ((\phi {\ast}_0 v) {\ast}_1 (u' {\ast}_0 B)) {\ast}_2 X_{\phi,\psi'} &= X_{\phi,\psi} {\ast}_2 ((u {\ast}_0 B) {\ast}_1 (\phi {\ast}_0 v')). \end{align*}

A morphism between two lax Gray categories C and D is a 3-prefunctor $F\colon C \rightarrow 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 and 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:

Proof. Given 1-composable 3-cells $F\colon \phi \Rrightarrow \phi'$ and $G\colon \psi \Rrightarrow \psi' \in C_3$ , by the exchange law for 3-cells, we have, in $C^{\top}_3$ ,

\begin{equation*} (F {\ast}_1 \psi) {\ast}_2 (\phi' {\ast}_1 G) = (\phi {\ast}_1 G) {\ast}_2 (F {\ast}_1 \psi'). \end{equation*}

By inverting $F {\ast}_1 \psi$ and $F {\ast}_1 \psi'$ , we obtain

\begin{equation*} (\phi' {\ast}_1 G) {\ast}_2 ({F}^{{-}1} {\ast}_1 \psi') = ({F}^{{-}1} {\ast}_1 \psi) {\ast}_2 (\phi {\ast}_1 G). \end{equation*}

Similarly,

\begin{equation*} (\phi {\ast}_1 {G}^{{-}1}) {\ast}_2 (F {\ast}_1 \psi) = (F {\ast}_1 \psi') {\ast}_2 (\phi' {\ast}_1 {G}^{{-}1}) \end{equation*}

and

\begin{equation*} ({F}^{{-}1} {\ast}_1 \psi') {\ast}_2 (\phi {\ast}_1 {G}^{{-}1}) = (\phi' {\ast}_1 {G}^{{-}1}) {\ast}_2 ({F}^{{-}1} {\ast}_1 \psi). \end{equation*}

Now, given general 1-composable $F\colon \phi \Rrightarrow \phi', G\colon \psi \Rrightarrow \psi' \in C^{\top}_3$ , we have that

\begin{equation*} F = F_1 {\ast}_2 {F_2}^{{-}1} {\ast}_2 \cdots {\ast}_2 F_{2k-1} {\ast}_2 {F_{2k}}^{{-}1} \end{equation*}

and

\begin{equation*} G = G_1 {\ast}_2 {G_2}^{{-}1} {\ast}_2 \cdots {\ast}_2 G_{2l-1} {\ast}_2 {G_{2l}}^{{-}1} \end{equation*}

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

\begin{equation*} (F {\ast}_1 \psi) {\ast}_2 (\phi' {\ast}_1 G) = (\phi {\ast}_1 G) {\ast}_2 (F {\ast}_1 \psi'). \end{equation*}

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

3.3 Gray presentations

Starting from a 3-prepolygraph $\textsf{P}$ , such as the one of Example 3.3.1, we want to add 3-generators to $\textsf{P}$ and relations on the 3-cells of $\textsf{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 $\textsf{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 $\textsf{P}$ containing the following distinguished generators:

1. (i) for 0-composable $\alpha,g,\beta$ with $\alpha\colon f \Rightarrow f',\beta\colon g \Rightarrow g' \in \textsf{P}_2$ , $g \in \textsf{P}^*_1$ , a 3-generator $X_{\alpha,g,\beta}\in \textsf{P}_3$ called interchange generator, which is of type:

   
   which can be represented using string diagrams by:
   

2. (ii) for every pair of 3-generators $A,B \in \textsf{P}_3$ and $e,e',h,h' \in \textsf{P}^*_1$ and $\chi \in \textsf{P}^*_2$ as in

   (6)

   
   a 4-generator of type $\Gamma \Rrightarrow \Delta$ , called independence generator, where
   \begin{equation*} \Gamma = ((e {\ast}_0 A {\ast}_0 h) {\ast}_1 \chi {\ast}_1 (e' {\ast}_0 \psi {\ast}_0 h')) {\ast}_2 ((e {\ast}_0 \phi' {\ast}_0 h) {\ast}_1 \chi {\ast}_1 (e' {\ast}_0 B {\ast}_0 h')) \end{equation*}
   and
   \begin{equation*} \Delta = ((e {\ast}_0 \phi {\ast}_0 h) {\ast}_1 \chi {\ast}_1 (e' {\ast}_0 B {\ast}_0 h')) {\ast}_2 ((e {\ast}_0 A {\ast}_0 h) {\ast}_1 \chi {\ast}_1 (e' {\ast}_0 \psi' {\ast}_0 h')) \end{equation*}
   and can be pictured as:
   

3. (iii) for all 0-composable $A,g,\beta$ with $A\in\textsf{P}_3$ , $g \in \textsf{P}^*_1$ , and $\beta\in\textsf{P}_2$ , respectively, and 0-composable $\alpha,g',B$ with $\alpha\in\textsf{P}_2$ , $g'\in\textsf{P}^*_1$ , and $B\in\textsf{P}_3$ , respectively, as on the first, resp. second line below

   (7)

   
   a 4-generator, called interchange naturality generator, respectively, of type:
   \begin{align*} ((A{\ast}_0 g{\ast}_0 h){\ast}_1(f'{\ast}_0 g{\ast}_0\beta)) {\ast}_2 X_{\phi',g {\ast}_0 \beta} &\Rrightarrow X_{\phi,g {\ast}_0 \beta} {\ast}_2 ((f{\ast}_0 g{\ast}_0\beta){\ast}_1(A{\ast}_0 g{\ast}_0 h')) \end{align*}
   and
   \begin{align*} ((\alpha{\ast}_0 g'{\ast}_0 h){\ast}_1(f'{\ast}_0 g'{\ast}_0 B)) {\ast}_2 X_{\alpha {\ast}_0 g',\psi'} &\Rrightarrow X_{\alpha {\ast}_0 g',\psi} {\ast}_2 ((f{\ast}_0 g'{\ast}_0 B){\ast}_1(\alpha{\ast}_0 g'{\ast}_0 h')) \end{align*}
   where the $X_{\chi_1,\chi_2}$ ’s appearing in the sources and targets will be defined below for any 0-composable $\chi_1,\chi_2 \in \textsf{P}^*_2$ ; the first kind of interchange naturality generator can be pictured by:
   

The 3-cells $X_{\phi,\psi} \in \textsf{P}^*_3$ , which are used in the above definition, generalize interchange generators to any pair of 0-composable 2-cells $\phi$ and $\psi$ . Their definition consists in a suitable composite of the generators $X_{\alpha,u,\beta}$ and is detailed below. Let us give an idea of the definition of those 3-cells on an example. Consider a Gray presentation $\textsf{Q}$ with

\begin{equation*}\textsf{Q}_0= \{{x}\},\quad \textsf{Q}_1 = \{{\bar1\colon x \rightarrow x}\} \quad\text{and}\quad \textsf{Q}_2 = \{{\tau\colon \bar1\Rightarrow\bar1}\}\end{equation*}

where $\tau$ is pictured by

. Then, the following sequence of “moves” is an admissible definition for $X_{\tau{\ast}_1\tau,\tau{\ast}_1\tau}$ :

(8)

Each “move” above is a 3-cell of the form $\phi{\ast}_1 X_{\tau,\text{id}_{x},\tau}{\ast}_1 \psi$ for some $\phi,\psi \in \textsf{Q}^*_2$ and where $X_{\tau, \text{id}_{x},\tau}$ is an interchange generator provided by the definition of Gray presentation. Another admissible sequence of moves is the following:

We see that there are multiple ways one can define the 3-cells $X_{\phi,\psi}$ based on the interchange generators of a Gray presentation $\textsf{P}$ . We will show in Proposition B.8 that, in the end, the choice does not matter, because all the possible definitions give rise to the same 3-cell in $\overline{\textsf{P}}$ . Still, we need to introduce a particular structure that allows us to represent all the possible definitions of the 3-cells $X_{\phi,\psi}$ and reason about them. This structure consists in a graph

associated with each pair of 0-composable 2-cells $\phi$ and $\psi$ in $\textsf{P}^*_2$ : intuitively, a vertex in this graph will correspond to an interleaving of the 2-generators of $\phi$ and $\psi$ , and an edge will correspond to a “move” as above, that is, an interchange generator $X_{\alpha,g,\beta}$ in context that exchanges two 2-generators $\alpha$ from $\phi$ and $\beta$ from $\psi$ , which appear consecutively in an interleaving of $\phi$ and $\psi$ . Given two 0-composable 2-cells:

\begin{equation*} \phi = \phi_1 \ast_1 \cdots \ast_1 \phi_k \in \textsf{P}^*_2 \qquad\text{and}\qquad \psi = \psi_1\ast_1 \cdots \ast_1 \psi_{k'} \in \textsf{P}^*_2\end{equation*}

with $\phi_i = f_i \ast_0 \alpha_i \ast_0 g_i$ and $\psi_j = f'_j \ast_0\alpha'_j \ast_0 g'_j$ for some $f_i,g_i,f'_j,g'_j \in \textsf{P}^*_1$ and $\alpha_i,\alpha'_j \in \textsf{P}_2$ , we define the graph

• whose vertices are the shuffles of the words $\textsf{l}_1 \ldots \textsf{l}_k$ and $\textsf{r}_1 \ldots \textsf{r}_{k'}$ on the alphabet:

  \begin{equation*} \Sigma_{\phi,\psi} = \{{\textsf{l}_1,\ldots,\textsf{l}_k,\textsf{r}_1,\ldots,\textsf{r}_{k'}}\}, \end{equation*}
  that is, words of length $k+k'$ which are order-preserving interleavings of the words $l_1\ldots l_k$ and $\textsf{r}_1 \ldots \textsf{r}_{k'}$ ,

• whose edges are of the form $\textsf{X}_{w,w'}\colon w \textsf{l}_i \textsf{r}_j w' \rightarrow w \textsf{r}_j \textsf{l}_i w'$ for some $i \in \mathbb{N}^*_k$ , $j \in \mathbb{N}^*_{k'}$ and some words $w,w' \in \Sigma^*_{\phi,\psi}$ such that , intuitively representing the local swaps one can do to move a letter $\textsf{l}_i$ to the right of a letter $\textsf{r}_j$ in a word.

Given $i,j,p,q\in \mathbb{N}$ with $0 \le i\le k$ , $0\le j \le k'$ , $0 \le p \le k-i+1$ , $0\le q \le k'-j+1$ , and a shuffle u of the words:

\begin{equation*} \textsf{l}_i \ldots \textsf{l}_{i+p-1} \quad\text{and}\quad \textsf{r}_j \ldots \textsf{r}_{j+q-1}{,}\end{equation*}

we define $[u]^{i,j}_{\phi,\psi} \in \textsf{P}^*_2$ (or simply $[u]^{i,j}$ ) by induction on p and q:

\begin{equation*} [u]^{i,j} = \begin{cases} (\phi_i \ast_0 \partial^+_1(\psi_j)) \ast_1 [u']^{i+1,j} & \text{if $u = \textsf{l}_i u'$,} \\[5pt] (\partial^+_1(\phi_i) \ast_0 \psi_j) \ast_1 [u']^{i,j+1} & \text{if $u = \textsf{r}_j u'$,} \\[5pt] \partial^+_1(\phi_i) \ast_0 \partial^+_1(\psi_j) & \text{if} u \text{is the empty word,} \end{cases}\end{equation*}

where, by convention, $\partial^+_1(\phi_0) = \partial^-_1(\phi_1)$ and $\partial^+_1(\psi_0) = \partial^-_1(\psi_1)$ . Note that the indices of $[u]^{i,j}$ are uniquely determined if u has at least an $\textsf{l}$ letter and an $\textsf{r}$ letter. Intuitively, the letters $\textsf{l}_i$ and $\textsf{r}_j$ correspond to the 2-cells $\phi_i \ast_0 (\!-\!)$ and $(\!-\!) \ast_0 \psi_j$ where the 1-cells $(\!-\!)$ are most of the time uniquely determined by the context, so that $[u]^{1,1}$ for

is an interleaving of the $\phi_i \ast_0 (\!-\!)$ and $(\!-\!) \ast_0 \psi_j$ . Now, given

\begin{gather*} \textsf{X}_{u,v}\colon u \textsf{l}_i\textsf{r}_j v \rightarrow u \textsf{r}_j \textsf{l}_i v \end{gather*}

in

, we define the 3-cell:

\begin{gather*} [\textsf{X}_{u,v}]_{\phi,\psi}\colon [u \textsf{l}_i\textsf{r}_j v]^{1,1}_{\phi,\psi} \Rrightarrow [u \textsf{r}_j \textsf{l}_i v]^{1,1}_{\phi,\psi} \end{gather*}

in $\textsf{P}^*_3$ by

\begin{gather*} [\textsf{X}_{u,v}]_{\phi,\psi} = [u]^{1,1}_{\phi,\psi} \ast_1 (f_i \ast_0 X_{\alpha_i,g_i \ast_0 f'_j,\alpha'_j} \ast_0 g'_j) \ast_1 [v]^{i+1,j+1}_{\phi,\psi}{.}\end{gather*}

We thus obtain a functor:

where

is the free 1-category on

considered as a 1-prepolygraph, and where $[-]_{\phi,\psi}$ is defined by the mappings:

For example, for $\textsf{Q}$ defined as above and $\phi = \psi = \tau\ast_1 \tau$ , $[\textsf{l}_1 \textsf{l}_2 \textsf{r}_1 \textsf{r}_2]_{\phi,\psi}$ and $[\textsf{l}_1 \textsf{r}_1 \textsf{l}_2 \textsf{r}_2]_{\phi,\psi}$ are, respectively, the 2-cells of $\textsf{Q}^*_2$ :

and $[\textsf{X}_{\textsf{l}_1,\textsf{r}_2}]_{\phi,\psi}$ and $[\textsf{X}_{\textsf{l}_1\textsf{r}_1,\epsilon}]_{\phi,\psi}$ are, respectively, the 3-cells of $\textsf{Q}^*_3$ :

We write $\textsf{X}_{\phi,\psi}$ for the path:

defined by induction by:

\begin{equation*} u_1 = \textsf{l}_1 \ldots \textsf{l}_{k-1} \qquad\quad\text{and}\quad\qquad v_1 =\textsf{r}_2 \ldots \textsf{r}_{k'}\end{equation*}

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

\begin{equation*} \partial^+_0(\textsf{X}_{u_i,v_i}) = u_{i+1} \textsf{l}_p\textsf{r}_q v_{i+1} \qquad\text{with}\qquad v_{i+1} = \textsf{r}_{q+1} \ldots\textsf{r}_{k'} \textsf{l}_{p+1} \ldots \textsf{l}_k\end{equation*}

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

\begin{equation*} X_{\phi,\psi} = [\textsf{X}_{\phi,\psi}]_{\phi,\psi}. \end{equation*}

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

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

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

Our notion of Gray presentation is correct, in the sense that:

4.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\colon \phi\Rrightarrow\psi\in C_3$ , we have $F_1=F_2$ . By extension, a Gray presentation $\textsf{P}$ is coherent when the underlying (3,2)-precategory of the (3,2)-Gray category $\overline{\textsf{P}}^{\top}$ is coherent (remember that $\overline{\textsf{P}}$ is a lax Gray category by Theorem 3.3.2, which implies that $\overline{\textsf{P}}^{\top}$ is a (3,2)-Gray category by Proposition 3.2.1). Gray presentations $\textsf{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 $\textsf{P}$ of pseudomonoids given in Example 3.3.1, we do not expect the following parallel 3-cells:

(9)

to be equal in $\overline{\textsf{P}}^{\top}$ . For coherence, we need to add “tiles” in $\textsf{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\colon F_1 \Rrightarrow F_2$ for every pair of parallel 3-cells $F_1$ and $F_2$ of $\textsf{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 4.4, in the form of Theorem 4.4.5: we will see that it is enough to add a tile of the form:

for every critical branching $(S_1,S_2)$ of $\textsf{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-prepolygraphs 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:

\begin{equation*} F_1\colon \phi \Rrightarrow \phi_1 \quad\text{and}\quad F_2\colon \phi \Rrightarrow \phi_2\end{equation*}

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

\begin{equation*} G_1\colon \phi_1 \Rrightarrow \psi \in C_3 \quad\text{and}\quad G_2\colon \phi_2 \Rrightarrow \psi \in C_3\end{equation*}

of C such that $F_1 \ast_2 G_1 = F_2 \ast_2 G_2$ :

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

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

\begin{equation*} F = G_1^{{-}1} {\ast}_2 H_1 {\ast}_2 \cdots {\ast}_2 {G_k}^{{-}1} {\ast}_2 H_k \end{equation*}

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

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'\colon \phi_{k-1} \rightarrow \psi_{k}$ and $H_{k}'\colon \phi_{k} \rightarrow \psi_{k}$ with

By induction, the morphism:

\begin{equation*} G_1^{{-}1} {\ast}_2 H_1 {\ast}_2 \cdots {\ast}_2 {G_{k-2}}^{{-}1} {\ast}_2 H_{k-2} {\ast}_2 {G_{k-1}}^{{-}1} {\ast}_2 (H_{k-1} {\ast}_2 G_{k}') \end{equation*}

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

\begin{equation*} F = G {\ast}_2 {H}^{{-}1} {\ast}_2 {H_k'}^{{-}1} = G {\ast}_2 {(H_k' {\ast}_2 H)}^{{-}1} \end{equation*}

which is of the wanted form.

Starting from a confluent 3-precategory, we have the following simple criterion to deduce the coherence of the associated (3,2)-precategory:

Proof. Let $F_1,F_2\colon \phi \Rrightarrow \phi' \in C^{\top}_3$ . By Proposition 4.1.1, for $i \in \{{1,2}\}$ , we have $F_i = G_i {\ast}_2 {H_i}^{-1}$ for some $\psi_i \in C_2$ , $G_i \colon \phi \Rrightarrow \psi_i \in C_3$ and $H_i \colon \phi' \Rrightarrow \psi_i \in C_3$ , as in

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

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

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

4.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 $\textsf{P}$ , a rewriting step of $\textsf{P}$ is a 3-cell $S\in \textsf{P}^*_3$ of the form:

\begin{equation*} \lambda {\ast}_1 (l {\ast}_0 A {\ast}_0 r) {\ast}_1 \rho\end{equation*}

for some $l,r \in \textsf{P}^*_1$ , $\lambda,\rho \in \textsf{P}^*_2$ , and $A \in\textsf{P}_3$ , with l,A,r 0-composable and $\lambda,l {\ast}_0 A {\ast}_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\colon \phi \Rrightarrow \phi'$ in $\textsf{P}^*_3$ . Such a rewriting path has a length $|F| \in \mathbb{N}$ which is defined as in Section 2.8. Also, by Theorem 2.8.3, it can be uniquely written as a composite of rewriting steps $S_1{\ast}_2 \cdots{\ast}_2 S_{|F|}$ , since rewriting steps are exactly three-dimensional whiskers. Given $\phi,\psi \in \textsf{P}^*_2$ , $\phi$ rewrites to $\psi$ when there exists a rewriting path $F\colon \phi \Rrightarrow \psi$ . A normal form is a 2-cell $\phi \in \textsf{P}^*_2$ such that for all $\psi \in \textsf{P}^*_2$ and $F\colon\phi\Rrightarrow \psi$ , we have $F = \text{id}_{\phi}$ . $\textsf{P}$ is terminating when there does not exist an infinite sequence of rewriting steps $F_i\colon \phi_i\Rrightarrow \phi_{i+1}$ for $i \ge 0$ ;

A branching is a pair rewriting paths $F_1\colon \phi\Rrightarrow \phi_1$ and $F_2\colon \phi\Rrightarrow \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\colon \phi_1 \Rrightarrow\psi$ and $G_2\colon \phi_2 \Rrightarrow \psi$ ; moreover, given a congruence

on $\textsf{P}^*$ , if we have that

, as in

we say that the branching is confluent (for

).

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

The analogs 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 (Baader and Nipkow Reference Baader and Nipkow1999, Lem. 2.7.2, for example) can be directly adapted in order to show that:

Proof. Let

be a rewriting system which is convergent. Let $\Rrightarrow^+ \subseteq \textsf{P}^*_2 \times \textsf{P}^*_2$ be the partial order such that $\phi \Rrightarrow^+ \psi$ if there exists a rewriting path $F\colon \phi \Rrightarrow \psi \in \textsf{P}^*_3$ with $|F| > 0$ . Since the underlying rewriting system is terminating, $\Rrightarrow^+$ is well founded. Thus, we can prove the theorem by induction on $\Rrightarrow^+$ . Suppose given a branching $F_1\colon \phi\Rrightarrow \phi_1 \in \textsf{P}^*_3$ and $F_2\colon \phi\Rrightarrow \phi_2 \in \textsf{P}^*_3$ . If $|F_1|=0$ or $|F_2|=0$ , then the branching is confluent. Otherwise, $F_i = S_i {\ast}_2 F_i'$ with $S_i\colon \phi \Rrightarrow \phi_i'$ a rewriting step and $F_i'\colon \phi_i' \Rrightarrow \phi_i$ a rewriting path for $i \in \{{1,2}\}$ . Since the rewriting system is locally confluent, there are $\psi \in \textsf{P}^*_2$ and rewriting paths $G_i\colon \phi_i' \Rrightarrow \psi$ for $i \in \{{1,2}\}$ such that

. Since the rewriting system is terminating and

is stable by composition, by composing the $G_i$ ’s with a path $G\colon \psi \Rrightarrow \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 \colon \phi_i \Rrightarrow \psi_i'$ and $F_i''\colon \psi \Rrightarrow \psi_i'$ such that

for $i \in \{{1,2}\}$ . Since $\psi$ is in normal form, $F_i'' = \text{id}_{\psi}$ and we have $H_i\colon \phi_i \Rrightarrow \psi$ for $i \in \{{1,2}\}$ as in

Moreover,

Theorem 4.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 4.1.2 for showing the coherence of Gray presentations.

Lemma 4.2.2. Given a convergent rewriting system

and two rewriting paths $F_1,F_2\colon \phi \Rrightarrow \phi' \in \textsf{P}^*_3$ as in

there exists $G\colon \phi' \Rrightarrow \psi \in \textsf{P}^*_3$ such that

, that is,

Note that, in Lemma 4.2.2, we do not necessarily have

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.

4.3 Termination

Here, we show a termination criterion for rewriting systems 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 $\textsf{P}$ is a well-founded partial order $<$ on $\textsf{P}^*_2$ such that:

• given $A\colon \phi\Rrightarrow\phi' \in \textsf{P}_3$ , we have $\phi > \phi'$ ,

• given $l,r \in \textsf{P}^*_1$ and parallel $\phi,\phi' \in \textsf{P}^*_2$ such that $l,\phi,r$ are 0-composable and $\phi > \phi'$ , we have

  \begin{equation*} l \ast_0 \phi \ast_0 r > l \ast_0 \phi' \ast_0 r{,} \end{equation*}

• given 1-composable $\lambda,\phi,\rho \in \textsf{P}^*_2$ , and $\phi' \in \textsf{P}^*_2$ parallel to $\phi$ such that $\phi > \phi'$ , we have

  \begin{equation*} \lambda \ast_1 \phi \ast_1 \rho > \lambda \ast_1 \phi' \ast_1 \rho{.} \end{equation*}

The termination criterion is then:

Proof. The definition of a reduction order implies that, given a rewriting step $\lambda {\ast}_1 (l {\ast}_0 A {\ast}_0 r) {\ast}_1 \rho$ with $l,r \in \textsf{P}^*_1$ , $\lambda,\rho \in \textsf{P}^*_2$ and $A\colon \phi \Rrightarrow \phi' \in \textsf{P}_3$ suitably composable, we have

\begin{equation*} \lambda {\ast}_1 (l {\ast}_0 \phi {\ast}_0 r) {\ast}_1 \rho > \lambda {\ast}_1 (l {\ast}_0 \phi' {\ast}_0 r) {\ast}_1 \rho. \end{equation*}

So, given a sequence of 2-composable rewriting steps $(F_i)_{i < k}$ , where $k \in \mathbb{N} \cup \{{\infty}\}$ , $F_i\colon \phi_i \Rrightarrow \phi_{i+1} \in \textsf{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 is terminating.

In order to build a reduction order for a Gray presentation $\textsf{P}$ , we have to build in particular a reduction order for the subset of $\textsf{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 $\mathrel{<_{\omega}}$ where

\begin{equation*} (a_1,\ldots,a_k) \mathrel{<_{\omega}} (b_1,\ldots,b_l)\end{equation*}

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 $\mathrel{<_{\omega}}$ is well founded. Given a 2-prepolygraph $\textsf{P}$ , there is a function ${\mathrm{N_{int}}}\colon \textsf{P}^*_2 \rightarrow\mathbb{N}^{<\omega}$ such that, given $\phi \in \textsf{P}^*_2$ , decomposed uniquely (using Theorem 2.8.3) as:

\begin{equation*} \phi = (l_1 \ast_0 \alpha_1 \ast_0 r_1) \ast_1 \cdots \ast_1 (l_k \ast_0 \alpha_k \ast_0 r_k)\end{equation*}

for some $k \in \mathbb{N}$ , $l_i,r_i \in \textsf{P}^*_1$ and $\alpha_i \in \textsf{P}_2$ for $i\in \{{1,\ldots,k}\}$ , ${\mathrm{N_{int}}}(\phi)$ is defined by:

\begin{equation*} {\mathrm{N_{int}}}(\phi) = (|l_k|,|l_{k-1}|,\ldots,|l_1|).\end{equation*}

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

Given a Gray presentation $\textsf{P}$ , we say that $\textsf{P}$ is positive when $|\partial^+_1(\alpha)| > 0$ for all $\alpha \in \textsf{P}_2$ . Under positiveness, the order $\mathrel{<_{\text{int}}}$ can be considered as a reduction order for the subset of 3-generators of a Gray presentation made of interchangers, as in

1. (i) for every $\alpha,\beta \in \textsf{P}_2$ and $f \in \textsf{P}^*_1$ such that $\alpha,f,\beta$ are 0-composable,

   \begin{equation*} \partial^-_2(X_{\alpha,f,\beta}) \mathrel{>_{\text{int}}} \partial^+_2(X_{\alpha,f,\beta}){,} \end{equation*}

2. (ii) for $\phi,\phi' \in \textsf{P}^*_2$ and $l,r \in \textsf{P}^*_1$ such that $l,\phi,r$ are 0-composable, if $\phi \mathrel{>_{\text{int}}} \phi'$ , then

   \begin{equation*} l \ast_0 \phi \ast_0 r \mathrel{>_{\text{int}}} l \ast_0 \phi' \ast_0 r{,} \end{equation*}

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

   \begin{equation*} \lambda \ast_1 \phi \ast_1 \rho \mathrel{>_{\text{int}}} \lambda \ast_1 \phi' \ast_1 \rho{.} \end{equation*}

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

\begin{equation*} X_{\alpha,f,\beta}\colon (\alpha {\ast}_0 f {\ast}_0 \partial^-_1(\beta)) {\ast}_1 (\partial^+_1(\alpha) {\ast}_0 f {\ast}_0 \beta) \Rrightarrow (\partial^-_1(\alpha) {\ast}_0 f {\ast}_0 \beta) {\ast}_1 (\alpha {\ast}_0 f {\ast}_0 \partial^+_1(\beta)) \end{equation*}

Then, we have

\begin{equation*} {\mathrm{N_{int}}}(\partial^-_2(X_{\alpha,f,\beta})) = (|\partial^+_1(\alpha)| + |f|,0) \qquad\text{and}\qquad {\mathrm{N_{int}}}(\partial^+_2(X_{\alpha,f,\beta})) = (0,|\partial^-_1(\alpha)| + |f|). \end{equation*}

Since $\textsf{P}$ is positive, we have $|\partial^+_1(\alpha)| > 0$ so that $\mathop{\mathrm{N_{int}}}(\partial^-_2(X_{\alpha,f,\beta})) \mathrel{>_{\text{int}}} \mathop{\mathrm{N_{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 {\ast}_0 - {\ast}_0 r$ and $\lambda {\ast}_1 - {\ast}_1 \rho$ on these representations and the definition of $\mathop{\mathrm{N_{int}}}$ .

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 $\textsf{P}$ where $\textsf{P}_0$ and $\textsf{P}_1$ have one element and $\textsf{P}_2$ has two 2-generators

and

, there are 2-cells of ${\textsf{P}^*}$ with “floating bubbles” which induce infinite reduction sequence with interchange generators as the following one:

4.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 Baader and Nipkow (Reference Baader and Nipkow1999, Sec. 6.2) for details. Note that we used this result earlier in the proof of Lemma 2.8.2.

Here, we show a similar result for rewriting on Gray presentations (introduced in Section 3.3). For this purpose, we give a definition of critical branchings which is similar to term rewriting systems, that is, 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 $\textsf{P}$ be a 3-prepolygraph. Given a local branching $(S_1\colon \phi\Rrightarrow \phi_1,S_2\colon \phi \Rrightarrow \phi_2)$ of $\textsf{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

  \begin{equation*} S_i=\lambda\ast_1(l\ast_0 S'_i\ast_0 r)\ast_1\rho \end{equation*}
  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

  \begin{align*} S_1&=((l_1{\ast}_0 A_1{\ast}_0 r_1){\ast}_1\chi{\ast}_1(l_2{\ast}_0\phi_2{\ast}_0 r_2)) \end{align*}
  and
  \begin{align*} S_2&=((l_1{\ast}_0\phi_1{\ast}_0 r_1){\ast}_1\chi{\ast}_1(l_2{\ast}_0 A_2{\ast}_0 r_2)) \end{align*}
  for some $l_i,r_i \in \textsf{P}^*_1$ and $A_i\colon \phi_i \Rrightarrow \phi'_i \in \textsf{P}_3$ for $i \in \{{1,2}\}$ and $\chi \in \textsf{P}^*_2$ .

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

• natural when

  \begin{equation*} S_1=((A{\ast}_0 g{\ast}_0 h){\ast}_1(f'{\ast}_0 g{\ast}_0\psi)) \end{equation*}
  for some $A\colon \phi\Rrightarrow\phi' \colon f \Rightarrow f' \in \textsf{P}_3$ , $\psi\colon h \Rightarrow h'\in \textsf{P}^*_2$ and $g \in \textsf{P}^*_1$ , and
  \begin{equation*} S_2 = [\textsf{X}_{u,v}]_{\phi,g {\ast}_0 \psi} \quad\text{with}\quad u = \textsf{l}_1 \ldots \textsf{l}_{|\phi| - 1} \quad\text{and}\quad v = \textsf{r}_2 \ldots \textsf{r}_{|\psi|} \end{equation*}
  and similarly for the situation on the second line of (3),

• 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 $\textsf{Q}$ and we write for $(\textsf{Q}_{\le }3,\sim^{\textsf{Q}})$ . Our next goal is to show an adapted version of the critical pair lemma. We start by two technical lemmas:

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 \textsf{P}^*_3$ , $l,r \in \textsf{P}^*_1$ and $\lambda,\rho \in \textsf{P}^*_2$ such that $S_i = \lambda {\ast}_1 (l {\ast}_0 S'_i {\ast}_0 r) {\ast}_1 \rho$ for $i \in \{{1,2}\}$ , such that $l,r,\lambda,\rho$ are not all identities. Since

\begin{equation*} |\partial^-_1(S_1)| = |l| + |\partial^-_1(S'_1)| + |r| \quad\text{and}\quad |\partial^-_2(S_1)| = |\lambda| + |\partial^-_2(S'_1)| + |\rho|, \end{equation*}

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

The critical pair lemma adapted to our context is then:

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

Note that Theorem 4.4.4 requires the rewriting system 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 (Knuth and Bendix Reference Knuth and Bendix1970) (see also Baader and Nipkow Reference Baader and Nipkow1999, 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 , 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 Guiraud et al. (Reference Guiraud, Malbos and Mimram2013), where it is called the Knuth–Bendix–Squier completion procedure.

Our coherence theorem implies a coherence criterion similar to the ones shown by Squier et al. (Reference Squier, Otto and Kobayashi1994, Thm. 5.2) and Guiraud and Malbos (Reference Guiraud and Malbos2009, Prop. 4.3.4), which states that adding a tile for each critical branching is enough to ensure coherence:

Note that, in Theorem 4.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 (Guiraud and Malbos Reference Guiraud and Malbos2009; Lafont Reference Lafont2003).

The proof of Theorem 4.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.

5.1 Pseudomonoids

In Example 3.3.1, we introduced a Gray presentation $\textsf{P}$ for the theory of pseudomonoids. The set $\textsf{P}_4$ of 4-generators contains only the required ones in a Gray presentation so that we do not expect $\textsf{P}$ to be coherent (see (9) for an example). We will show that the rewriting system is terminating and thus, Theorem 4.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 4.4.6, which is constructive: we obtain, up to symmetrical branchings, five critical branchings:

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:

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

As claimed above, in order to deduce coherence, we need to show the termination of $\textsf{PMon}$ . For this purpose, we use the tools of Section 4 and build a reduction order. We split the task in two and define a first order that handles the termination of the $\textsf{A},\textsf{L},\textsf{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 Lafont (Reference Lafont1992). Given $n \in \mathbb{N}$ , we write $<_{\text{ex}}^1$ for the partial order on $\mathbb{N}^n$ such that, given $a,b \in \mathbb{N}^n$ , $a <_{\text{ex}}^1 b$ when $a_i \le b_i$ for all $i \in \{{1,\ldots,n}\}$ and there exists $j \in \{{1,\ldots,n}\}$ such that $a_{j} < b_{j}$ . Let MFun be the 2-precategory

• which has only one 0-cell: $MFun_0 = \{{\ast}\}$ ,

• whose 1-cells are the natural numbers: $MFun_1 = \mathbb{N}$ ,

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

  \begin{equation*} \phi\colon (\mathbb{N}^m,<_{\text{ex}}^1) \rightarrow (\mathbb{N}^n,<_{\text{ex}}^1). \end{equation*}

Moreover, $\text{id}_{\ast}= 0$ and composition of 1-cells is given by addition. Given $m \in MFun_1$ , $\text{id}_{m}$ is the identity function on $\mathbb{N}^m$ , and given $m,n,k,k' \in \mathbb{N}$ and $\chi \colon k \rightarrow k' \in MFun_2$ , the 2-cell:

\begin{equation*} m {\ast}_0 \chi {\ast}_0 n \colon {m+k+n} \Rightarrow {m+k'+n}\end{equation*}

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

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

and, given $m,n,p \in \mathbb{N}$ , $\phi \colon m \Rightarrow n \in MFun_2$ and $\psi \colon n \Rightarrow p\in MFun_2$ , $\phi {\ast}_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\colon m\Rightarrow n,\psi\colon m'\Rightarrow n' \in MFun$ , we write $\phi <_{\text{ex}}^2 \psi$ when $m = m'$ , $n = n'$ and $\phi(x)<_{\text{ex}}^1 \psi(x)$ for all $x \in \mathbb{N}^m$ . We have that:

Proof. We define a function $N\colon MFun_2 \rightarrow \mathbb{N}$ by:

\begin{equation*} N(\phi) = \phi(z)_1 + \cdots + \phi(z)_n \qquad \mathrm{for} \phi\colon m \Rightarrow n \in \mathrm{MFun}_2 \end{equation*}

where $z = (0,\ldots,0)$ . Now, if $\psi\colon m \Rightarrow n \in MFun_2$ is such that $\psi <_{\text{ex}}^2 \phi$ , then $\psi(z) <_{\text{ex}}^1 \phi(z)$ so that $N(\psi)<N(\phi)$ . Thus, $<_{\text{ex}}^2$ on $MFun_2$ is well founded.

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

1. (i) $m {\ast}_0 \phi {\ast}_0 n >_{\text{ex}}^2 m {\ast}_0 \phi' {\ast}_0 n$ ,

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

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

\begin{equation*} (m \ast_0 \phi \ast_0 n)(x) >_{\text{ex}}^1 (m \ast_0 \phi' \ast_0 n)(x){.} \end{equation*}

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

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

\begin{equation*} f_\mu\colon \mathbb{N}^2 \rightarrow \mathbb{N}^1 \qquad\qquad f_\eta \colon \mathbb{N}^0 \rightarrow \mathbb{N}^1\end{equation*}

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

1. (i) $F(\partial^-_2(\textsf{A})) >_{\text{ex}}^2 F(\partial^+_2(\textsf{A}))$ ,

2. (ii) $F(\partial^-_2(\textsf{L})) >_{\text{ex}}^2 F(\partial^+_2(\textsf{L}))$ ,

3. (iii) $F(\partial^-_2(\textsf{R})) >_{\text{ex}}^2 F(\partial^+_2(\textsf{R}))$ ,

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

Proof. Let $\phi = F(\partial^-_2(\textsf{A}))$ and $\psi = F(\partial^+_2(\textsf{A}))$ . By calculations, we get that

\begin{equation*} \phi(x,y,z) = (4x + 2y + z + 3) \qquad\text{and}\qquad \psi(x,y,z) = (2x + 2y + z + 1) \end{equation*}

for $x,y,z \in \mathbb{N}$ , so $\phi(x,y,z) >_{\text{ex}}^1 \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.