<figure><img src="image_20.png" /><figcaption>Figure 7: The rules (≈-L) and (≈-R) for ≈_2</figcaption></figure>

**Source and target of contexts** Let $n \in \mathbb{N} \cup \{\omega\}$ and $C \in \mathbf{Cat}_n$. Given $m \in \mathbb{N}_n^*$, an $m$-type $(u, u')$ and an $m$-context $E = (l, F, r)$ of type $(u, u')$ of $C$, the source and the target of $E$ are respectively the $(m-1)$-cells

$$ \partial_{m-1}^{-}(E) = \partial_{m-1}^{-}(l) \quad \text{and} \quad \partial_{m-1}^{+}(E) = \partial_{m-1}^{+}(r). $$

When $m > 1$, for $\epsilon \in \{-, +\}$, we easily verify that

$$ \partial_{m-2}^{\epsilon} \circ \partial_{m-1}^{-}(E) = \partial_{m-2}^{\epsilon} \circ \partial_{m-1}^{+}(E). $$

The operations $\partial^{-}, \partial^{+}$ on $m$-contexts extend to $m$-context classes since they are compatible with the $\approx_m$ relation. Given $i \in \mathbb{N}_{m-1}$ and $\epsilon \in \{-, +\}$ and an $m$-context $E$ (resp. an $m$-context class $F$), we write $\partial_i^{\epsilon}(E)$ for $\partial_i^{\epsilon} \circ \partial_{m-1}^{\epsilon}(E)$ (resp. $\partial_i^{\epsilon} \circ \partial_{m-1}^{\epsilon}(F)$). Thus, for $i \in \mathbb{N}_{n-1}$, we can extend the notion of $i$-composable sequences of globes of globular sets to sequences $X_1, \dots, X_l$ for some $l \in \mathbb{N}^*$ where $X_s$ is either an $m$-context, an $m$-context class, or a cell of $C$ for $s \in \mathbb{N}_l^*$, and say that $X_1, \dots, X_l$ is $i$-composable when $\partial_i^{+}(X_s) = \partial_i^{-}(X_{s+1})$ for $s \in \mathbb{N}_{l-1}^*$.

**Composition operations** Let $n \in \mathbb{N} \cup \{\omega\}$ and $C \in \mathbf{Cat}_n$. Given $i, m \in \mathbb{N}_n$ with $i < m$, an $m$-context $E = (l, F, r)$ of some $m$-type $(u, u')$ of $C$, and $v \in C_{i+1}$, if $(v, E)$ is $i$-composable, we define an $m$-context $v \bullet_i E$ by induction on $m - i$ with

$$ v \bullet_i E = \begin{cases} (v \bullet_i l, F, r) & \text{if } i + 1 = m, \\ (v \bullet_i l, v \bullet_i F, v \bullet_i r) & \text{if } i + 1 < m, \end{cases} $$

and, since it can be verified that the $\bullet_i$ operation is compatible with $\approx_m$, we extend the operation on $m$-context classes and put $v \bullet_i [[E]] = [[v \bullet_i E]]$. Similarly, if $(E, v)$ is $i$-composable, we define an $m$-context $E \bullet_i v$ using an induction on $m - i$ by

$$ E \bullet_i v = \begin{cases} (l, F, r \bullet_i v) & \text{if } i + 1 = m, \\ (l \bullet_i v, F \bullet_i v, r \bullet_i v) & \text{if } i + 1 < m, \end{cases} $$

and we put $[[E]] \bullet_i v = [[E \bullet_i v]]$. These composition operations satisfy properties similar to strict $(n+1)$-categories (unitality, associativity, condition (E), etc.).
<figure><img src="image_24.png" /><figcaption>Figure 7: The rules (≈-L) and (≈-R) for ≈_2</figcaption></figure>

**Source and target of contexts** Let $n \in \mathbb{N} \cup \{\omega\}$ and $C \in \mathbf{Cat}_n$. Given $m \in \mathbb{N}_n^*$, an $m$-type $(u, u')$ and an $m$-context $E = (l, F, r)$ of type $(u, u')$ of $C$, the source and the target of $E$ are respectively the $(m-1)$-cells

$$ \partial_{m-1}^{-}(E) = \partial_{m-1}^{-}(l) \quad \text{and} \quad \partial_{m-1}^{+}(E) = \partial_{m-1}^{+}(r). $$

When $m > 1$, for $\epsilon \in \{-, +\}$, we easily verify that

$$ \partial_{m-2}^{\epsilon} \circ \partial_{m-1}^{-}(E) = \partial_{m-2}^{\epsilon} \circ \partial_{m-1}^{+}(E). $$

The operations $\partial^{-}, \partial^{+}$ on $m$-contexts extend to $m$-context classes since they are compatible with the $\approx_{m}$ relation. Given $i \in \mathbb{N}_{m-1}$ and $\epsilon \in \{-, +\}$ and an $m$-context $E$ (resp. an $m$-context class $F$), we write $\partial_{i}^{\epsilon}(E)$ for $\partial_{i}^{\epsilon} \circ \partial_{m-1}^{\epsilon}(E)$ (resp. $\partial_{i}^{\epsilon} \circ \partial_{m-1}^{\epsilon}(F)$). Thus, for $i \in \mathbb{N}_{n-1}$, we can extend the notion of $i$-composable sequences of globes of globular sets to sequences $X_1, \dots, X_l$ for some $l \in \mathbb{N}^*$ where $X_s$ is either an $m$-context, an $m$-context class, or a cell of $C$ for $s \in \mathbb{N}_l^*$, and say that $X_1, \dots, X_l$ is $i$-composable when $\partial_{i}^{+}(X_s) = \partial_{i}^{-}(X_{s+1})$ for $s \in \mathbb{N}_{l-1}^*$.

**Composition operations** Let $n \in \mathbb{N} \cup \{\omega\}$ and $C \in \mathbf{Cat}_n$. Given $i, m \in \mathbb{N}_n$ with $i < m$, an $m$-context $E = (l, F, r)$ of some $m$-type $(u, u')$ of $C$, and $v \in C_{i+1}$, if $(v, E)$ is $i$-composable, we define an $m$-context $v \bullet_i E$ by induction on $m - i$ with

$$ v \bullet_i E = \begin{cases} (v \bullet_i l, F, r) & \text{if } i + 1 = m, \\ (v \bullet_i l, v \bullet_i F, v \bullet_i r) & \text{if } i + 1 < m, \end{cases} $$

and, since it can be verified that the $\bullet_i$ operation is compatible with $\approx_m$, we extend the operation on $m$-context classes and put $v \bullet_i [[E]] = [[v \bullet_i E]]$. Similarly, if $(E, v)$ is $i$-composable, we define an $m$-context $E \bullet_i v$ using an induction on $m - i$ by

$$ E \bullet_i v = \begin{cases} (l, F, r \bullet_i v) & \text{if } i + 1 = m, \\ (l \bullet_i v, F \bullet_i v, r \bullet_i v) & \text{if } i + 1 < m, \end{cases} $$

and we put $[[E]] \bullet_i v = [[E \bullet_i v]]$. These composition operations satisfy properties similar to strict $(n+1)$-categories (unitality, associativity, condition (E), etc.).
**B.3 A description of free extensions** We now introduce a concrete description of the free extension functor $-[−]$ of strict categories using context and context classes. It is based on the intermediate notion of categorical action, which encodes the structure of context and context classes with regard to the underlying $n$-category. On the one hand, the cells of free categorical action on a cellular extension will then be characterized as formally applied context classes on the generators. On the other hand, the cells of the free strict category on a categorical action will be characterized as adequately quotiented sequences of the cells of the categorical action. This will result in the characterization of cells of free extensions as quotiented sequences of formally applied context classes.

**Categorical actions** Let $n \in \mathbb{N}$. An $n$-categorical action is the data of an $n$-cellular extension $(C, C_{n+1})$ together with, for $k \in \mathbb{N}_n^*$, composition operations

$$ \bullet_{k,n+1}: C_k \times_{k-1} C_{n+1} \to C_{n+1} \quad \text{and} \quad \bullet_{n+1,k}: C_{n+1} \times_{k-1} C_k \to C_{n+1} $$

satisfying the axioms given below. We extend the convention used for precategories, meaning that, for $i, k, l \in \mathbb{N}_{n+1}$ with $i = \min(k, l) - 1$ and $\max(k, l) = n + 1$, given $(u, v) \in C_k \times_i C_l$, we write $u \bullet_i v$ for $u \bullet_{k,l} v$. The axioms satisfied by $n$-categorical actions are then the following:

(A-i) for $i, k, l \in \mathbb{N}_{n+1}$ satisfying
$$ i = \min(k, l) - 1 \le n - 1 \quad \text{and} \quad \max(k, l) = n + 1, $$
and $(u, v) \in C_k \times_i C_l$ and $\epsilon \in \{-, +\}$,

$$ \partial_n^\epsilon(u \bullet_i v) = \begin{cases} u \bullet_i \partial_n^\epsilon(v) & \text{if } k < l, \\ \partial_n^\epsilon(u) \bullet_i v & \text{if } k > l, \end{cases} $$

(A-ii) for $i, k, l, m \in \mathbb{N}_{n+1}$ satisfying
$$ i = \min(k, l) - 1 = \min(l, m) - 1 \le n - 1 \quad \text{and} \quad \max(k, l, m) = n + 1, $$
and $(u, v, w) \in C_k \times_i C_l \times_i C_m,$
$$ (u \bullet_i v) \bullet_i w = u \bullet_i (v \bullet_i w), $$

(A-iii) for $i, j \in \mathbb{N}_{n-1}$ with $i < j$, $u_1, u_2 \in C_{i+1}$, $v_1, v_2 \in C_{j+1}$ and $w \in C_{n+1}$ such that $u_1, w, u_2$ are $i$-composable and $v_1, w, v_2$ are $j$-composable,

$$ u_1 \bullet_i (v_1 \bullet_j w \bullet_j v_2) \bullet_i u_2 = (u_1 \bullet_i v_1 \bullet_i u_2) \bullet_j (u_1 \bullet_i w \bullet_i u_2) \bullet_j (u_1 \bullet_i v_2 \bullet_i u_2), $$

(A-iv) for $i, k, l \in \mathbb{N}_{n+1}^*$ satisfying
$$ i = \min(k, l) - 1 \le n - 1 \quad \text{and} \quad \max(k, l) = n + 1, $$
and $(u, v) \in C_k \times_{i-1} C_l,$
$$ (u \bullet_{i-1} \partial_i^-(v)) \bullet_i (\partial_i^+(u) \bullet_{i-1} v) = (\partial_i^-(u) \bullet_{i-1} v) \bullet_i (u \bullet_{i-1} \partial_i^+(v)). $$

Axioms (A-i), (A-ii) and (A-iii) above closely match Axioms (P-ii), (P-iv) and (P-v) of precategories. Axiom (A-iv) is analogous to the condition (E) satisfied by precategories derived from strict categories (c.f. Appendix B.1). An $n$-categorical action morphism between $(C, C_{n+1})$ and $(D, D_{n+1})$ is a morphism of $n$-cellular extension

$$ (F, f): (C, C_{n+1}) \to (D, D_{n+1}) \in \mathbf{Cat}_n^+ $$

which is moreover commutes with the $\bullet_{k,n+1}$ and $\bullet_{n+1,k}$ operations for $k \in \mathbb{N}_n^*$. We write $\mathbf{Cat}_n^\Lambda$ for the category of $n$-categorical actions.
**B.3 A description of free extensions** We now introduce a concrete description of the free extension functor $-[–]$ of strict categories using context and context classes. It is based on the intermediate notion of categorical action, which encodes the structure of context and context classes with regard to the underlying $n$-category. On the one hand, the cells of free categorical action on a cellular extension will then be characterized as formally applied context classes on the generators. On the other hand, the cells of the free strict category on a categorical action will be characterized as adequately quotiented sequences of the cells of the categorical action. This will result in the characterization of cells of free extensions as quotiented sequences of formally applied context classes.

**Categorical actions** Let $n \in \mathbb{N}$. An $n$-categorical action is the data of an $n$-cellular extension $(C, C_{n+1})$ together with, for $k \in \mathbb{N}_n^*$, composition operations

$$ \bullet_{k,n+1}: C_k \times_{k-1} C_{n+1} \to C_{n+1} \quad \text{and} \quad \bullet_{n+1,k}: C_{n+1} \times_{k-1} C_k \to C_{n+1} $$

satisfying the axioms given below. We extend the convention used for precategories, meaning that, for $i, k, l \in \mathbb{N}_{n+1}$ with $i = \min(k, l) - 1$ and $\max(k, l) = n + 1$, given $(u, v) \in C_k \times_i C_l$, we write $u \bullet_i v$ for $u \bullet_{k,l} v$. The axioms satisfied by $n$-categorical actions are then the following:

(A-i) for $i, k, l \in \mathbb{N}_{n+1}$ satisfying
$$ i = \min(k, l) - 1 \le n - 1 \quad \text{and} \quad \max(k, l) = n + 1, $$
and $(u, v) \in C_k \times_i C_l$ and $\epsilon \in \{-, +\}$,

$$ \partial_n^\epsilon(u \bullet_i v) = \begin{cases} u \bullet_i \partial_n^\epsilon(v) & \text{if } k < l, \\ \partial_n^\epsilon(u) \bullet_i v & \text{if } k > l, \end{cases} $$

(A-ii) for $i, k, l, m \in \mathbb{N}_{n+1}$ satisfying
$$ i = \min(k, l) - 1 = \min(l, m) - 1 \le n - 1 \quad \text{and} \quad \max(k, l, m) = n + 1, $$
and $(u, v, w) \in C_k \times_i C_l \times_i C_m$,
$$ (u \bullet_i v) \bullet_i w = u \bullet_i (v \bullet_i w), $$

(A-iii) for $i, j \in \mathbb{N}_{n-1}$ with $i < j$, $u_1, u_2 \in C_{i+1}$, $v_1, v_2 \in C_{j+1}$ and $w \in C_{n+1}$ such that $u_1, w, u_2$ are $i$-composable and $v_1, w, v_2$ are $j$-composable,

$$ u_1 \bullet_i (v_1 \bullet_j w \bullet_j v_2) \bullet_i u_2 = (u_1 \bullet_i v_1 \bullet_i u_2) \bullet_j (u_1 \bullet_i w \bullet_i u_2) \bullet_j (u_1 \bullet_i v_2 \bullet_i u_2), $$

(A-iv) for $i, k, l \in \mathbb{N}_{n+1}^*$ satisfying
$$ i = \min(k, l) - 1 \le n - 1 \quad \text{and} \quad \max(k, l) = n + 1, $$
and $(u, v) \in C_k \times_{i-1} C_l$,
$$ (u \bullet_{i-1} \partial_i^-(v)) \bullet_i (\partial_i^+(u) \bullet_{i-1} v) = (\partial_i^-(u) \bullet_{i-1} v) \bullet_i (u \bullet_{i-1} \partial_i^+(v)). $$

Axioms (A-i), (A-ii) and (A-iii) above closely match Axioms (P-ii), (P-iv) and (P-v) of precategories. Axiom (A-iv) is analogous to the condition (E) satisfied by precategories derived from strict categories (c.f. Appendix B.1). An $n$-categorical action morphism between $(C, C_{n+1})$ and $(D, D_{n+1})$ is a morphism of $n$-cellular extension

$$ (F, f): (C, C_{n+1}) \to (D, D_{n+1}) \in \mathbf{Cat}_n^+ $$

which is moreover commutes with the $\bullet_{k,n+1}$ and $\bullet_{n+1,k}$ operations for $k \in \mathbb{N}_n^*$. We write $\mathbf{Cat}_n^\Lambda$ for the category of $n$-categorical actions.
**Free action on a cellular extension** There is a forgetful functor

$$ \mathcal{U}: \mathrm{Cat}_n^A \to \mathrm{Cat}_n^+ $$

which forgets the data of the $\bullet_{k,n+1}$ and $\bullet_{n+1,k}$ operations, for $k \in \mathbb{N}_n^*$. In this section, we use the formalism of contexts and contexts classes to define a left adjoint $(-, -^A)$ to the functor $\mathcal{U}: \mathrm{Cat}_n^A \to \mathrm{Cat}_n^+$: given an $n$-cellular extension $(C, X)$, the elements of $X^A$ will be the pairs $(g, F)$, where $g \in X$ and $F$ is an adapted $n$-context class, i.e., $X^A$ is the set of context classes formally applied to generators of $X$.

Let $n \in \mathbb{N}$. Given an $n$-cellular extension $(C, X)$, an $n$-categorical action $C[X]^A = (C, X^A)$ can be defined as follows: $X^A$ is the set of pairs $(g, F)$ with $g \in X$ and $F$ an $n$-context class of type $g$. The $n$-source and $n$-target of such a pair $(g, F)$ are defined respectively as the $n$-cells

$$ \partial_n^-( (g, F) ) = F[\mathrm{d}_n^-(g)] \quad \text{and} \quad \partial_n^+ ( (g, F) ) = F[\mathrm{d}_n^+(g)]. $$

and they equip $(C, X^A)$ with a structure of an $n$-cellular extension. We extend the operations $\bullet_i$ defined for $n$-context classes to such pairs by putting

$$ u \bullet_i (g, F) = (g, u \bullet_i F) \quad \text{and} \quad (g, F) \bullet_i v = (g, F \bullet_i v) $$

for $i \in \mathbb{N}_{n-1}$ and $u, v \in C_{i+1}$ such that $u, (g, F)$ and $(g, F), v$ are $i$-composable. We then have:

**Proposition B.3.1.** The operations $\bullet_i$ defined above equip $C[X]^A$ with the structure of an $n$-categorical action. It is the free categorical action relatively to the forgetful functor $\mathcal{U}$.

The construction $(C, X) \mapsto C[X]^A$ of the above proof uniquely extends to a functor

$$ -[-]^A: \mathrm{Cat}_n^+ \to \mathrm{Cat}_n^A $$

which is left adjoint to $\mathcal{U}$. Given $(H, h): (C, X) \to (D, Y)$ in $\mathrm{Cat}_n^+$, the $n$-categorical action morphism

$$ H[h]^A: C[X]^A \to D[Y]^A \in \mathrm{Cat}_n^A $$

is defined by $H[h]^A_i = H_i$ and $H[h]^A_{n+1}((g, F)) = (h(g), H(F))$ for $i \in \mathbb{N}_n$ and $(g, F) \in X^A$.

**Free $(n+1)$-categories on $n$-categorical actions** There is a forgetful functor

$$ \mathcal{U}': \mathrm{Cat}_{n+1} \to \mathrm{Cat}_n^A $$

which maps an $(n+1)$-category $C$ to an $n$-categorical action $(C_{\le n}, C_{n+1})$ by forgetting the $\bullet_n$ operation (where we consider the $(n+1)$-precategory structure of $C$). In this section, we describe explicitly a left adjoint $-[ - ]^A$ to this functor: given $(C, A) \in \mathrm{Cat}_n^A$, we show that the $(n+1)$-cells of $C[A]^A$ can be described as sequences of composable elements of $A$ that are adequately quotiented.

Let $n \in \mathbb{N}$ and $(C, A) \in \mathrm{Cat}_n^A$. We define the set $A^*$ of $n$-composable sequences (or simply, $n$-sequences) of $(C, A)$ as the set of terms of the form

$$ (u_1, \dots, u_k)^s $$

for some $k \in \mathbb{N}$ and $u_1, \dots, u_k \in A$ such that $u_1, \dots, u_k$ are $n$-composable. When $k = 0$, by convention, there is an empty sequence $( )^s_u$ for each $u \in C_n$. Given $v = (v_1, \dots, v_k)^s \in A^*$, we
**Free action on a cellular extension** There is a forgetful functor

$$ \mathcal{U}: \mathrm{Cat}_n^A \to \mathrm{Cat}_n^+ $$

which forgets the data of the $\bullet_{k,n+1}$ and $\bullet_{n+1,k}$ operations, for $k \in \mathbb{N}_n^*$. In this section, we use the formalism of contexts and contexts classes to define a left adjoint $(-, -^A)$ to the functor $\mathcal{U}: \mathrm{Cat}_n^A \to \mathrm{Cat}_n^+$: given an $n$-cellular extension $(C, X)$, the elements of $X^A$ will be the pairs $(g, F)$, where $g \in X$ and $F$ is an adapted $n$-context class, i.e., $X^A$ is the set of context classes formally applied to generators of $X$.

Let $n \in \mathbb{N}$. Given an $n$-cellular extension $(C, X)$, an $n$-categorical action $C[X]^A = (C, X^A)$ can be defined as follows: $X^A$ is the set of pairs $(g, F)$ with $g \in X$ and $F$ an $n$-context class of type $g$. The $n$-source and $n$-target of such a pair $(g, F)$ are defined respectively as the $n$-cells

$$ \partial_n^-( (g, F) ) = F[\mathrm{d}_n^-(g)] \quad \text{and} \quad \partial_n^+ ( (g, F) ) = F[\mathrm{d}_n^+(g)]. $$

and they equip $(C, X^A)$ with a structure of an $n$-cellular extension. We extend the operations $\bullet_i$ defined for $n$-context classes to such pairs by putting

$$ u \bullet_i (g, F) = (g, u \bullet_i F) \quad \text{and} \quad (g, F) \bullet_i v = (g, F \bullet_i v) $$

for $i \in \mathbb{N}_{n-1}$ and $u, v \in C_{i+1}$ such that $u, (g, F)$ and $(g, F), v$ are $i$-composable. We then have:

**Proposition B.3.1.** *The operations $\bullet_i$ defined above equip $C[X]^A$ with the structure of an $n$-categorical action. It is the free categorical action relatively to the forgetful functor $\mathcal{U}$.*

The construction $(C, X) \mapsto C[X]^A$ of the above proof uniquely extends to a functor

$$ -[-]^A: \mathrm{Cat}_n^+ \to \mathrm{Cat}_n^A $$

which is left adjoint to $\mathcal{U}$. Given $(H, h): (C, X) \to (D, Y)$ in $\mathrm{Cat}_n^+$, the $n$-categorical action morphism

$$ H[h]^A: C[X]^A \to D[Y]^A \in \mathrm{Cat}_n^A $$

is defined by $H[h]^A_i = H_i$ and $H[h]^A_{n+1}((g, F)) = (h(g), H(F))$ for $i \in \mathbb{N}_n$ and $(g, F) \in X^A$.

**Free $(n+1)$-categories on $n$-categorical actions** There is a forgetful functor

$$ \mathcal{U}': \mathrm{Cat}_{n+1} \to \mathrm{Cat}_n^A $$

which maps an $(n+1)$-category $C$ to an $n$-categorical action $(C_{\le n}, C_{n+1})$ by forgetting the $\bullet_n$ operation (where we consider the $(n+1)$-precategory structure of $C$). In this section, we describe explicitly a left adjoint $-[ - ]^A$ to this functor: given $(C, A) \in \mathrm{Cat}_n^A$, we show that the $(n+1)$-cells of $C[A]^A$ can be described as sequences of composable elements of $A$ that are adequately quotiented.

Let $n \in \mathbb{N}$ and $(C, A) \in \mathrm{Cat}_n^A$. We define the set $A^*$ of $n$-composable sequences (or simply, $n$-sequences) of $(C, A)$ as the set of terms of the form

$$ (u_1, \dots, u_k)^s $$

for some $k \in \mathbb{N}$ and $u_1, \dots, u_k \in A$ such that $u_1, \dots, u_k$ are $n$-composable. When $k = 0$, by convention, there is an empty sequence $( )^s_u$ for each $u \in C_n$. Given $v = (v_1, \dots, v_k)^s \in A^*$, we
<figure><img src="image_21.png" /><figcaption>Figure 8: A configuration of 2-cells $l, l', r, r', u, v$ such that $\mathcal{X}(l, l', r, r', u, v)$</figcaption></figure>

say that $k$ is the length of $v$ and we write $|v|$ for $k$. Moreover, we define a source $\partial_n^-(v)$ and a target $\partial_n^+(v)$ for $v$ by putting

$$ \partial_n^-(v) = \partial_n^-(v_1) \quad \text{and} \quad \partial_n^+(v) = \partial_n^+(v_k) $$

where, by convention, if $v = ()^s_u$ for some $u \in C_n$, then $\partial_n^-(v) = \partial_n^+(v) = u$. Thus, we obtain an $n$-cellular extension whose set of $(n+1)$-globes is $A^*$ and whose underlying $n$-category is $C$. We now define composition operations for the $n$-sequences. Given $i \in \mathbb{N}_{n-1}$, a cell $u \in C_{i+1}$ and an $n$-sequence $v = (v_1, \dots, v_l)^s \in A^*$ such that $u, v$ are $i$-composable, we put

$$ u \bullet_i v = (u \bullet_i v_1, \dots, u \bullet_i v_l)^s $$

where, by convention, if $v = ()^s_{\tilde{v}}$ for some $\tilde{v} \in C_n$, then $u \bullet_i v = ()^s_{u \bullet_i \tilde{v}}$. Given $n$-composable $n$-sequences $u = (u_1, \dots, u_k)^s$ and $v = (v_1, \dots, v_l)^s$ in $A^*$, we put

$$ u \bullet_n v = (u_1, \dots, u_k, v_1, \dots, v_l)^s. $$

In order to obtain a strict $(n+1)$-category from $C$ and $A^*$, we need to quotient $A^*$ so that the exchange condition (E) on precategories holds (c.f. Theorem B.1.1). For this purpose, we define a relation $\mathcal{X} \subseteq A^6$ such that, given $l, l', r, r', u, v \in A$, $\mathcal{X}(l, l', r, r', u, v)$ holds when $u, v$ are $(n-1)$-composable and the following equalities hold in $A$

$$ \begin{aligned} l &= u \bullet_{n-1} \partial_n^-(v) & r &= \partial_n^-(u) \bullet_{n-1} v \\ l' &= \partial_n^+(u) \bullet_{n-1} v & r' &= u \bullet_{n-1} \partial_n^+(v). \end{aligned} $$

In Figure 8, we illustrate this condition in the case of a 1-categorical action. Given top-level elements $l, l', r, r' \in A$, we write $\mathcal{X}(l, l', r, r')$ when there exist $u, v \in A$ such that we have $\mathcal{X}(l, l', r, r', u, v)$. We define an equivalence relation $\approx$ on $A^*$ as the reflexive symmetrical transitive closure of $\approx^1$, where, for $l = (l_1, \dots, l_k)^s$ and $r = (r_1, \dots, r_k)^s$ in $A^*$, $l \approx^1 r$ when there is $i \in \mathbb{N}_{k-1}^*$ such that $\mathcal{X}(l_i, l_{i+1}, r_i, r_{i+1})$ and $l_j = r_j$ for $j \in \mathbb{N}_k^* \setminus \{i, i+1\}$. We write $A \approx$ for the quotient set $A^*/\approx$ of $n$-sequence classes and

$$ \llbracket - \rrbracket: A^* \to A^\approx $$

for the associated projection. We remark that, if $u, v \in A^*$ are such that $u \approx v$, then $|u| = |v|$. Thus, the length given for the members of $A^*$ induces a length for the members of $A^\approx$. The
<figure><img src="image_25.png" /><figcaption>Figure 8: A configuration of 2-cells $l, l', r, r', u, v$ such that $X(l, l', r, r', u, v)$</figcaption></figure>

say that $k$ is the length of $v$ and we write $|v|$ for $k$. Moreover, we define a source $\partial_n^-(v)$ and a target $\partial_n^+(v)$ for $v$ by putting

$$ \partial_n^-(v) = \partial_n^-(v_1) \quad \text{and} \quad \partial_n^+(v) = \partial_n^+(v_k) $$

where, by convention, if $v = ()^s_u$ for some $u \in C_n$, then $\partial_n^-(v) = \partial_n^+(v) = u$. Thus, we obtain an $n$-cellular extension whose set of $(n+1)$-globes is $A^*$ and whose underlying $n$-category is $C$. We now define composition operations for the $n$-sequences. Given $i \in \mathbb{N}_{n-1}$, a cell $u \in C_{i+1}$ and an $n$-sequence $v = (v_1, \dots, v_l)^s \in A^*$ such that $u, v$ are $i$-composable, we put

$$ u \bullet_i v = (u \bullet_i v_1, \dots, u \bullet_i v_l)^s $$

where, by convention, if $v = ()^s_{\tilde{v}}$ for some $\tilde{v} \in C_n$, then $u \bullet_i v = ()^s_{u \bullet_i \tilde{v}}$. Given $n$-composable $n$-sequences $u = (u_1, \dots, u_k)^s$ and $v = (v_1, \dots, v_l)^s$ in $A^*$, we put

$$ u \bullet_n v = (u_1, \dots, u_k, v_1, \dots, v_l)^s. $$

In order to obtain a strict $(n+1)$-category from $C$ and $A^*$, we need to quotient $A^*$ so that the exchange condition (E) on precategories holds (c.f. Theorem B.1.1). For this purpose, we define a relation $\mathcal{X} \subseteq A^6$ such that, given $l, l', r, r', u, v \in A$, $\mathcal{X}(l, l', r, r', u, v)$ holds when $u, v$ are $(n-1)$-composable and the following equalities hold in $A$

$$ \begin{aligned} l &= u \bullet_{n-1} \partial_n^-(v) & r &= \partial_n^-(u) \bullet_{n-1} v \\ l' &= \partial_n^+(u) \bullet_{n-1} v & r' &= u \bullet_{n-1} \partial_n^+(v). \end{aligned} $$

In Figure 8, we illustrate this condition in the case of a 1-categorical action. Given top-level elements $l, l', r, r' \in A$, we write $\mathcal{X}(l, l', r, r')$ when there exist $u, v \in A$ such that we have $\mathcal{X}(l, l', r, r', u, v)$. We define an equivalence relation $\approx$ on $A^*$ as the reflexive symmetrical transitive closure of $\approx^1$, where, for $l = (l_1, \dots, l_k)^s$ and $r = (r_1, \dots, r_k)^s$ in $A^*$, $l \approx^1 r$ when there is $i \in \mathbb{N}_{k-1}^*$ such that $\mathcal{X}(l_i, l_{i+1}, r_i, r_{i+1})$ and $l_j = r_j$ for $j \in \mathbb{N}_k^* \setminus \{i, i+1\}$. We write $A \approx$ for the quotient set $A^*/ \approx$ of $n$-sequence classes and

$$ \llbracket - \rrbracket: A^* \to A^\approx $$

for the associated projection. We remark that, if $u, v \in A^*$ are such that $u \approx v$, then $|u| = |v|$. Thus, the length given for the members of $A^*$ induces a length for the members of $A^\approx$. The
operations $\partial_n^\epsilon$ for $\epsilon \in \{-, +\}$ on $A^*$ can be shown compatible with the relation $\approx$, so that they are well-defined on $A^\approx$ as well. Thus, we obtain an $n$-cellular extension $C[A]^\approx$ by extending the strict $n$-category $C$ with $A^\approx$. Similarly, the operations $\bullet_i$ for $i \in \mathbb{N}_{n-1}$ and $\bullet_n$ defined for $A^*$ are compatible with the relation $\approx$, so that they are well-defined on $C[A]^\approx_{n+1} = A^\approx$ as well. We add an identity operation by putting $\mathrm{id}_u^{n+1} = [(\cdot)_u^s]$ for $u \in C_n$. We then have:

**Proposition B.3.2.** $C[A]^\approx$ has a structure of a strict $(n+1)$-category. It is the free $(n+1)$-category on the action $(C, A)$ relatively to the forgetful functor $\mathcal{U}'$.

In the following, for all $n$-categorical action $(C, A)$, we write $C[A]^\approx$ for $C[A]^\approx$ as above. The construction $(C, A) \mapsto C[A]^\approx$ uniquely extends to a functor

$$-[-]^\approx: \mathrm{Cat}_n^A \to \mathrm{Cat}_{n+1}$$

which is left adjoint to $\mathcal{U}'$. Given $(H, h): (C, A) \to (D, B)$ in $\mathrm{Cat}_n^+$, the $(n+1)$-functor

$$H[h]^\approx: C[A]^\approx \to D[B]^\approx \in \mathrm{Cat}_{n+1}$$

is defined by $H[h]^\approx_i = H_i$ and $H[h]^\approx_{n+1}([[(u_1, \dots, u_k)^s]]) = [[(h(u_1), \dots, h(u_k))^s]]$ for $i \in \mathbb{N}_n$ and $(u_1, \dots, u_k)^s \in A^*.$

**Free categories on cellular extensions** Let $n \in \mathbb{N}$. We can sum up the content of the previous sections to give a concrete description of the functor

$$-[-]: \mathrm{Cat}_n^+ \to \mathrm{Cat}_{n+1}.$$

Indeed, since its right adjoint $\mathcal{V}_n: \mathrm{Cat}_{n+1} \to \mathrm{Cat}_n^+$ is the composite of the right adjoints $\mathcal{U}'$ and $\mathcal{U}$, we have, as a consequence of Propositions B.3.1 and B.3.2:

**Theorem B.3.3.** The composite

$$(-[-]^\approx) \circ (-[-]^A): \mathrm{Cat}_n^+ \to \mathrm{Cat}_{n+1}$$

is a left adjoint for $\mathcal{V}_n$. In particular, it is isomorphic to $-[–]$.

Our description of $-[–]$ also induces a decomposition property for the $(n+1)$-cells of free extensions:

**Proposition B.3.4.** Given an $n$-cellular extension $(C, X)$ and $u \in C[X]_{n+1}$, $u$ can be written

$$F_1[g_1] \bullet_n \cdots \bullet_n F_k[g_k]$$

where $k \in \mathbb{N}$, $g_i \in X$ and $F_i$ is an $n$-context class of type $g_i$ for $i \in \mathbb{N}_k^*$. Moreover, $k$ is unique for $u$.

**B.4 Cell decompositions** Here, we use the machinery of context classes in order to prove a decomposition property for the cells of a torsion-free complex. More precisely, given a torsion-free complex $P$, we prove that the $n$-cells of $\mathrm{Cell}(P)$ can be written as sequences of applied $(n-1)$-context classes. Actually, we prove the stronger statement that such a composite exists for any total ordering, called *linear extensions*, of the top-level $n$-generators that respects the relation $\prec$. This result will be a first step towards the proof that $\mathrm{Cell}(P)$ is freely generated on the atoms. The next one, tackled in the following section, will be to show that the above decomposition is unique up to the relation $\approx$ defined in the previous section.
operations $\partial_n^\epsilon$ for $\epsilon \in \{-, +\}$ on $A^*$ can be shown compatible with the relation $\approx$, so that they are well-defined on $A^\approx$ as well. Thus, we obtain an $n$-cellular extension $C[A]^\approx$ by extending the strict $n$-category $C$ with $A^\approx$. Similarly, the operations $\bullet_i$ for $i \in \mathbb{N}_{n-1}$ and $\bullet_n$ defined for $A^*$ are compatible with the relation $\approx$, so that they are well-defined on $C[A]^\approx_{n+1} = A^\approx$ as well. We add an identity operation by putting $\mathrm{id}_u^{n+1} = [(\cdot)_u^s]$ for $u \in C_n$. We then have:

**Proposition B.3.2.** $C[A]^\approx$ has a structure of a strict $(n+1)$-category. It is the free $(n+1)$-category on the action $(C, A)$ relatively to the forgetful functor $\mathcal{U}'$.

In the following, for all $n$-categorical action $(C, A)$, we write $C[A]^\approx$ for $C[A]^\approx$ as above. The construction $(C, A) \mapsto C[A]^\approx$ uniquely extends to a functor

$$-[\cdot]^\approx: \mathrm{Cat}_n^A \to \mathrm{Cat}_{n+1}$$

which is left adjoint to $\mathcal{U}'$. Given $(H, h): (C, A) \to (D, B)$ in $\mathrm{Cat}_n^+$, the $(n+1)$-functor

$$H[h]^\approx: C[A]^\approx \to D[B]^\approx \in \mathrm{Cat}_{n+1}$$

is defined by $H[h]^\approx_i = H_i$ and $H[h]^\approx_{n+1}([[(u_1, \dots, u_k)^s]]) = [[(h(u_1), \dots, h(u_k))^s]]$ for $i \in \mathbb{N}_n$ and $(u_1, \dots, u_k)^s \in A^*.$

**Free categories on cellular extensions** Let $n \in \mathbb{N}$. We can sum up the content of the previous sections to give a concrete description of the functor

$$-[\cdot]: \mathrm{Cat}_n^+ \to \mathrm{Cat}_{n+1}.$$

Indeed, since its right adjoint $\mathcal{V}_n: \mathrm{Cat}_{n+1} \to \mathrm{Cat}_n^+$ is the composite of the right adjoints $\mathcal{U}'$ and $\mathcal{U}$, we have, as a consequence of Propositions B.3.1 and B.3.2:

**Theorem B.3.3.** *The composite*

$$(-[\cdot]^\approx) \circ (-[\cdot]^A): \mathrm{Cat}_n^+ \to \mathrm{Cat}_{n+1}$$

is a left adjoint for $\mathcal{V}_n$. In particular, it is isomorphic to $-[\cdot]$.

Our description of $-[\cdot]$ also induces a decomposition property for the $(n+1)$-cells of free extensions:

**Proposition B.3.4.** *Given an $n$-cellular extension $(C, X)$ and $u \in C[X]_{n+1}$, $u$ can be written*

$$F_1[g_1] \bullet_n \cdots \bullet_n F_k[g_k]$$

where $k \in \mathbb{N}$, $g_i \in X$ and $F_i$ is an $n$-context class of type $g_i$ for $i \in \mathbb{N}_k^*$. Moreover, $k$ is unique for $u$.

**B.4 Cell decompositions** Here, we use the machinery of context classes in order to prove a decomposition property for the cells of a torsion-free complex. More precisely, given a torsion-free complex $P$, we prove that the $n$-cells of $\mathrm{Cell}(P)$ can be written as sequences of applied $(n-1)$-context classes. Actually, we prove the stronger statement that such a composite exists for any total ordering, called *linear extensions*, of the top-level $n$-generators that respects the relation $\prec$. This result will be a first step towards the proof that $\mathrm{Cell}(P)$ is freely generated on the atoms. The next one, tackled in the following section, will be to show that the above decomposition is unique up to the relation $\approx$ defined in the previous section.
**Linear extensions** Given a finite poset $(S, <)$, a linear extension of $(S, <)$ is the data of a bijection $\sigma: N^*_{|S|} \to S$ such that, for $i, j \in N^*_{|S|}$, if $\sigma(i) < \sigma(j)$, then $i < j$. Given two linear extensions $\sigma, \sigma'$: $N^*_{|S|} \to S$, a morphism of linear extensions of $(S, <)$ between $\sigma$ and $\sigma'$ is a function $\rho: N^*_{|S|} \to N^*_{|S|}$ such that the triangle

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

is commutative (in particular, $\rho$ is a bijection). We write $\text{LinExt}(S)$ for the category of linear extensions of $S$. Given $n \in \mathbb{N}$ and a bijection $\rho: N^*_n \to N^*_n$, we write $\text{Inv}(\rho) \in \mathbb{N}$ for the number of inversions of $\rho$, i.e.,

$$ \text{Inv}(\rho) = |\{(i, j) \in \mathbb{N}^*_n \times \mathbb{N}^*_n \mid i < j \text{ and } \rho(i) > \rho(j)\}|. $$

Moreover, given $i, j \in N^*_n$ such that $i \neq j$, we write $\tau_{i,j}$ for the bijection $N^*_n \to N^*_n$ which is the transposition of $i$ and $j$. We show that the morphisms of linear extensions are generated by the transpositions:

**Lemma B.4.1.** Given a poset $(S, <)$ and $\sigma, \sigma' \in \text{LinExt}(S)$ and $\rho: \sigma \to \sigma' \in \text{LinExt}(S)_1$, there exist $p \in \mathbb{N}$ and $\sigma_0, \dots, \sigma_p \in \text{LinExt}(S)$ with $\sigma = \sigma_0$ and $\sigma_p = \sigma'$, and $\rho_i: \sigma_{i-1} \to \sigma_i \in \text{LinExt}(S)$ for $i \in N^*_p$ such that $\rho = \rho_1 *_0 \dots *_0 \rho_p$ and $\rho_i$ is a transposition for $i \in N^*_p$.

*Proof.* We prove the result by induction on the number $\text{Inv}(\rho)$ of inversions of the bijection $\rho$. If $\text{Inv}(\rho) = 0$, then $\rho = 1_{N^*_{|S|}} = \text{id}^1_\sigma$. So suppose that $\text{Inv}(\rho) > 0$. Thus, there exists $k \in N^*_{|S|-1}$ such that $\rho(k) > \rho(k+1)$. The bijection $\bar{\sigma} = \sigma \circ \tau_{k,k+1}$ is then a linear extension of $(S, <)$ as in

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

Indeed, for $i, j \in N^*_{|S|}$ such that $i \neq j$ and $\bar{\sigma}(i) < \bar{\sigma}(j)$,

- if $i = k+1$ and $j = k$, then $\sigma(k) < \sigma(k+1)$, so $\sigma'(\rho(k)) < \sigma'(\rho(k+1))$ and $\rho(k) < \rho(k+1)$, contradicting the hypothesis;

- if $i = k+1$ and $j \neq k$, then $\sigma(i-1) < \sigma(j)$, so $i-1 < j$, and, since $j \neq i$, $i < j$;

- otherwise, we are able to prove that $i < j$ easily.

Moreover, the number of inversions of $\rho \circ \tau_{k,k+1}$ is $\text{Inv}(\rho) - 1$. By induction hypothesis, $\rho \circ \tau_{k,k+1}$ can be written as

$$ \rho \circ \tau_{k,k+1} = \rho_2 *_0 \dots *_0 \rho_p $$

for some $p \in \mathbb{N}$ and transpositions $\rho_i: \sigma_{i-1} \to \sigma_i \in \text{LinExt}(S)_1$ for $i \in N^*_{p-1}$, so that

$$ \rho = \tau_{k,k+1} *_0 \rho_2 *_0 \dots *_0 \rho_p $$

is of the wanted form.

□
**Linear extensions** Given a finite poset $(S, <)$, a linear extension of $(S, <)$ is the data of a bijection $\sigma: N^*_{|S|} \to S$ such that, for $i, j \in N^*_{|S|}$, if $\sigma(i) < \sigma(j)$, then $i < j$. Given two linear extensions $\sigma, \sigma'$: $N^*_{|S|} \to S$, a morphism of linear extensions of $(S, <)$ between $\sigma$ and $\sigma'$ is a function $\rho: N^*_{|S|} \to N^*_{|S|}$ such that the triangle

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

is commutative (in particular, $\rho$ is a bijection). We write $\mathrm{LinExt}(S)$ for the category of linear extensions of $S$. Given $n \in \mathbb{N}$ and a bijection $\rho: N^*_n \to N^*_n$, we write $\mathrm{Inv}(\rho) \in \mathbb{N}$ for the number of inversions of $\rho$, i.e.,

$$ \mathrm{Inv}(\rho) = |\{(i, j) \in N^*_n \times N^*_n | i < j \text{ and } \rho(i) > \rho(j)\}|. $$

Moreover, given $i, j \in N^*_n$ such that $i \neq j$, we write $\tau_{i,j}$ for the bijection $N^*_n \to N^*_n$ which is the transposition of $i$ and $j$. We show that the morphisms of linear extensions are generated by the transpositions:

**Lemma B.4.1.** Given a poset $(S, <)$ and $\sigma, \sigma' \in \mathrm{LinExt}(S)$ and $\rho: \sigma \to \sigma' \in \mathrm{LinExt}(S)_1$, there exist $p \in \mathbb{N}$ and $\sigma_0, \dots, \sigma_p \in \mathrm{LinExt}(S)$ with $\sigma = \sigma_0$ and $\sigma_p = \sigma'$, and $\rho_i: \sigma_{i-1} \to \sigma_i \in \mathrm{LinExt}(S)$ for $i \in N^*_p$ such that $\rho = \rho_1 *_0 \dots *_0 \rho_p$ and $\rho_i$ is a transposition for $i \in N^*_p$.

*Proof.* We prove the result by induction on the number $\mathrm{Inv}(\rho)$ of inversions of the bijection $\rho$. If $\mathrm{Inv}(\rho) = 0$, then $\rho = 1_{N^*_{|S|}} = \mathrm{id}^1_\sigma$. So suppose that $\mathrm{Inv}(\rho) > 0$. Thus, there exists $k \in N^*_{|S|-1}$ such that $\rho(k) > \rho(k+1)$. The bijection $\bar{\sigma} = \sigma \circ \tau_{k,k+1}$ is then a linear extension of $(S, <)$ as in

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

Indeed, for $i, j \in N^*_{|S|}$ such that $i \neq j$ and $\bar{\sigma}(i) < \bar{\sigma}(j)$,

- if $i = k+1$ and $j = k$, then $\sigma(k) < \sigma(k+1)$, so $\sigma'(\rho(k)) < \sigma'(\rho(k+1))$ and $\rho(k) < \rho(k+1)$, contradicting the hypothesis;

- if $i = k+1$ and $j \neq k$, then $\sigma(i-1) < \sigma(j)$, so $i-1 < j$, and, since $j \neq i$, $i < j$;

- otherwise, we are able to prove that $i < j$ easily.

Moreover, the number of inversions of $\rho \circ \tau_{k,k+1}$ is $\mathrm{Inv}(\rho) - 1$. By induction hypothesis, $\rho \circ \tau_{k,k+1}$ can be written as

$$ \rho \circ \tau_{k,k+1} = \rho_2 *_0 \dots *_0 \rho_p $$

for some $p \in \mathbb{N}$ and transpositions $\rho_i: \sigma_{i-1} \to \sigma_i \in \mathrm{LinExt}(S)_1$ for $i \in N^*_{p-1}$, so that

$$ \rho = \tau_{k,k+1} *_0 \rho_2 *_0 \dots *_0 \rho_p $$

is of the wanted form.

□
**Decomposition theorem** Here, we write $P$ for a torsion-free complex. We show that cells of $\mathrm{Cell}(P)$ can be decomposed as composites of applied context classes that respect the relation $\triangleleft$. First, we state a simple criterion for equality in $\mathrm{Cell}(P)$, which readily follows from the definitions of cells and source/target operations:

**Lemma B.4.2.** Given $k, n \in \mathbb{N}$ with $k < n$, $\epsilon \in \{-, +\}$ and $X, Y \in \mathrm{Cell}(P)_n$ such that $\partial_k^\epsilon(X) = \partial_k^\epsilon(Y)$ and $X_{i,\epsilon} = Y_{i,\epsilon}$ for $i \in \{k+1, \dots, n\}$, we have $X = Y$.

Next, we show that we can write a cell as a composition by extracting a minimal element for $\triangleleft$:

**Lemma B.4.3.** Let $n \in \mathbb{N}^*$ and $X$ be an $n$-cell and $g$ be a minimal element of $X_n$ for $\triangleleft X_n$. Then, there exist $n$-cells $Y$ and $Z$ that are $(n-1)$-composable such that $Y_n = \{g\}$, $Z_n = X_n \setminus \{g\}$ and $X = Y *_{n-1} Z$.

*Proof.* Since $g$ is minimal for $\triangleleft X_n$, we have $\{g\}^\mp \subseteq X_{n-1, -}$. Moreover, since $X$ is an $n$-cell, $X_n$ is fork-free so that $\{g\} \perp (X_n \setminus \{g\})$. Thus, by Lemma A.1.4, writing $V$ for $(X_{n-1, -} \cup g^+) \setminus g^-$, we have that $\{g\}$ moves $X_{n-1, -}$ to $V$ and $X_n \setminus \{g\}$ moves $V$ to $X_{n-1, +}$. By Theorem 2.1.1, the cell $Y = \mathrm{Glue}(\partial_{n-1}^-(X), \{g\})$ is an $n$-cell which satisfies that

$$Y_n = \{g\}, \quad \partial_{n-1}^-(Y) = \partial_{n-1}^-(X) \quad \text{and} \quad Y_{n-1, +} = V.$$

By Theorem 2.1.1 again, $Z = \mathrm{Glue}(\partial_{n-1}^+(Y), X_n \setminus \{g\})$ is an $n$-cell such that

$$Z_n = X_n \setminus \{g\}, \quad \partial_{n-1}^-(Z) = \partial_{n-1}^+(Y) \quad \text{and} \quad Z_{n-1, +} = X_{n-1, +},$$

so that $\partial_{n-1}^+(Z) = \partial_{n-1}^+(X)$. Then, by the definition of $*_{n-1}$, we have $X = Y *_{n-1} Z$. $\square$

The previous lemma implies that we can write a cell as a composite of cells with a single top-level generator, that are moreover ordered by a given linear extension:

**Lemma B.4.4.** Let $n \in \mathbb{N}^*$ and $X$ be an $n$-cell of $P$, $p = |X_n|$ and $\sigma: \mathbb{N}_p^* \to (X_n, \triangleleft X_n)$ be a linear extension. There exist $n$-cells $X^1, \dots, X^p$ that are $(n-1)$-composable and such that

$$X_n^i = \{\sigma(i)\} \quad \text{for } i \in \mathbb{N}_p^* \quad \text{and} \quad X = X^1 *_{n-1} \cdots *_{n-1} X^p.$$

*Proof.* We prove this property by induction on $p$. When $p = 0$ or $p = 1$, then the property is trivial. So suppose that $p > 1$. Note that $\sigma(1)$ is minimal in $X_n$ for $\triangleleft X_n$. By Lemma B.4.3, we can write $X = X^1 *_{n-1} X'$ where $X^1$ and $X'$ are $(n-1)$-composable $n$-cells such that $X_n^1 = \{\sigma(1)\}$ and $X_n' = X_n \setminus \{\sigma(1)\}$. By induction hypothesis, we have that $X' = X^2 *_{n-1} \cdots *_{n-1} X^p$ for some $(n-1)$-composable $n$-cells $X^2, \dots, X^p$ such that $X_n^i = \{\sigma(i)\}$ for $i \in \{2, \dots, p\}$, which concludes the proof. $\square$

Next, we give a sufficient criterion for a cell to be written as an applied context class:

**Lemma B.4.5.** Let $k, n \in \mathbb{N}$ with $k < n$, $g \in P_n$ and $X$ be an $n$-cell such that $X_{i, \epsilon} = \langle g \rangle_{i, \epsilon}$ for $i \in \{k+1, \dots, n\}$ and $\epsilon \in \{-, +\}$. There exists a $k$-context class $F$ of type $\langle g \rangle$ such that we have $X = F[\langle g \rangle]$.

*Proof.* We show this property by induction on $k$. When $k = 0$, we have that $X_{i, \epsilon} = \langle g \rangle_{i, \epsilon}$ for $i \in \mathbb{N}_n^*$ and $\epsilon \in \{-, +\}$. Moreover, since $X$ is an $n$-cell, we have that $\langle g \rangle_{1, -}$ moves $X_{0, -}$ to $X_{0, +}$, so that $\langle g \rangle_{1, -}^\mp = \langle g \rangle_{0, -} \subseteq X_{0, -}$. Since $X_{0, -}$ is fork-free, $|X_{0, -}| = 1$. Thus, $X_{0, -} = \langle g \rangle_{0, -}$.
**Decomposition theorem** Here, we write $P$ for a torsion-free complex. We show that cells of $\mathrm{Cell}(P)$ can be decomposed as composites of applied context classes that respect the relation $\triangleleft$. First, we state a simple criterion for equality in $\mathrm{Cell}(P)$, which readily follows from the definitions of cells and source/target operations:

**Lemma B.4.2.** Given $k, n \in \mathbb{N}$ with $k < n$, $\epsilon \in \{-, +\}$ and $X, Y \in \mathrm{Cell}(P)_n$ such that $\partial_k^\epsilon(X) = \partial_k^\epsilon(Y)$ and $X_{i,\epsilon} = Y_{i,\epsilon}$ for $i \in \{k+1, \dots, n\}$, we have $X = Y$.

Next, we show that we can write a cell as a composition by extracting a minimal element for $\triangleleft$:

**Lemma B.4.3.** Let $n \in \mathbb{N}^*$ and $X$ be an $n$-cell and $g$ be a minimal element of $X_n$ for $\triangleleft X_n$. Then, there exist $n$-cells $Y$ and $Z$ that are $(n-1)$-composable such that $Y_n = \{g\}$, $Z_n = X_n \setminus \{g\}$ and $X = Y *_{n-1} Z$.

*Proof.* Since $g$ is minimal for $\triangleleft X_n$, we have $\{g\}^\mp \subseteq X_{n-1,-}$. Moreover, since $X$ is an $n$-cell, $X_n$ is fork-free so that $\{g\} \perp (X_n \setminus \{g\})$. Thus, by Lemma A.1.4, writing $V$ for $(X_{n-1,-} \cup g^+) \setminus g^-$, we have that $\{g\}$ moves $X_{n-1,-}$ to $V$ and $X_n \setminus \{g\}$ moves $V$ to $X_{n-1,+}$. By Theorem 2.1.1, the cell $Y = \mathrm{Glue}(\partial_{n-1}^-(X), \{g\})$ is an $n$-cell which satisfies that

$$Y_n = \{g\}, \quad \partial_{n-1}^-(Y) = \partial_{n-1}^-(X) \quad \text{and} \quad Y_{n-1,+} = V.$$

By Theorem 2.1.1 again, $Z = \mathrm{Glue}(\partial_{n-1}^+(Y), X_n \setminus \{g\})$ is an $n$-cell such that

$$Z_n = X_n \setminus \{g\}, \quad \partial_{n-1}^-(Z) = \partial_{n-1}^+(Y) \quad \text{and} \quad Z_{n-1,+} = X_{n-1,+},$$

so that $\partial_{n-1}^+(Z) = \partial_{n-1}^+(X)$. Then, by the definition of $*_{n-1}$, we have $X = Y *_{n-1} Z$. $\square$

The previous lemma implies that we can write a cell as a composite of cells with a single top-level generator, that are moreover ordered by a given linear extension:

**Lemma B.4.4.** Let $n \in \mathbb{N}^*$ and $X$ be an $n$-cell of $P$, $p = |X_n|$ and $\sigma: \mathbb{N}_p^* \to (X_n, \triangleleft X_n)$ be a linear extension. There exist $n$-cells $X^1, \dots, X^p$ that are $(n-1)$-composable and such that

$$X_n^i = \{\sigma(i)\} \quad \text{for } i \in \mathbb{N}_p^* \quad \text{and} \quad X = X^1 *_{n-1} \cdots *_{n-1} X^p.$$

*Proof.* We prove this property by induction on $p$. When $p=0$ or $p=1$, then the property is trivial. So suppose that $p>1$. Note that $\sigma(1)$ is minimal in $X_n$ for $\triangleleft X_n$. By Lemma B.4.3, we can write $X = X^1 *_{n-1} X'$ where $X^1$ and $X'$ are $(n-1)$-composable $n$-cells such that $X_n^1 = \{\sigma(1)\}$ and $X_n' = X_n \setminus \{\sigma(1)\}$. By induction hypothesis, we have that $X' = X^2 *_{n-1} \cdots *_{n-1} X^p$ for some $(n-1)$-composable $n$-cells $X^2, \dots, X^p$ such that $X_n^i = \{\sigma(i)\}$ for $i \in \{2, \dots, p\}$, which concludes the proof. $\square$

Next, we give a sufficient criterion for a cell to be written as an applied context class:

**Lemma B.4.5.** Let $k, n \in \mathbb{N}$ with $k < n$, $g \in P_n$ and $X$ be an $n$-cell such that $X_{i,\epsilon} = \langle g \rangle_{i,\epsilon}$ for $i \in \{k+1, \dots, n\}$ and $\epsilon \in \{-, +\}$. There exists a $k$-context class $F$ of type $\langle g \rangle$ such that we have $X = F[\langle g \rangle]$.

*Proof.* We show this property by induction on $k$. When $k=0$, we have that $X_{i,\epsilon} = \langle g \rangle_{i,\epsilon}$ for $i \in \mathbb{N}_n^*$ and $\epsilon \in \{-, +\}$. Moreover, since $X$ is an $n$-cell, we have that $\langle g \rangle_{1,-}$ moves $X_{0,-}$ to $X_{0,+}$, so that $\langle g \rangle_{1,-}^\mp = \langle g \rangle_{0,-} \subseteq X_{0,-}$. Since $X_{0,-}$ is fork-free, $|X_{0,-}| = 1$. Thus, $X_{0,-} = \langle g \rangle_{0,-}$.
Similarly, $X_{0,+} = \langle g \rangle_{0,+}$. Hence, we have $X = \langle g \rangle$ and the property of the statement is verified with the unique 0-context class.

So suppose that $k > 0$. We have that $X_{k+1,\epsilon} = \langle g \rangle_{k+1,\epsilon}$ moves $X_{k,-}$ to $X_{k,+}$, so $\langle g \rangle_{k,-} \subseteq X_{k,-}$. By Axiom (T3), $\langle g \rangle_{k,-}$ is a segment for $\langle X_{k,-} \rangle$ and, by Lemma A.1.8, there exist $U, V \subseteq X_{k,-}$ and $A, B \subseteq P_{k-1}$ such that

- $U, \langle g \rangle_{k,-}$, $V$ is a partition of $X_{k,-}$,

- $U$ moves $X_{k-1,-}$ to $A$, $\langle g \rangle_{k,-}$ moves $A$ to $B$ and $V$ moves $B$ to $X_{k-1,+}$.

Writing

$$L = \text{Glue}(\partial_{k-1}^{-}(X), U) \quad X^k = \text{Glue}(\partial_{k-1}^{+}(L), \langle g \rangle_{k,-}) \quad R = \text{Glue}(\partial_{k-1}^{+}(X^k), V),$$

by Theorem 2.1.1, we have that $L, X^k, R$ are $k$-cells that are $(k-1)$-composable and such that

$$\partial_k^{-}(X) = L \bullet_{k-1} X^k \bullet_{k-1} R$$

By induction on $i \in \{k+1, n\}$, we define $i$-cells $X^i$ such that $\partial_{i-1}^{-}(X^i) = X^{i-1}$ and $X_i^i = \langle g \rangle_{i,-}$ by putting $X^i = \text{Glue}(X^{i-1}, \langle g \rangle_{i,-})$, which is indeed a cell by Theorem 2.1.1. Then, $X^n$ is an $n$-cell such that $\partial_k^{-}(X^n) = X^k$ and $X_{i,\epsilon}^n = \langle g \rangle_{i,\epsilon}$ for $i \in \{k, \dots, n\}$. Moreover, since $\partial_k^{-}(X^n) = X^k$,

$$L, X^n, R \text{ are } (k-1)\text{-composable and } \partial_k^{-}(L \bullet_{k-1} X^n \bullet_{k-1} R) = \partial_k^{-}(X).$$

Furthermore, we have that

$$X_{i,-} = \langle g \rangle_{i,-} = X_{i,-}^n = (L \bullet_{k-1} X^n \bullet_{k-1} R)_{i,-}$$

for $i \in \{k+1, n\}$ so that, by Lemma B.4.2, we have $X = L \bullet_{k-1} X^n \bullet_{k-1} R$. By induction hypothesis, there exists a $(k-1)$-context class $F'$ such that $X^n = F'[\langle g \rangle]$. Writing $F$ for the $k$-context class $\llbracket (L, F', R) \rrbracket$, we have that $X = F[\langle g \rangle]$ as wanted. $\square$

We can now prove the following decomposition theorem:

**Theorem B.4.6.** Given $n \in \mathbb{N}^*$, an $n$-cell $X \in \text{Cell}(P)$ and a linear extension

$$\sigma: \mathbb{N}_p^* \to (X_n, \langle X_n \rangle)$$

with $p = |X_n|$, there exist $(n-1)$-context classes $F_1, \dots, F_p$ of $\text{Cell}(P)$ of types $\langle \sigma(1) \rangle, \dots, \langle \sigma(p) \rangle$ respectively such that

$$X = F_1[\langle \sigma(1) \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_p[\langle \sigma(p) \rangle].$$

**Remark B.4.7.** By Axiom (T1), given $n \in \mathbb{N}^*$ and a finite subset $S \subseteq P_n$, there always exists a linear extension $\sigma: \mathbb{N}_{|P|}^* \to (S, \langle S \rangle)$, so that an $n$-cell $X$ of $P$ has at least one decomposition of the form given by Theorem B.4.6.

*Proof.* By Lemma B.4.4, $X$ can be written $X = X^1 \bullet_{n-1} \cdots \bullet_{n-1} X^p$ for some $n$-cells $X^1, \dots, X^p$ such that $X_n^i = \{\sigma(i)\}$ for $i \in \mathbb{N}_p^*$. We conclude with Lemma B.4.5. $\square$

We verify with the following property that Theorem B.4.6 does not miss other possible decompositions:

**Proposition B.4.8.** Given $n \in \mathbb{N}^*$ and $X \in \text{Cell}(P)_n$ such that

$$X = F_1[\langle x_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_k[\langle x_k \rangle]$$

for some $k \in \mathbb{N}$, $x_1, \dots, x_k \in P_n$ and $(n-1)$-context classes $F_1, \dots, F_k$ of $\text{Cell}(P)$, we have
Similarly, $X_{0,+} = \langle g \rangle_{0,+}$. Hence, we have $X = \langle g \rangle$ and the property of the statement is verified with the unique 0-context class.

So suppose that $k > 0$. We have that $X_{k+1,\epsilon} = \langle g \rangle_{k+1,\epsilon}$ moves $X_{k,-}$ to $X_{k,+}$, so $\langle g \rangle_{k,-} \subseteq X_{k,-}$. By Axiom (T3), $\langle g \rangle_{k,-}$ is a segment for $\langle X_{k,-} \rangle$ and, by Lemma A.1.8, there exist $U, V \subseteq X_{k,-}$ and $A, B \subseteq P_{k-1}$ such that

- $U, \langle g \rangle_{k,-}, V$ is a partition of $X_{k,-}$,

- $U$ moves $X_{k-1,-}$ to $A$, $\langle g \rangle_{k,-}$ moves $A$ to $B$ and $V$ moves $B$ to $X_{k-1,+}$.

Writing

$$L = \text{Glue}(\partial_{k-1}^{-}(X), U) \quad X^k = \text{Glue}(\partial_{k-1}^{+}(L), \langle g \rangle_{k,-}) \quad R = \text{Glue}(\partial_{k-1}^{+}(X^k), V),$$

by Theorem 2.1.1, we have that $L, X^k, R$ are $k$-cells that are $(k-1)$-composable and such that

$$\partial_k^{-}(X) = L \bullet_{k-1} X^k \bullet_{k-1} R$$

By induction on $i \in \{k+1, n\}$, we define $i$-cells $X^i$ such that $\partial_{i-1}^{-}(X^i) = X^{i-1}$ and $X_i^i = \langle g \rangle_{i,-}$ by putting $X^i = \text{Glue}(X^{i-1}, \langle g \rangle_{i,-})$, which is indeed a cell by Theorem 2.1.1. Then, $X^n$ is an $n$-cell such that $\partial_k^{-}(X^n) = X^k$ and $X_{i,\epsilon}^n = \langle g \rangle_{i,\epsilon}$ for $i \in \{k, \dots, n\}$. Moreover, since $\partial_k^{-}(X^n) = X^k$,

$$L, X^n, R \text{ are } (k-1)\text{-composable and } \partial_k^{-}(L \bullet_{k-1} X^n \bullet_{k-1} R) = \partial_k^{-}(X).$$

Furthermore, we have that

$$X_{i,-} = \langle g \rangle_{i,-} = X_{i,-}^n = (L \bullet_{k-1} X^n \bullet_{k-1} R)_{i,-}$$

for $i \in \{k+1, n\}$ so that, by Lemma B.4.2, we have $X = L \bullet_{k-1} X^n \bullet_{k-1} R$. By induction hypothesis, there exists a $(k-1)$-context class $F'$ such that $X^n = F'[\langle g \rangle]$. Writing $F$ for the $k$-context class $\llbracket (L, F', R) \rrbracket$, we have that $X = F[\langle g \rangle]$ as wanted. $\square$

We can now prove the following decomposition theorem:

**Theorem B.4.6.** Given $n \in \mathbb{N}^*$, an $n$-cell $X \in \text{Cell}(P)$ and a linear extension

$$\sigma: \mathbb{N}_p^* \to (X_n, \langle X_n \rangle)$$

with $p = |X_n|$, there exist $(n-1)$-context classes $F_1, \dots, F_p$ of $\text{Cell}(P)$ of types $\langle \sigma(1) \rangle, \dots, \langle \sigma(p) \rangle$ respectively such that

$$X = F_1[\langle \sigma(1) \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_p[\langle \sigma(p) \rangle].$$

**Remark B.4.7.** By Axiom (T1), given $n \in \mathbb{N}^*$ and a finite subset $S \subseteq P_n$, there always exists a linear extension $\sigma: \mathbb{N}_{\mid P_n}^* \to (S, \langle S \rangle)$, so that an $n$-cell $X$ of $P$ has at least one decomposition of the form given by Theorem B.4.6.

*Proof.* By Lemma B.4.4, $X$ can be written $X = X^1 \bullet_{n-1} \cdots \bullet_{n-1} X^p$ for some $n$-cells $X^1, \dots, X^p$ such that $X_n^i = \{\sigma(i)\}$ for $i \in \mathbb{N}_p^*$. We conclude with Lemma B.4.5. $\square$

We verify with the following property that Theorem B.4.6 does not miss other possible decompositions:

**Proposition B.4.8.** Given $n \in \mathbb{N}^*$ and $X \in \text{Cell}(P)_n$ such that

$$X = F_1[\langle x_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_k[\langle x_k \rangle]$$

for some $k \in \mathbb{N}$, $x_1, \dots, x_k \in P_n$ and $(n-1)$-context classes $F_1, \dots, F_k$ of $\text{Cell}(P)$, we have
(i) $X_n = \{x_1, \dots, x_k\}$,

(ii) for $i, j \in \mathbb{N}_k^*$ with $i \neq j$, we have $x_i \neq x_j$,

(iii) the function $p \mapsto x_p$ of type $\mathbb{N}_k^* \to X_n$ is a linear extension of $(X_n, \triangleleft_{X_n})$.

In particular, if $X = F'_1[\langle y_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F'_l[\langle y_l \rangle]$ for some $l \in \mathbb{N}$, $y_1, \dots, y_l \in P_n$ and $(n-1)$-context classes $F'_1, \dots, F'_l$, then $k = l$ and $\{x_1, \dots, x_k\} = \{y_1, \dots, y_l\}$.

**Proof.** Given $m < n$, $x \in P_n$ and an $m$-context class $F$ of type $\langle x \rangle$, by a simple induction on $m$, one can prove that $(F[\langle x \rangle])_n = \{x\}$. Thus, by definition of $*_n$, we have $X_n = \{x_1, \dots, x_k\}$, so (i) holds. Let $i, j \in \mathbb{N}_k^*$ with $i < j$, and $Y, Z$ be the $n$-cells defined by

$$Y = F_1[\langle x_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_i[\langle x_i \rangle] \quad \text{and} \quad Z = F_{i+1}[\langle x_{i+1} \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_k[\langle x_k \rangle].$$

Then $x_i \in Y_n$, $x_j \in Z_n$ and $Y, Z$ are $(n-1)$-composable. By Lemma 2.2.1, $Y_n \cap Z_n = \emptyset$. Hence, $x_i \neq x_j$, thus (ii) holds. Moreover, by Lemma 2.2.1 again, $(Y_n)^- \cap (Z_n)^+ = \emptyset$, so that $\neg(x_j \triangleleft_{X_n} x_i)$. Thus, by contrapositive, given $i, j \in \mathbb{N}_k^*$ such that $x_i \triangleleft_{X_n} x_j$, we have $i \le j$, and in fact $i < j$ by Axiom (T1). Since $\triangleleft_{X_n}$ is the transitive closure of $\triangleleft_{X_n}$, given $i, j \in \mathbb{N}_k^*$, we have that $x_i \triangleleft_{X_n} x_j$ implies $i < j$, so the function $p \mapsto x_p$ is a linear extension of $(X_n, \triangleleft_{X_n})$, which concludes the proof of (iii). $\square$

**B.5 Freeness for torsion-free complexes** In this section, we give a proof to Theorem 2.4.1, which states that the $\omega$-category of cells of a torsion-free complex is, in each dimension, a free extension over itself. By the characterization of the functor $-[–]: \mathbf{Cat}_n^+ \to \mathbf{Cat}_{n+1}$ given in Appendix B.3, we are only left to prove that the canonical forms $F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$ from the previous section are unique, up to the relation $\approx$ defined in Appendix B.2. We first prove the unicity of the decomposition in the case $p = 1$, and then handle the general case afterwards.

In this section, we write $P$ for a torsion-free complex.

**Freeness of decompositions of length one** We first prove two technical lemmas on the manipulation of contexts by mutual induction. The first states that, as long as we respect the relation $\triangleleft$, we can modify the whiskers of the contexts:

**Lemma B.5.1.** Let $k, n \in \mathbb{N}^*$ with $k < n$, $\epsilon \in \{-, +\}$, $g \in P_n$ and $E = (L, F, R)$ be a $k$-context of type $\langle g \rangle$ of Cell($P$). Consider the following subsets of $P_k$:

$$S = L_k \cup R_k, \\ U = \{y \in S \mid y \triangleleft_{S'} \langle g \rangle_{k, \epsilon}\},$$

$$S' = S \cup \langle g \rangle_{k, \epsilon}, \\ V = \{y \in S \mid \langle g \rangle_{k, \epsilon} \triangleleft_{S'} y\}.$$

Then, for every partition $U' \cup V'$ of $S$ such that $U \subseteq U'$, $V \subseteq V'$, $U'$ is initial in $S$ and $V'$ is final in $S$, there exists a $k$-context $E' = (L', F', R')$ of type $X$ such that

$$L'_k = U',$$

$$R'_k = V',$$

$$E \approx_k E.$$

For $k = 2$, Lemma B.5.1 states that, given $g \in P_n$ for some $n > 2$ and a 2-context $E = (L, F, R)$ of type $\langle g \rangle$ Figure 9, $E$ is equivalent through $\approx_2$ to a 2-context $E' = (L', F', R')$ as on the right of Figure 9. The second lemma gives sufficient conditions under which two composable context classes can be decomposed in a way that allows them to be exchanged by the relations $\approx_k$ or $\approx$ defined in Appendix B.2:
(i) $X_n = \{x_1, \dots, x_k\}$,

(ii) for $i, j \in \mathbb{N}_k^*$ with $i \neq j$, we have $x_i \neq x_j$,

(iii) the function $p \mapsto x_p$ of type $\mathbb{N}_k^* \to X_n$ is a linear extension of $(X_n, \triangleleft_{X_n})$.

In particular, if $X = F'_1[\langle y_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F'_l[\langle y_l \rangle]$ for some $l \in \mathbb{N}$, $y_1, \dots, y_l \in P_n$ and $(n-1)$-context classes $F'_1, \dots, F'_l$, then $k = l$ and $\{x_1, \dots, x_k\} = \{y_1, \dots, y_l\}$.

**Proof.** Given $m < n$, $x \in P_n$ and an $m$-context class $F$ of type $\langle x \rangle$, by a simple induction on $m$, one can prove that $(F[\langle x \rangle])_n = \{x\}$. Thus, by definition of $*_n$, we have $X_n = \{x_1, \dots, x_k\}$, so (i) holds. Let $i, j \in \mathbb{N}_k^*$ with $i < j$, and $Y, Z$ be the $n$-cells defined by

$$Y = F_1[\langle x_1 \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_i[\langle x_i \rangle] \quad \text{and} \quad Z = F_{i+1}[\langle x_{i+1} \rangle] \bullet_{n-1} \cdots \bullet_{n-1} F_k[\langle x_k \rangle].$$

Then $x_i \in Y_n$, $x_j \in Z_n$ and $Y, Z$ are $(n-1)$-composable. By Lemma 2.2.1, $Y_n \cap Z_n = \emptyset$. Hence, $x_i \neq x_j$, thus (ii) holds. Moreover, by Lemma 2.2.1 again, $(Y_n)^- \cap (Z_n)^+ = \emptyset$, so that $\neg(x_j \triangleleft_{X_n} x_i)$. Thus, by contrapositive, given $i, j \in \mathbb{N}_k^*$ such that $x_i \triangleleft_{X_n} x_j$, we have $i \leq j$, and in fact $i < j$ by Axiom (T1). Since $\triangleleft_{X_n}$ is the transitive closure of $\triangleleft_{X_n}$, given $i, j \in \mathbb{N}_k^*$, we have that $x_i \triangleleft_{X_n} x_j$ implies $i < j$, so the function $p \mapsto x_p$ is a linear extension of $(X_n, \triangleleft_{X_n})$, which concludes the proof of (iii). $\square$

**B.5 Freeness for torsion-free complexes** In this section, we give a proof to Theorem 2.4.1, which states that the $\omega$-category of cells of a torsion-free complex is, in each dimension, a free extension over itself. By the characterization of the functor $-[–]: \mathbf{Cat}_n^+ \to \mathbf{Cat}_{n+1}$ given in Appendix B.3, we are only left to prove that the canonical forms $F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$ from the previous section are unique, up to the relation $\approx$ defined in Appendix B.2. We first prove the unicity of the decomposition in the case $p = 1$, and then handle the general case afterwards. In this section, we write $P$ for a torsion-free complex.

**Freeness of decompositions of length one** We first prove two technical lemmas on the manipulation of contexts by mutual induction. The first states that, as long as we respect the relation $\triangleleft$, we can modify the whiskers of the contexts:

**Lemma B.5.1.** Let $k, n \in \mathbb{N}^*$ with $k < n$, $\epsilon \in \{-, +\}$, $g \in P_n$ and $E = (L, F, R)$ be a $k$-context of type $\langle g \rangle$ of Cell($P$). Consider the following subsets of $P_k$:

$$S = L_k \cup R_k,$$ 
$U = \{y \in S \mid y \triangleleft_{S'} \langle g \rangle_{k, \epsilon}\},$$

$$S' = S \cup \langle g \rangle_{k, \epsilon},$$ 
$V = \{y \in S \mid \langle g \rangle_{k, \epsilon} \triangleleft_{S'} y\}.$$

Then, for every partition $U' \cup V'$ of $S$ such that $U \subseteq U'$, $V \subseteq V'$, $U'$ is initial in $S$ and $V'$ is final in $S$, there exists a $k$-context $E' = (L', F', R')$ of type $X$ such that

$$L'_k = U',$$

$$R'_k = V',$$

$$E \approx_k E'.$$

For $k = 2$, Lemma B.5.1 states that, given $g \in P_n$ for some $n > 2$ and a 2-context $E = (L, F, R)$ of type $\langle g \rangle$ Figure 9, $E$ is equivalent through $\approx_2$ to a 2-context $E' = (L', F', R')$ as on the right of Figure 9. The second lemma gives sufficient conditions under which two composable context classes can be decomposed in a way that allows them to be exchanged by the relations $\approx_k$ or $\approx$ defined in Appendix B.2:
<figure><img src="image_24.png" /><figcaption>Figure 9: Illustration of Lemma B.5.1</figcaption></figure>

**Lemma B.5.2.** Let $k, n_1, n_2 \in \mathbb{N}^*$ with $k < \min(n_1, n_2)$, $g_1 \in P_{n_1}$, $g_2 \in P_{n_2}$, and $F_1, F_2$ be $k$-context classes of Cell($P$), of type $\langle g_1 \rangle$ and $\langle g_2 \rangle$ respectively, such that

$$F_1[\partial_k^+(\langle g_1 \rangle)] = F_2[\partial_k^-(\langle g_2 \rangle)] \quad \text{and} \quad \langle g_1 \rangle_{k,+} \cap \langle g_2 \rangle_{k,-} = \emptyset.$$

There exist $k$-context classes $\bar{F}_1, \bar{F}_2$ of type $\langle g_1 \rangle$ and $\langle g_2 \rangle$ respectively, such that

- either $\bar{F}_1, \bar{F}_2$ are $(k-1)$-composable and

$$F_1 = \bar{F}_1 \bullet_{k-1} \bar{F}_2[\partial_k^-(\langle g_2 \rangle)] \qquad F_2 = \bar{F}_1[\partial_k^+(\langle g_1 \rangle)] \bullet_{k-1} \bar{F}_2,$$

- or $\bar{F}_2, \bar{F}_1$ are $(k-1)$-composable and

$$F_1 = \bar{F}_2[\partial_k^-(\langle g_2 \rangle)] \bullet_{k-1} \bar{F}_1 \qquad F_2 = \bar{F}_2 \bullet_{k-1} \bar{F}_1[\partial_k^+(\langle g_1 \rangle)].$$

*Proof.* We prove the two lemmas by induction on $k$.

*Proof of Lemma B.5.1.* Let $p = |L_k|$. Since $U'$ is initial in $S$, $U' \cap L_k$ is initial for $\langle L_k \rangle$, so there exists a linear extension

$$\sigma: \mathbb{N}_p^* \to (L_k, \langle L_k \rangle)$$

such that $\{i \in \mathbb{N}_p^* | \sigma(i) \in U'\} = \{1, \dots, i_0\}$ for some $i_0 \in \mathbb{N}_p$. Writing $x_i$ for $\sigma(i)$ for $i \in \mathbb{N}_p^*$, by Theorem B.4.6, $L$ can be decomposed as

$$L = F_1[\langle x_1 \rangle] \bullet_{k-1} \cdots \bullet_{k-1} F_p[\langle x_p \rangle]$$

for some $(k-1)$-context classes $F_1, \dots, F_p$. For $i \in \{i_0 + 1, \dots, p\}$, we aim at transferring $F_i[x_i]$ from $L$ to $R$ using the relation $\approx_k$ on $k$-contexts. If $k = 1$, then $\langle x_1 \rangle, \dots, \langle x_p \rangle, \partial_1^+(\langle g \rangle)$ are 0-composable, so that

$$x_1 \triangleleft S' \cdots \triangleleft S' x_p \triangleleft S' \langle g \rangle_{1,\epsilon}$$

which implies that $x_1, \dots, x_p \in U'$ and $i_0 = p$. Thus, we can suppose that $k > 1$. Assume moreover that $i_0 < p$. To transfer the $F_i[x_i]$'s, our plan is to use Lemma B.5.2. We only need to show how to do this for $i = p$, and then iterate this procedure for $i \in \{i_0 + 1, \dots, p-1\}$.

Note that $F_p[\partial_{k-1}^+(\langle x_p \rangle)] = F[\partial_{k-1}^-(\langle g \rangle)]$. Moreover, since $x_p \notin U'$, we have $x_p \notin U$, so that

$$\langle x_p \rangle_{k-1,+} \cap \langle g \rangle_{k-1,-} = \emptyset.$$

Thus, using Lemma B.5.2 inductively, we get $(k-1)$-context classes $\bar{F}_p$ and $\bar{F}$ of type $\langle x_p \rangle$ and $\langle g \rangle$ such that
<figure><img src="image_28.png" /><figcaption>Figure 9: Illustration of Lemma B.5.1</figcaption></figure>

**Lemma B.5.2.** Let $k, n_1, n_2 \in \mathbb{N}^*$ with $k < \min(n_1, n_2)$, $g_1 \in P_{n_1}$, $g_2 \in P_{n_2}$, and $F_1, F_2$ be $k$-context classes of Cell($P$), of type $\langle g_1 \rangle$ and $\langle g_2 \rangle$ respectively, such that

$$F_1[\partial_k^+(\langle g_1 \rangle)] = F_2[\partial_k^-(\langle g_2 \rangle)] \quad \text{and} \quad \langle g_1 \rangle_{k,+} \cap \langle g_2 \rangle_{k,-} = \emptyset.$$

There exist $k$-context classes $\bar{F}_1, \bar{F}_2$ of type $\langle g_1 \rangle$ and $\langle g_2 \rangle$ respectively, such that

- either $\bar{F}_1, \bar{F}_2$ are $(k-1)$-composable and

$$F_1 = \bar{F}_1 \bullet_{k-1} \bar{F}_2[\partial_k^-(\langle g_2 \rangle)] \qquad F_2 = \bar{F}_1[\partial_k^+(\langle g_1 \rangle)] \bullet_{k-1} \bar{F}_2,$$

- or $\bar{F}_2, \bar{F}_1$ are $(k-1)$-composable and

$$F_1 = \bar{F}_2[\partial_k^-(\langle g_2 \rangle)] \bullet_{k-1} \bar{F}_1 \qquad F_2 = \bar{F}_2 \bullet_{k-1} \bar{F}_1[\partial_k^+(\langle g_1 \rangle)].$$

*Proof.* We prove the two lemmas by induction on $k$.

*Proof of Lemma B.5.1.* Let $p = |L_k|$. Since $U'$ is initial in $S$, $U' \cap L_k$ is initial for $\langle L_k \rangle$, so there exists a linear extension

$$\sigma: \mathbb{N}_p^* \to (L_k, \langle L_k \rangle)$$

such that $\{i \in \mathbb{N}_p^* | \sigma(i) \in U'\} = \{1, \dots, i_0\}$ for some $i_0 \in \mathbb{N}_p$. Writing $x_i$ for $\sigma(i)$ for $i \in \mathbb{N}_p^*$, by Theorem B.4.6, $L$ can be decomposed as

$$L = F_1[\langle x_1 \rangle] \bullet_{k-1} \cdots \bullet_{k-1} F_p[\langle x_p \rangle]$$

for some $(k-1)$-context classes $F_1, \dots, F_p$. For $i \in \{i_0 + 1, \dots, p\}$, we aim at transferring $F_i[x_i]$ from $L$ to $R$ using the relation $\approx_k$ on $k$-contexts. If $k = 1$, then $\langle x_1 \rangle, \dots, \langle x_p \rangle, \partial_1^+(\langle g \rangle)$ are 0-composable, so that

$$x_1 \triangleleft_{S'} \cdots \triangleleft_{S'} x_p \triangleleft_{S'} \langle g \rangle_{1,\epsilon}$$

which implies that $x_1, \dots, x_p \in U'$ and $i_0 = p$. Thus, we can suppose that $k > 1$. Assume moreover that $i_0 < p$. To transfer the $F_i[x_i]$'s, our plan is to use Lemma B.5.2. We only need to show how to do this for $i = p$, and then iterate this procedure for $i \in \{i_0 + 1, \dots, p-1\}$.

Note that $F_p[\partial_{k-1}^+(\langle x_p \rangle)] = F[\partial_{k-1}^-(\langle g \rangle)]$. Moreover, since $x_p \notin U'$, we have $x_p \notin U$, so that

$$\langle x_p \rangle_{k-1,+} \cap \langle g \rangle_{k-1,-} = \emptyset.$$

Thus, using Lemma B.5.2 inductively, we get $(k-1)$-context classes $\bar{F}_p$ and $\bar{F}$ of type $\langle x_p \rangle$ and $\langle g \rangle$ such that
- either $\bar{F}_p, \bar{F}$ are $(k-2)$-composable and

$$F_p = \bar{F}_p \bullet_{k-2} \bar{F}[\partial_{k-1}^-(\langle g \rangle)] \qquad F = \bar{F}_p[\partial_{k-1}^+(\langle x_p \rangle)] \bullet_{k-2} \bar{F}$$

- or $\bar{F}, \bar{F}_p$ are $(k-2)$-composable and

$$F_p = \bar{F}[\partial_{k-1}^-(\langle g \rangle)] \bullet_{k-2} \bar{F}_p \qquad F = \bar{F} \bullet_{k-2} \bar{F}_p[\partial_{k-1}^+(\langle x_p \rangle)]$$

By symmetry, we can suppose that we are in the first situation. Then, by axiom (≈-L) of $\approx_k$, we get that $E \approx_k \tilde{E}$ where $\tilde{E} = (\tilde{L}, \tilde{F}, \tilde{R})$ is such that

$$\begin{align*}
\tilde{L} &= F_1[\langle x_1 \rangle] \bullet_{k-1} \cdots \bullet_{k-1} F_{p-1}[\langle x_{p-1} \rangle] \\
\tilde{F} &= \bar{F}_p[\partial_{k-1}^-(\langle x_p \rangle)] \bullet_{k-2} \bar{F} \\
\tilde{R} &= (\bar{F}_p[\langle x_p \rangle] \bullet_{k-2} \bar{F}[\partial_{k-1}^+(\langle g \rangle)]) \bullet_{k-1} R
\end{align*}$$

By iterating the above procedure for $i \in \{i_0+1, \dots, p-1\}$, we obtain a $k$-context $E' = (L', F', R')$ of type $\langle g \rangle$ such that

$$E \approx_k E' \qquad L'_k = L_k \cap U' \qquad R'_k = R_k \cup (L_k \setminus U').$$

Using a similar method to transfer elements from $R'$ to $L'$, we get a $k$-context $E'' = (L'', F'', R'')$ of type $\langle g \rangle$ such that

$$E' \approx_k E'' \qquad L_k'' = L_k' \cup (R_k' \setminus V') \qquad R_k'' = R_k' \cap V'$$

Then, we have $E \approx_k E''$ and we compute that

$$\begin{align*}
L_k'' &= L_k' \cup (R_k' \setminus V') \\
&= (L_k \cap U') \cup (R_k \setminus V') \cup (L_k \setminus (U' \cup V')) \\
&= (L_k \cap U') \cup (R_k \cap U') && \text{(since } L_k \cup R_k = U' \cup V') \\
&= U'
\end{align*}$$

and, similarly, $R_k'' = V'$. Thus, $E''$ satisfies the wanted properties.

*Proof of Lemma B.5.2.* Let $E_k = (L^k, F'_k, R^k)$ be such that $[E_k] = F_k$ for $k \in \{1, 2\}$. Consider

$$\begin{align*}
M &= F_1[\partial_k^+(\langle g_1 \rangle)] && \text{(or, equivalently, } F_2[\partial_k^-(\langle g_2 \rangle)]\text{)}, \\
S_i &= L_k^i \cup R_k^i && \text{for } i \in \{1, 2\}, \\
S' &= M_k, \\
U_1 &= \{x \in S_1 \mid x \prec_{S'} \langle g_1 \rangle_{k,+}\} && V_1 = \{x \in S_1 \mid \langle g_1 \rangle_{k,+} \prec_{S'} x\}, \\
U_2 &= \{x \in S_2 \mid x \prec_{S'} \langle g_2 \rangle_{k,-}\} && V_2 = \{x \in S_2 \mid \langle g_2 \rangle_{k,-} \prec_{S'} x\}
\end{align*}$$

Since, by Axiom (T4), $g_1$ and $g_2$ are not in torsion with respect to $F_1[\partial_k^+(\langle g_1 \rangle)]$, we have

$$\text{either } \neg(\langle g_1 \rangle_{k,+} \prec_{S'} \langle g_2 \rangle_{k,-}) \text{ or } \neg(\langle g_2 \rangle_{k,-} \prec_{S'} \langle g_1 \rangle_{k,+}).$$

By symmetry, we can suppose that $\neg(\langle g_2 \rangle_{k,-} \prec_{S'} \langle g_1 \rangle_{k,+})$. Since we can use Lemma B.5.1 (which is proved for the current value of $k$) to change $E_1$ and $E_2$, we can suppose that

$$\begin{align*}
L_k^1 &= U_1, & R_k^1 &= S_1 \setminus U_1, \\
L_k^2 &= S_2 \setminus V_2, & R_k^2 &= V_2.
\end{align*}$$
- either $\bar{F}_p, \bar{F}$ are $(k-2)$-composable and

$$F_p = \bar{F}_p \bullet_{k-2} \bar{F}[\partial_{k-1}^-(\langle g \rangle)] \qquad F = \bar{F}_p[\partial_{k-1}^+(\langle x_p \rangle)] \bullet_{k-2} \bar{F}$$

- or $\bar{F}, \bar{F}_p$ are $(k-2)$-composable and

$$F_p = \bar{F}[\partial_{k-1}^-(\langle g \rangle)] \bullet_{k-2} \bar{F}_p \qquad F = \bar{F} \bullet_{k-2} \bar{F}_p[\partial_{k-1}^+(\langle x_p \rangle)]$$

By symmetry, we can suppose that we are in the first situation. Then, by axiom (≈-L) of $\approx_k$, we get that $E \approx_k \tilde{E}$ where $\tilde{E} = (\tilde{L}, \tilde{F}, \tilde{R})$ is such that

$$\begin{align*}
\tilde{L} &= F_1[\langle x_1 \rangle] \bullet_{k-1} \cdots \bullet_{k-1} F_{p-1}[\langle x_{p-1} \rangle] \\
\tilde{F} &= \bar{F}_p[\partial_{k-1}^-(\langle x_p \rangle)] \bullet_{k-2} \bar{F} \\
\tilde{R} &= (\bar{F}_p[\langle x_p \rangle] \bullet_{k-2} \bar{F}[\partial_{k-1}^+(\langle g \rangle)]) \bullet_{k-1} R
\end{align*}$$

By iterating the above procedure for $i \in \{i_0+1, \dots, p-1\}$, we obtain a $k$-context $E' = (L', F', R')$ of type $\langle g \rangle$ such that

$$E \approx_k E' \qquad L'_k = L_k \cap U' \qquad R'_k = R_k \cup (L_k \setminus U').$$

Using a similar method to transfer elements from $R'$ to $L'$, we get a $k$-context $E'' = (L'', F'', R'')$ of type $\langle g \rangle$ such that

$$E' \approx_k E'' \qquad L_k'' = L_k' \cup (R_k' \setminus V') \qquad R_k'' = R_k' \cap V'$$

Then, we have $E \approx_k E''$ and we compute that

$$\begin{align*}
L_k'' &= L_k' \cup (R_k' \setminus V') \\
&= (L_k \cap U') \cup (R_k \setminus V') \cup (L_k \setminus (U' \cup V')) \\
&= (L_k \cap U') \cup (R_k \cap U') && \text{(since } L_k \cup R_k = U' \cup V') \\
&= U'
\end{align*}$$

and, similarly, $R_k'' = V'$. Thus, $E''$ satisfies the wanted properties.

**Proof of Lemma B.5.2.** Let $E_k = (L^k, F'_k, R^k)$ be such that $[[E_k]] = F_k$ for $k \in \{1, 2\}$. Consider

$$\begin{align*}
M &= F_1[\partial_k^+(\langle g_1 \rangle)] && \text{(or, equivalently, } F_2[\partial_k^-(\langle g_2 \rangle)]\text{)}, \\
S_i &= L_k^i \cup R_k^i && \text{for } i \in \{1, 2\}, \\
S' &= M_k, \\
U_1 &= \{x \in S_1 \mid x \prec_{S'} \langle g_1 \rangle_{k,+}\} && V_1 = \{x \in S_1 \mid \langle g_1 \rangle_{k,+} \prec_{S'} x\}, \\
U_2 &= \{x \in S_2 \mid x \prec_{S'} \langle g_2 \rangle_{k,-}\} && V_2 = \{x \in S_2 \mid \langle g_2 \rangle_{k,-} \prec_{S'} x\}
\end{align*}$$

Since, by Axiom (T4), $g_1$ and $g_2$ are not in torsion with respect to $F_1[\partial_k^+(\langle g_1 \rangle)]$, we have

$$\text{either } \neg(\langle g_1 \rangle_{k,+} \prec_{S'} \langle g_2 \rangle_{k,-}) \text{ or } \neg(\langle g_2 \rangle_{k,-} \prec_{S'} \langle g_1 \rangle_{k,+}).$$

By symmetry, we can suppose that $\neg(\langle g_2 \rangle_{k,-} \prec_{S'} \langle g_1 \rangle_{k,+})$. Since we can use Lemma B.5.1 (which is proved for the current value of $k$) to change $E_1$ and $E_2$, we can suppose that

$$\begin{align*}
L_k^1 &= U_1, & R_k^1 &= S_1 \setminus U_1, \\
L_k^2 &= S_2 \setminus V_2, & R_k^2 &= V_2.
\end{align*}$$
<figure><img src="image_25.png" /><figcaption>Figure 10: The decomposition of M</figcaption></figure>

Then,

$$ (U_1 \cup \langle g_1 \rangle_{k,+}) \cap (\langle g_2 \rangle_{k,-} \cup V_2) = \emptyset $$

since, otherwise, it would contradict the condition $\neg(\langle g_2 \rangle_{k,-} \triangleleft_S' \langle g_1 \rangle_{k,+})$. Consider the following sets:

$$ \begin{align*} Q_1 &= U_1, & Q_2 &= \langle g_1 \rangle_{k,+}, \\ Q_3 &= S' \setminus (U_1 \cup \langle g_1 \rangle_{k,+} \cup \langle g_2 \rangle_{k,-} \cup V_2), & \\ Q_4 &= \langle g_2 \rangle_{k,-}, & Q_5 &= V_2. \end{align*} $$

Then $Q_1, Q_2, Q_3, Q_4, Q_5$ form a partition of $S'$. Moreover, this partition is compatible with $\triangleleft_S'$. Indeed, given $x, y \in S'$ such that $x \triangleleft_S' y$,

- if $x \in Q_2$, then we can not have $y \in Q_1$ since, by Axiom (T3), $\langle g_1 \rangle_{k,+}$ is a segment for $\triangleleft_S'$,

- if $x \in Q_3$, then we can not have $y \in Q_1 \cup Q_2$ (otherwise, we would have $x \in U_1 \cup \langle g_1 \rangle_{k,+}$),

- if $x \in Q_4$, then either $y \in Q_4$ or $y \in Q_5$ by definition of $Q_5$,

- if $x \in Q_5$, then $y \in Q_5$ since, by Axiom (T3), $\langle g_2 \rangle_{k,-}$ is a segment for $\triangleleft_S'$.

Thus, there exists a linear extension for $(S', \triangleleft_S')$

$$ \sigma: \mathbb{N}_{S'} \to S' $$

such that, for $i, j \in \mathbb{N}_{|S'|}$ and $r, s \in \mathbb{N}_5^*$, if $\sigma(i) \in Q_r$ and $\sigma(j) \in Q_s$ with $r < s$, then $i < j$. Since $S' = M_k$, using Theorem B.4.6, M can be written

$$ M = \prod_{i=1}^{|S'|} F_i[\langle \sigma(i) \rangle] $$

for some $(k-1)$-context classes $F_1, \dots, F_{|S'|}$. By gathering the terms corresponding to $Q_1, \dots, Q_5$ respectively, we obtain five $k$-cells $M^1, M^2, M^3, M^4, M^5 \in \text{Cell}(P)_k$ where

$$ M^j = \prod_{i \in \sigma^{-1}(Q_j)} F_i[\langle \sigma(i) \rangle] $$

as in Figure 10 and such that

$$ M = M^1 \bullet_{k-1} M^2 \bullet_{k-1} M^3 \bullet_{k-1} M^4 \bullet_{k-1} M^5. $$
<figure><img src="image_29.png" /><figcaption>Figure 10: The decomposition of M</figcaption></figure>

Then,

$$ (U_1 \cup \langle g_1 \rangle_{k,+}) \cap (\langle g_2 \rangle_{k,-} \cup V_2) = \emptyset $$

since, otherwise, it would contradict the condition $\neg(\langle g_2 \rangle_{k,-} \triangleleft_S' \langle g_1 \rangle_{k,+})$. Consider the following sets:

$$ \begin{align*} Q_1 &= U_1, & Q_2 &= \langle g_1 \rangle_{k,+}, \\ Q_3 &= S' \setminus (U_1 \cup \langle g_1 \rangle_{k,+} \cup \langle g_2 \rangle_{k,-} \cup V_2), & \\ Q_4 &= \langle g_2 \rangle_{k,-}, & Q_5 &= V_2. \end{align*} $$

Then $Q_1, Q_2, Q_3, Q_4, Q_5$ form a partition of $S'$. Moreover, this partition is compatible with $\triangleleft_S'$. Indeed, given $x, y \in S'$ such that $x \triangleleft_S' y$,

- if $x \in Q_2$, then we can not have $y \in Q_1$ since, by Axiom (T3), $\langle g_1 \rangle_{k,+}$ is a segment for $\triangleleft_S'$,

- if $x \in Q_3$, then we can not have $y \in Q_1 \cup Q_2$ (otherwise, we would have $x \in U_1 \cup \langle g_1 \rangle_{k,+}$),

- if $x \in Q_4$, then either $y \in Q_4$ or $y \in Q_5$ by definition of $Q_5$,

- if $x \in Q_5$, then $y \in Q_5$ since, by Axiom (T3), $\langle g_2 \rangle_{k,-}$ is a segment for $\triangleleft_S'$.

Thus, there exists a linear extension for $(S', \triangleleft_S')$

$$ \sigma: \mathbb{N}_{S'} \to S' $$

such that, for $i, j \in \mathbb{N}_{|S'|}$ and $r, s \in \mathbb{N}_5^*$, if $\sigma(i) \in Q_r$ and $\sigma(j) \in Q_s$ with $r < s$, then $i < j$. Since $S' = M_k$, using Theorem B.4.6, M can be written

$$ M = \prod_{i=1}^{|S'|} F_i[\langle \sigma(i) \rangle] $$

for some $(k-1)$-context classes $F_1, \dots, F_{|S'|}$. By gathering the terms corresponding to $Q_1, \dots, Q_5$ respectively, we obtain five $k$-cells $M^1, M^2, M^3, M^4, M^5 \in \text{Cell}(P)_k$ where

$$ M^j = \prod_{i \in \sigma^{-1}(Q_j)} F_i[\langle \sigma(i) \rangle] $$

as in Figure 10 and such that

$$ M = M^1 \bullet_{k-1} M^2 \bullet_{k-1} M^3 \bullet_{k-1} M^4 \bullet_{k-1} M^5. $$
Since

$$ \partial_{k-1}^{-}(L^{1}) = \partial_{k-1}^{-}(M) = \partial_{k-1}^{-}(M^{1}) \quad \text{and} \quad L_{k}^{1} = U_{1} = M_{k}^{1}, $$

by Lemma B.4.2, we have $L^1 = M^1$. Moreover, since

$$ \partial_{k-1}^{-}(F'_{1}[\langle g_1 \rangle]) = \partial_{k-1}^{+}(L^{1}) = \partial_{k-1}^{+}(M^{1}) = \partial_{k-1}^{-}(M^{2}) $$

and

$$ (F'_{1}[\partial_{k}^{+}(\langle g_{1} \rangle)])_{k} = \langle g_{1} \rangle_{k,+} = M_{k}^{2}, $$

by Lemma B.4.2, it follows that

$$ F'_{1}[\partial_{k}^{+}(\langle g_{1} \rangle)] = M^{2}. $$

Similarly, we can show that

$$ F'_{2}[\partial_{k}^{-}(\langle g_{2} \rangle)] = M^{4} \quad \text{and} \quad R^{2} = M^{5}. $$

Moreover, since

$$ \partial_{k-1}^{-}(L^{2}) = \partial_{k-1}^{-}(M) = \partial_{k-1}^{-}(M^{1} \bullet_{k-1} M^{2} \bullet_{k-1} M^{3}) $$

and

$$ L_{k}^{2} = S_{2} \setminus V_{2} = S' \setminus (\langle g_{2} \rangle_{k,-} \cup V_{2}) = Q_{1} \cup Q_{2} \cup Q_{3}, $$

by Lemma B.4.2, we have

$$ L^2 = M^1 \bullet_{k-1} M^2 \bullet_{k-1} M^3. $$

Similarly, we have

$$ R^1 = M^3 \bullet_{k-1} M^4 \bullet_{k-1} M^5. $$

Hence, writing

$$ \bar{F}_1 = \left[ \left( (L^1, F'_1, \mathrm{id}_{F'_1[\partial_{k-1}^+(\langle g_1 \rangle)]}) \right) \right] \quad \text{and} \quad \bar{F}_2 = \left[ \left( (M^3, F'_2, R^2) \right) \right] $$

we have $F_1 = \bar{F}_1 \bullet_{k-1} \bar{F}_2[\partial_k^-(g_2)]$ and $F_2 = \bar{F}_1[\partial_k^+(g_1)] \bullet_{k-1} \bar{F}_2$ as wanted. $\square$

We deduce that applied context classes are completely determined by their sources (or targets):

**Theorem B.5.3.** Given $k, n \in \mathbb{N}$ with $k < n$, $g \in P_n$ and $k$-context classes $F_1, F_2$ of type $\langle g \rangle$ such that

$$ \partial_k^{-}(F_1[\langle g \rangle]) = \partial_k^{-}(F_2[\langle g \rangle]) \quad \text{or} \quad \partial_k^{+}(F_1[\langle g \rangle]) = \partial_k^{+}(F_2[\langle g \rangle]), $$

we have $F_1 = F_2$.

*Proof.* By symmetry, it is enough to prove the case where $\partial_k^-(F_1[\langle g \rangle]) = \partial_k^-(F_2[\langle g \rangle])$. We prove this property by an induction on $k$. If $k = 0$, the result is trivial. So suppose that $k > 0$. Let

$$ E_1 = (L^1, F'_1, R^1) \quad \text{and} \quad E_2 = (L^2, F'_2, R^2) $$

be $k$-contexts such that $F_i = [E_i]$ for $i \in \{1, 2\}$. Thus,

$$ L^1 \bullet_{k-1} F'[\partial_k^-(\langle g \rangle)] \bullet_{k-1} R^1 = L^2 \bullet_{k-1} F'[\partial_k^-(\langle g \rangle)] \bullet_{k-1} R^2 $$
Since

$$ \partial_{k-1}^{-}(L^{1}) = \partial_{k-1}^{-}(M) = \partial_{k-1}^{-}(M^{1}) \quad \text{and} \quad L_{k}^{1} = U_{1} = M_{k}^{1}, $$

by Lemma B.4.2, we have $L^1 = M^1$. Moreover, since

$$ \partial_{k-1}^{-}(F'_{1}[\langle g_1 \rangle]) = \partial_{k-1}^{+}(L^{1}) = \partial_{k-1}^{+}(M^{1}) = \partial_{k-1}^{-}(M^{2}) $$

and

$$ (F'_{1}[\partial_{k}^{+}(\langle g_{1} \rangle)])_{k} = \langle g_{1} \rangle_{k,+} = M_{k}^{2}, $$

by Lemma B.4.2, it follows that

$$ F'_{1}[\partial_{k}^{+}(\langle g_{1} \rangle)] = M^{2}. $$

Similarly, we can show that

$$ F'_{2}[\partial_{k}^{-}(\langle g_{2} \rangle)] = M^{4} \quad \text{and} \quad R^{2} = M^{5}. $$

Moreover, since

$$ \partial_{k-1}^{-}(L^{2}) = \partial_{k-1}^{-}(M) = \partial_{k-1}^{-}(M^{1} \bullet_{k-1} M^{2} \bullet_{k-1} M^{3}) $$

and

$$ L_{k}^{2} = S_{2} \setminus V_{2} = S' \setminus (\langle g_{2} \rangle_{k,-} \cup V_{2}) = Q_{1} \cup Q_{2} \cup Q_{3}, $$

by Lemma B.4.2, we have

$$ L^2 = M^1 \bullet_{k-1} M^2 \bullet_{k-1} M^3. $$

Similarly, we have

$$ R^1 = M^3 \bullet_{k-1} M^4 \bullet_{k-1} M^5. $$

Hence, writing

$$ \bar{F}_1 = \left[ (L^1, F'_1, \mathrm{id}_{F'_1[\partial_{k-1}^+(\langle g_1 \rangle)]}) \right] \quad \text{and} \quad \bar{F}_2 = \left[ (M^3, F'_2, R^2) \right] $$

we have $F_1 = \bar{F}_1 \bullet_{k-1} \bar{F}_2[\partial_k^-(g_2)]$ and $F_2 = \bar{F}_1[\partial_k^+(g_1)] \bullet_{k-1} \bar{F}_2$ as wanted. $\square$

We deduce that applied context classes are completely determined by their sources (or targets):

**Theorem B.5.3.** Given $k, n \in \mathbb{N}$ with $k < n$, $g \in P_n$ and $k$-context classes $F_1, F_2$ of type $\langle g \rangle$ such that

$$ \partial_k^{-}(F_1[\langle g \rangle]) = \partial_k^{-}(F_2[\langle g \rangle]) \quad \text{or} \quad \partial_k^{+}(F_1[\langle g \rangle]) = \partial_k^{+}(F_2[\langle g \rangle]), $$

we have $F_1 = F_2$.

*Proof.* By symmetry, it is enough to prove the case where $\partial_k^-(F_1[\langle g \rangle]) = \partial_k^-(F_2[\langle g \rangle])$. We prove this property by an induction on $k$. If $k = 0$, the result is trivial. So suppose that $k > 0$. Let

$$ E_1 = (L^1, F'_1, R^1) \quad \text{and} \quad E_2 = (L^2, F'_2, R^2) $$

be $k$-contexts such that $F_i = [E_i]$ for $i \in \{1, 2\}$. Thus,

$$ L^1 \bullet_{k-1} F'[\partial_k^-(\langle g \rangle)] \bullet_{k-1} R^1 = L^2 \bullet_{k-1} F'[\partial_k^-(\langle g \rangle)] \bullet_{k-1} R^2 $$
In particular, $L_k^1 \cup \langle g \rangle_{k,-} \cup R_k^1 = L_k^2 \cup \langle g \rangle_{k,-} \cup R^2$ and, by Lemma 2.2.1, both sides are partitions, so that we have $L_k^1 \cup R_k^1 = L_k^2 \cup R_k^2$. Consider the following subsets of $P_k$:

$$S = L_k^1 \cup R_k^1,$$

$$U = \{x \in S \mid x \triangleleft_{S'} \langle g \rangle_{k,-}\},$$

$$S' = S \cup \langle g \rangle_{k,-},$$

$$V = S \setminus U.$$

By Lemma B.5.1, we can suppose that

$$L_k^1 = L_k^2 = U \quad \text{and} \quad R_k^1 = R_k^2 = V.$$

For $i \in \{1, 2\}$, we have

$$\partial_{k-1}^{-}(L^{i}) = \partial_{k-1}^{-}(F_{i}[\langle g \rangle]) = \partial_{k-1}^{-} \circ \partial_{k}^{-}(F_{i}[\langle g \rangle])$$

so that $\partial_{k-1}^{-}(L^1) = \partial_{k-1}^{-}(L^2)$. Thus, by Lemma B.4.2, we have $L^1 = L^2$ and, by a similar argument, $R^1 = R^2$. Moreover, for $i \in \{1, 2\}$, $\partial_{k-1}^{+}(L^i) = \partial_{k-1}^{-}(F_i'[\langle g \rangle])$, so

$$\partial_{k-1}^{-}(F_{1}'[\langle g \rangle]) = \partial_{k-1}^{-}(F_{2}'[\langle g \rangle]).$$

By induction hypothesis, we have $F_1' = F_2'$. Hence, $F_1 = F_2$. $\square$

**Freeness of general decompositions** We now handle the case of general decompositions of arbitrary lengths. First, we show an analogous of Theorem B.4.6, i.e., that the decompositions in Cell($P$)$^{n+}$ can also be reordered by linear extensions:

**Lemma B.5.4.** Let $n \in \mathbb{N}$ and $X$ be an $(n+1)$-cell of Cell($P$)$^{n+}$ such that

$$X = F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$$

for some $p \in \mathbb{N}$, $x_1, \dots, x_p \in P_{n+1}$ and n-context classes $F_1, \dots, F_p$ of Cell($P$). Then, we have that the function $q \mapsto x_q$ of type $\mathbb{N}_q^* \to X_{n+1}$ is a linear extension of $(X_{n+1}, \triangleleft_{X_{n+1}})$. Moreover, if $\sigma$ is a linear extension of $(X_{n+1}, \triangleleft_{X_{n+1}})$, then there exist n-context classes $\bar{F}_1, \dots, \bar{F}_p$ of respective types $\langle \sigma(1) \rangle, \dots, \langle \sigma(p) \rangle$ such that

$$X = \bar{F}_1[\sigma(1)] \bullet_n \cdots \bullet_n \bar{F}_p[\sigma(p)].$$

*Proof.* Write $\rho: \mathbb{N}_p \to X_{n+1}$ for the function such that $\rho(i) = x_i$ for $i \in \mathbb{N}_p^*$. By the functoriality of eval, we have

$$\mathrm{eval}(X) = F_1[\langle x_1 \rangle] \bullet_n \cdots \bullet_n F_p[\langle x_p \rangle]$$

so that $\rho$ is a linear extension by Proposition B.4.8. We are left to prove the second part of the statement. We have a morphism of linear extensions

$$f = \sigma^{-1} \circ \rho$$

between $\sigma$ and $\rho$. By Lemma B.4.1, we can suppose that $f = \tau_{i,i+1}$ for some $i \in \mathbb{N}_{p-1}^*$. To conclude, we only need to show that $x_i$ and $x_{i+1}$ can be swapped in the decomposition of $X$ as $F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$. By contradiction, suppose that $\langle x_i \rangle_{n,+} \cap \langle x_{i+1} \rangle_{n,-} \neq \emptyset$. In particular, we have $\rho(i) \triangleleft_{X_{n+1}} \rho(i+1)$. Since $\rho = \sigma \circ \tau_{i,i+1}$, it implies $\sigma(i+1) \triangleleft_{X_{n+1}} \sigma(i)$. Thus, since $\sigma$ is a linear extension, we deduce that $i+1 < i$, which is a contradiction. So $\langle x_i \rangle_{n,+} \cap \langle x_{i+1} \rangle_{n,-} = \emptyset$. By Lemma B.5.2, there exist n-context classes $\bar{F}_i$ and $\bar{F}_{i+1}$ such that, in Cell($P$)$^{\le n}[P_{n+1}] \approx$,

$$((x_i, F_i), (x_{i+1}, F_{i+1}))^s \approx ((x_{i+1}, \bar{F}_i), (x_i, \bar{F}_{i+1}))^s$$
In particular, $L_k^1 \cup \langle g \rangle_{k,-} \cup R_k^1 = L_k^2 \cup \langle g \rangle_{k,-} \cup R^2$ and, by Lemma 2.2.1, both sides are partitions, so that we have $L_k^1 \cup R_k^1 = L_k^2 \cup R_k^2$. Consider the following subsets of $P_k$:

$$S = L_k^1 \cup R_k^1,$$

$$U = \{x \in S \mid x \triangleleft_S' \langle g \rangle_{k,-}\},$$

$$S' = S \cup \langle g \rangle_{k,-},$$

$$V = S \setminus U.$$

By Lemma B.5.1, we can suppose that

$$L_k^1 = L_k^2 = U \quad \text{and} \quad R_k^1 = R_k^2 = V.$$

For $i \in \{1, 2\}$, we have

$$\partial_{k-1}^{-}(L^{i}) = \partial_{k-1}^{-}(F_{i}[\langle g \rangle]) = \partial_{k-1}^{-} \circ \partial_{k}^{-}(F_{i}[\langle g \rangle])$$

so that $\partial_{k-1}^{-}(L^1) = \partial_{k-1}^{-}(L^2)$. Thus, by Lemma B.4.2, we have $L^1 = L^2$ and, by a similar argument, $R^1 = R^2$. Moreover, for $i \in \{1, 2\}$, $\partial_{k-1}^{+}(L^i) = \partial_{k-1}^{-}(F_i'[\langle g \rangle])$, so

$$\partial_{k-1}^{-}(F_1'[\langle g \rangle]) = \partial_{k-1}^{-}(F_2'[\langle g \rangle]).$$

By induction hypothesis, we have $F_1' = F_2'$. Hence, $F_1 = F_2$. $\square$

**Freeness of general decompositions** We now handle the case of general decompositions of arbitrary lengths. First, we show an analogous of Theorem B.4.6, i.e., that the decompositions in Cell($P$)$^{n+}$ can also be reordered by linear extensions:

**Lemma B.5.4.** Let $n \in \mathbb{N}$ and $X$ be an $(n+1)$-cell of Cell($P$)$^{n+}$ such that

$$X = F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$$

for some $p \in \mathbb{N}$, $x_1, \dots, x_p \in P_{n+1}$ and n-context classes $F_1, \dots, F_p$ of Cell($P$). Then, we have that the function $q \mapsto x_q$ of type $\mathbb{N}_q^* \to X_{n+1}$ is a linear extension of $(X_{n+1}, \triangleleft_{X_{n+1}})$. Moreover, if $\sigma$ is a linear extension of $(X_{n+1}, \triangleleft_{X_{n+1}})$, then there exist n-context classes $\bar{F}_1, \dots, \bar{F}_p$ of respective types $\langle \sigma(1) \rangle, \dots, \langle \sigma(p) \rangle$ such that

$$X = \bar{F}_1[\sigma(1)] \bullet_n \cdots \bullet_n \bar{F}_p[\sigma(p)].$$

*Proof.* Write $\rho: \mathbb{N}_p \to X_{n+1}$ for the function such that $\rho(i) = x_i$ for $i \in \mathbb{N}_p^*$. By the functoriality of eval, we have

$$\mathrm{eval}(X) = F_1[\langle x_1 \rangle] \bullet_n \cdots \bullet_n F_p[\langle x_p \rangle]$$

so that $\rho$ is a linear extension by Proposition B.4.8. We are left to prove the second part of the statement. We have a morphism of linear extensions

$$f = \sigma^{-1} \circ \rho$$

between $\sigma$ and $\rho$. By Lemma B.4.1, we can suppose that $f = \tau_{i,i+1}$ for some $i \in \mathbb{N}_{p-1}^*$. To conclude, we only need to show that $x_i$ and $x_{i+1}$ can be swapped in the decomposition of $X$ as $F_1[x_1] \bullet_n \cdots \bullet_n F_p[x_p]$. By contradiction, suppose that $\langle x_i \rangle_{n,+} \cap \langle x_{i+1} \rangle_{n,-} \neq \emptyset$. In particular, we have $\rho(i) \triangleleft_{X_{n+1}} \rho(i+1)$. Since $\rho = \sigma \circ \tau_{i,i+1}$, it implies $\sigma(i+1) \triangleleft_{X_{n+1}} \sigma(i)$. Thus, since $\sigma$ is a linear extension, we deduce that $i+1 < i$, which is a contradiction. So $\langle x_i \rangle_{n,+} \cap \langle x_{i+1} \rangle_{n,-} = \emptyset$. By Lemma B.5.2, there exist n-context classes $\bar{F}_i$ and $\bar{F}_{i+1}$ such that, in Cell($P$)$^{\le n}[P_{n+1}] \approx$,

$$((x_i, F_i), (x_{i+1}, F_{i+1}))^s \approx ((x_{i+1}, \bar{F}_i), (x_i, \bar{F}_{i+1}))^s$$
so that

$$ ((x_1, F_1), \dots, (x_p, F_p))^s \\ \approx ((x_1, F_1), \dots, (x_{i-1}, F_{i-1}), (x_{i+1}, \bar{F}_i), (x_i, \bar{F}_{i+1}), (x_{i+2}, F_{i+2}), \dots, (x_p, F_p))^s $$

i.e., in Cell($P$)$^{n+}$,

$$ X = F_1[x_1] \bullet_n \cdots \bullet_n F_{i-1}[x_{i-1}] \bullet_n \bar{F}_i[x_{i+1}] \bullet_n \bar{F}_{i+1}[x_i] \bullet_n F_{i+2}[x_{i+2}] \cdots \bullet_n F_p[x_p] $$

which concludes the proof.

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

We can now deduce that $Cell(P)_{\le n+1}$ is canonically a free extension on $Cell(P)_{\le n}$:

**Theorem 2.4.1.** Given a torsion-free complex $P$, for $n \in \mathbb{N}$, the $(n+1)$-functor $eval^n$ is an isomorphism between $Cell(P)^{n+}$ and $Cell(P)_{\le n+1}$.

*Proof.* Since $eval_{\le n} = \text{id}_{Cell(P)_{\le n}}$, it is enough to prove that $eval$ induces a bijection on the $(n+1)$-cells. By Theorem B.4.6, it is surjective, so we are left to prove injectivity. Let $X^1$ and $X^2$ be $(n+1)$-cells of $Cell(P)^{n+}$, such that $eval(X^1) = eval(X^2)$ and

$$ X^i = F_1^i[x_1^i] \bullet_n \cdots \bullet_n F_{p_i}^i[x_{p_i}^i] $$

for some $p_i \in \mathbb{N}$, $x_1^i, \dots, x_{p_i}^i \in P_{n+1}$ and $n$-context classes $F_1^i, \dots, F_{p_i}^i$ for $i \in \{1, 2\}$. By functoriality of eval, we have

$$ \text{eval}(X^i) = F_1^i[\langle x_1^i \rangle] \bullet_n \cdots \bullet_n F_{p_i}^i[\langle x_{p_i}^i \rangle] $$

for $i \in \{1, 2\}$, so that, by Proposition B.4.8, we have $p_1 = p_2$, and we write $p$ for the common value. Moreover, $\{x_1^1, \dots, x_p^1\} = \{x_1^2, \dots, x_p^2\}$. By Lemma B.5.4, we can suppose that $x_j^1 = x_j^2$ for $j \in \mathbb{N}_p^*$, and we write $x_j$ for the common value. Since $\partial_n^-(X^i) = \partial_n^-(F_1^i[x_1])$ for $i \in \{1, 2\}$, we have

$$ \partial_n^-(F_1^1[x_1]) = \partial_n^-(F_1^2[x_1]) $$

so that, by Theorem B.5.3, $F_1^1 = F_1^2$. In particular, $\partial_n^+(F_1^1[x_1]) = \partial_n^+(F_1^2[x_1])$, so that

$$ \partial_n^-(F_2^1[x_2] \bullet_n \cdots \bullet_n F_p^1[x_p]) = \partial_n^-(F_2^2[x_2] \bullet_n \cdots \bullet_n F_p^2[x_p]). $$

Thus, we can iterate the above procedure to show that $F_j^1 = F_j^2$ for $j \in \{1, \dots, p\}$, so that we get $X^1 = X^2$. Hence, the $(n+1)$-functor eval is an isomorphism. □

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

$$ ((x_1, F_1), \dots, (x_p, F_p))^s \\ \approx ((x_1, F_1), \dots, (x_{i-1}, F_{i-1}), (x_{i+1}, \bar{F}_i), (x_i, \bar{F}_{i+1}), (x_{i+2}, F_{i+2}), \dots, (x_p, F_p))^s $$

i.e., in Cell($P$)$^{n+}$,

$$ X = F_1[x_1] \bullet_n \cdots \bullet_n F_{i-1}[x_{i-1}] \bullet_n \bar{F}_i[x_{i+1}] \bullet_n \bar{F}_{i+1}[x_i] \bullet_n F_{i+2}[x_{i+2}] \cdots \bullet_n F_p[x_p] $$

which concludes the proof.

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

We can now deduce that $Cell(P)_{\le n+1}$ is canonically a free extension on $Cell(P)_{\le n}$:

**Theorem 2.4.1.** Given a torsion-free complex $P$, for $n \in \mathbb{N}$, the $(n+1)$-functor $eval^n$ is an isomorphism between $Cell(P)^{n+}$ and $Cell(P)_{\le n+1}$.

*Proof.* Since $eval_{\le n} = \text{id}_{Cell(P)_{\le n}}$, it is enough to prove that $eval$ induces a bijection on the $(n+1)$-cells. By **Theorem B.4.6**, it is surjective, so we are left to prove injectivity. Let $X^1$ and $X^2$ be $(n+1)$-cells of $Cell(P)^{n+}$, such that $eval(X^1) = eval(X^2)$ and

$$ X^i = F_1^i[x_1^i] \bullet_n \cdots \bullet_n F_{p_i}^i[x_{p_i}^i] $$

for some $p_i \in \mathbb{N}$, $x_1^i, \dots, x_{p_i}^i \in P_{n+1}$ and $n$-context classes $F_1^i, \dots, F_{p_i}^i$ for $i \in \{1, 2\}$. By functoriality of $eval$, we have

$$ \mathrm{eval}(X^i) = F_1^i[\langle x_1^i \rangle] \bullet_n \cdots \bullet_n F_{p_i}^i[\langle x_{p_i}^i \rangle] $$

for $i \in \{1, 2\}$, so that, by **Proposition B.4.8**, we have $p_1 = p_2$, and we write $p$ for the common value. Moreover, $\{x_1^1, \dots, x_p^1\} = \{x_1^2, \dots, x_p^2\}$. By **Lemma B.5.4**, we can suppose that $x_j^1 = x_j^2$ for $j \in \mathbb{N}_p^*$, and we write $x_j$ for the common value. Since $\partial_n^-(X^i) = \partial_n^-(F_1^i[x_1])$ for $i \in \{1, 2\}$, we have

$$ \partial_n^-(F_1^1[x_1]) = \partial_n^-(F_1^2[x_1]) $$

so that, by **Theorem B.5.3**, $F_1^1 = F_1^2$. In particular, $\partial_n^+(F_1^1[x_1]) = \partial_n^+(F_1^2[x_1])$, so that

$$ \partial_n^-(F_2^1[x_2] \bullet_n \cdots \bullet_n F_p^1[x_p]) = \partial_n^-(F_2^2[x_2] \bullet_n \cdots \bullet_n F_p^2[x_p]). $$

Thus, we can iterate the above procedure to show that $F_j^1 = F_j^2$ for $j \in \{1, \dots, p\}$, so that we get $X^1 = X^2$. Hence, the $(n+1)$-functor $eval$ is an isomorphism. □

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

[1] Michael Barr and Charles Wells. *Toposes, Triples, and Theories*. Springer-Verlag, 2000.

[2] Michael A. Batanin. "Computads for finitary monads on globular sets". In: *Contemporary Mathematics* 230 (1998), pp. 37–58.

[3] Mitchell Buckley. "A formal verification of the theory of parity complexes". In: *Journal of Formalized Reasoning* 8.1 (2015), pp. 25–48.

[4] Albert Burroni. "Higher-dimensional word problems with applications to equational logic". In: *Theoretical Computer Science* 115.1 (1993), pp. 43–62.

[5] Alexander Campbell. "A higher categorical approach to Giraud's non-abelian cohomology". PhD thesis. Macquarie University, Australia, 2016.

[6] Simon Forest. *The categ program*. https://github.com/SimonForest/categ. 2020.

[7] Simon Forest. "Computational descriptions of higher categories". Theses. Institut Polytechnique de Paris, Jan. 2021. URL: https://tel.archives-ouvertes.fr/tel-03155192.

[8] Simon Forest and Samuel Mimram. "Describing free $\omega$-categories". In: *34th Annual Symposium on Logic in Computer Science (LICS)*. 2019, pp. 1–13.

[9] Amar Hadzihasanovic. *A combinatorial-topological shape category for polygraphs*. 2018. arXiv: 1806.10353.

[10] Simon Henry. *Non-unital polygraphs form a presheaf category*. 2017. arXiv: 1711.00744.

[11] Simon Henry. *Regular polygraphs and the Simpson conjecture*. 2018. arXiv: 1807.02627.

[12] Michael S. J. Johnson. "Pasting diagrams in $n$-categories with applications to coherence theorems and categories of paths". PhD thesis. University of Sydney, Australia, 1987.

[13] Michael S. J. Johnson. "The combinatorics of $n$-categorical pasting". In: *Journal of Pure and Applied Algebra* 62.3 (1989), pp. 211–225.

[14] Mikhail Kapranov and Vladimir Voevodsky. "$\infty$-groupoids and homotopy types". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.1 (1991), pp. 29–46.

[15] Mikhail Kapranov and Vladimir Voevodsky. "Combinatorial-geometric aspects of polycategory theory: pasting schemes and higher Bruhat orders (list of results)". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.1 (1991), pp. 11–27.

[16] Michael Makkai. *The word problem for computads*. 2005.

[17] François Métayer. "Cofibrant objects among higher-dimensional categories". In: *Homology, Homotopy and Applications* 10.1 (2008), pp. 181–203.

[18] Christopher Nguyen. "Parity structure on associahedra and other polytopes". PhD thesis. Macquarie University, Australia, 2017.

[19] A. John Power. "An $n$-categorical pasting theorem". In: *Category theory*. 1991, pp. 326–358.

[20] Carlos Simpson. *Homotopy types of strict 3-groupoids*. 1998. arXiv: math/9810059.

[21] Richard Steiner. "Omega-categories and chain complexes". In: *Homology, Homotopy and Applications* 6.1 (2004), pp. 175–200.

[22] Ross Street. "Limits indexed by category-valued 2-functors". In: *Journal of Pure and Applied Algebra* 8.2 (1976), pp. 149–181.
References

[1] Michael Barr and Charles Wells. *Toposes, Triples, and Theories*. Springer-Verlag, 2000.

[2] Michael A. Batanin. "Computads for finitary monads on globular sets". In: *Contemporary Mathematics* 230 (1998), pp. 37–58.

[3] Mitchell Buckley. "A formal verification of the theory of parity complexes". In: *Journal of Formalized Reasoning* 8.1 (2015), pp. 25–48.

[4] Albert Burroni. "Higher-dimensional word problems with applications to equational logic". In: *Theoretical Computer Science* 115.1 (1993), pp. 43–62.

[5] Alexander Campbell. "A higher categorical approach to Giraud's non-abelian cohomology". PhD thesis. Macquarie University, Australia, 2016.

[6] Simon Forest. *The categ program*. https://github.com/SimonForest/categ. 2020.

[7] Simon Forest. "Computational descriptions of higher categories". Theses. Institut Polytechnique de Paris, Jan. 2021. URL: https://tel.archives-ouvertes.fr/tel-03155192.

[8] Simon Forest and Samuel Mimram. "Describing free $\omega$-categories". In: *34th Annual Symposium on Logic in Computer Science (LICS)*. 2019, pp. 1–13.

[9] Amar Hadzihasanovic. *A combinatorial-topological shape category for polygraphs*. 2018. arXiv: 1806.10353.

[10] Simon Henry. *Non-unital polygraphs form a presheaf category*. 2017. arXiv: 1711.00744.

[11] Simon Henry. *Regular polygraphs and the Simpson conjecture*. 2018. arXiv: 1807.02627.

[12] Michael S. J. Johnson. "Pasting diagrams in $n$-categories with applications to coherence theorems and categories of paths". PhD thesis. University of Sydney, Australia, 1987.

[13] Michael S. J. Johnson. "The combinatorics of $n$-categorical pasting". In: *Journal of Pure and Applied Algebra* 62.3 (1989), pp. 211–225.

[14] Mikhail Kapranov and Vladimir Voevodsky. "$\infty$-groupoids and homotopy types". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.1 (1991), pp. 29–46.

[15] Mikhail Kapranov and Vladimir Voevodsky. "Combinatorial-geometric aspects of polycategory theory: pasting schemes and higher Bruhat orders (list of results)". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.1 (1991), pp. 11–27.

[16] Michael Makkai. *The word problem for computads*. 2005.

[17] François Métayer. "Cofibrant objects among higher-dimensional categories". In: *Homology, Homotopy and Applications* 10.1 (2008), pp. 181–203.

[18] Christopher Nguyen. "Parity structure on associahedra and other polytopes". PhD thesis. Macquarie University, Australia, 2017.

[19] A. John Power. "An $n$-categorical pasting theorem". In: *Category theory*. 1991, pp. 326–358.

[20] Carlos Simpson. *Homotopy types of strict 3-groupoids*. 1998. arXiv: math/9810059.

[21] Richard Steiner. "Omega-categories and chain complexes". In: *Homology, Homotopy and Applications* 6.1 (2004), pp. 175–200.

[22] Ross Street. "Limits indexed by category-valued 2-functors". In: *Journal of Pure and Applied Algebra* 8.2 (1976), pp. 149–181.
[23] Ross Street. "Parity complexes". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.4 (1991), pp. 315-343.

[24] Ross Street. "Parity complexes: corrigenda". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 35.4 (1994), pp. 359-361.

[25] Ross Street. "Categorical structures". In: *Handbook of Algebra*. Vol. 1. 1996, pp. 529-577.
[23] Ross Street. "Parity complexes". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 32.4 (1991), pp. 315-343.

[24] Ross Street. "Parity complexes: corrigenda". In: *Cahiers de Topologie et Géométrie Différentielle Catégoriques* 35.4 (1994), pp. 359-361.

[25] Ross Street. "Categorical structures". In: *Handbook of Algebra*. Vol. 1. 1996, pp. 529-577.