for $x$ a fresh variable name.

*Introduction of degenerate pasting diagrams.*

$$ \frac{\Gamma, x : T}{\Gamma, x : T \vdash \{x\}} \text{degen} $$

The shape of this pasting diagram is $(\{\{x\}\})^{\mathcal{H}} := \{\{x^{\mathcal{H}}\}\}$.

*Introduction of non-degenerate pasting diagrams.* If there exists $\mathbf{p} \in \mathbb{P}^{\surd}$ a non-degenerate opetope, say

$$ \mathbf{p} = \begin{cases} [p_1] & \leftarrow \psi_1 \\ \vdots \\ [p_k] & \leftarrow \psi_k \end{cases} $$

and typings $x_1 : T_1, \dots, x_k : T_k$ in the current context $\Gamma$ such that

(1) $x_i^{\mathcal{H}} = \psi_i$,

(2) (Inner) whenever $[p_j] = [p_i[q]]$ we have $\text{t}x_j = \mathfrak{s}_{[q]} x_i$, then:

$$ \frac{\Gamma}{\Gamma \vdash \begin{cases} [p_1] \leftarrow x_1 \\ \vdots \\ [p_k] \leftarrow x_k \end{cases}} \text{graft} $$

The shape of this pasting diagram is of course **p**.

*Shift to the next dimension.* If we have a pasting diagram **P** of shape $\mathbf{P}^{\mathcal{H}} = \mathbf{p}$, a cell $x : \mathbf{Q} \to a$ in the current context, such that

(1) $x^{\mathcal{H}} = \text{t}\mathbf{p}$,

(2) (Glob1) if $\mathbf{p}$ is non-degenerate, then $\text{t}\mathfrak{s}_{[q]} \mathbf{P} = \text{t}x$,

(3) (Glob2) if $\mathbf{p}$ is non-degenerate, then for a leaf $[p[q]] \in \mathbf{p}^{\mathcal{H}}$, we have $\mathfrak{s}_{[q]} \mathfrak{s}_{[p]} \mathbf{P} = \mathfrak{s}_{\mathcal{P}}[p[q]] x$,

(4) (Degen) if $\mathbf{p}$ is degenerate, then $\mathbf{Q} = \{[\,] \leftarrow a,$ then:

$$ \frac{\Gamma \vdash \mathbf{P}}{\Gamma, y : \mathbf{P} \to x} \text{shift} $$

for $y$ a fresh variable.

*Remark 4.46.* The syntax of *OPTSET?* is closely related to the notion of *FOLDS* [20]. In fact, the category $\mathcal{O}^{\text{op}}$ is a *FOLDS* signature with no relation symbols. Intuitively, each opetope $\omega$ corresponds to a sort, that depends on variables $a_f$ of type $\psi_f$, where $f : \omega \to \psi_f$ ranges over $\omega/\mathcal{O}^{\text{op}} - \{\text{id}_\omega\} \cong \mathcal{O}/\omega - \{\text{id}_\omega\}$. Since morphisms of $\mathcal{O}^{\text{op}}$ are generated by (opposites of) source and target embeddings, it is enough to consider the type $\omega$ to be only parametrized by $a_f$ where $f$ is a source or target embedding, modulo additional coherence conditions. For instance, if $\omega$ corresponds to the following preopetope

$$ \begin{cases} [p_1] & \leftarrow \psi_1 \\ \vdots \\ [p_k] & \leftarrow \psi_k \end{cases} $$
(the case where $\omega$ is degenerate is similar) then the following type in $\mathbf{OPTSET}^?$

$$ \left\{ \begin{array}{l} [p_1] \leftarrow x_1 \\ \vdots \\ [p_k] \leftarrow x_k \end{array} \right. \quad \rightarrow y $$

precisely represents the sort $\omega$ parametrized by variables $a_f$ of type $\psi_f$, where $f: \omega \to \psi_f$ is a source or target embedding: $a_{s[p_i]} := x_i$, and $a_t := y$. The side conditions of rules **graft** and **shift** guarantee that this indeed corresponds to a sort in FOLDS, namely, that we can find dependency variables $a_f$ for all $f \in \omega/\mathbb{O}^{\text{op}} - \{\text{id}_\omega\}$.

## 4.7 Equivalence with opetopic sets

**Definition 4.47 (Substitution).** Let $\Upsilon$ and $\Gamma$ be two derivable contexts in $\mathbf{OPTSET}^?$. Write the context $\Gamma$ as $(x_1 : T_1, \dots, x_k : T_k)$. By construction, $1 \le i \le k$, the variable $x_i$ does not occur in the type of $x_j$ whenever $j < i$. Akin to classical type theory (see e.g. [14, definition 2.11]), a substitution $\sigma : \Upsilon \to \Gamma$ is a sequence of variables $(\sigma_1, \dots, \sigma_k)$ such that for $1 \le i \le k$, the typing $\sigma_i : T_i[\sigma_1/x_1]\dots[\sigma_{i-1}/x_{i-1}]$ (i.e. $T_i$ where all instances of $x_j$ have been replaced by $\sigma_j$, for $1 \le j < i$) is in $\Upsilon$.

Write the context $\Upsilon$ as $(y_1 : U_1, \dots, y_l : U_l)$, and let $\tau = (\tau_1, \dots, \tau_l) : \Xi \to \Upsilon$ be another substitution. For $1 \le i \le k$, if $f(i)$ is the unique index such that $y_{f(i)} = \sigma_i$, then the composite $\tau\sigma : \Xi \to \Gamma$ is given by the sequence of variables $(\tau_{f(1)}, \dots, \tau_{f(k)})$.

Let $\mathfrak{C}\mathfrak{t}^?$ be the syntactic category of our type theory, i.e. the category whose objects are derivable contexts, and morphisms are substitutions as defined above.

**Lemma 4.48.** In the setting above, we have $\sigma_i^\flat = x_i^\flat$.

*Proof.* The shape of a variable, i.e. the shape of its source pasting diagram, does not depend on the variables present in it, only on its underlying preopetope. $\square$

Recall from definition 4.26 the *unnamed coding function* $C^? : \mathbb{O}_n \to \mathbb{P}_n^\square$.

**Definition 4.49 (Unnamed stratification).** We construct the *unnamed stratification functor* $S^? : (\mathfrak{C}\mathfrak{t}^?)^{\text{op}} \to \tilde{\mathbb{O}}_{\text{fin}}$. For $\Gamma \in \mathfrak{C}\mathfrak{t}^?$ and $\omega \in \mathbb{O}$, let

$$ S^?\Gamma_\omega := \{x \in \Gamma \mid x^\flat = C^? (\omega)\}. $$

If $x^\flat \neq \diamond$, then the type $X$ of $x$ is of the form $\mathbf{P} \to z$, and we let $tx:=z$. This is well defined as by construction of $\Gamma$ we have $z^\flat = t(x^\flat)$. For $[p] \in \omega^\bullet$, we let $s_{[p]} x := s_{[p]} \mathbf{P}$. Again, this is well-defined as $(s_{[p]} \mathbf{P})^\flat = s_{[p]}(\mathbf{P}^\flat) = s_{[p]}(x^\flat)$. From there, the opetopic identities clearly hold, and $S^?\Gamma$ is a finite opetopic set.

On morphisms, write $\Gamma = (x_1 : T_1, \dots, x_k : T_k)$, let $\sigma = (\sigma_1, \dots, \sigma_k) : \Upsilon \to \Gamma$ be a substitution, and define a morphism $S^?\sigma : S^?\Gamma \to S^?\Upsilon$ as follows. For $x_i$ a variable of $\Gamma$, and $\omega \in \mathbb{O}$ such that $C^? (\omega) = x_i^\flat$, there is a corresponding cell $x_i \in S^?\Gamma_\omega$, and we let $(S^?\sigma)(x_i) := \sigma_i$. This is well-defined since by lemma 4.48, we have $\sigma_i^\flat = x_i^\flat = \omega$, thus $\sigma_i \in S^?\Upsilon_\omega$.

**Lemma 4.50.** The map $S^?\sigma$ of definition 4.49 is a morphism of opetopic sets.
Proof. Assume $\omega \neq \diamond$, so that the type of $x_i$ is $\mathbf{P} \to x_j$ for some $j < i$, and the type of $\sigma_i$ is $\mathbf{P}[\sigma_1/x_1]\cdots[\sigma_{i-1}/x_{i-1}] \to \sigma_j$. Then $(S^?\sigma)(\mathbf{t}x_i) = \sigma_j = \mathbf{t}(S^?\sigma)(x_i)$. If $[p] \in \omega^\bullet$, then $\mathbf{s}_{[p]}x_i = x_l$, for some $l < i$, and

$$
\begin{align*}
(S^?\sigma)(\mathbf{s}_{[p]}x_i) &= (S^?\sigma)(x_l) \\
&= \sigma_l && \text{see definition 4.47} \\
&= \mathbf{s}_{[p]}(\mathbf{P}[\sigma_1/x_1]\cdots[\sigma_l/x_l]\cdots[\sigma_{i-1}/x_{i-1}]) \\
&= \mathbf{s}_{[p]}(S^?\sigma(x_i)) && \text{see definition 4.47.}
\end{align*}
$$

In conclusion, $S^?\sigma$ is compatible with the source and target maps, and thus is a morphism of opetopic sets $S^?\Gamma \to S^?\Upsilon$. $\square$

**Theorem 4.51.** *The stratification functor $S^? : (\mathbb{C}\mathrm{tx}^?)^{\mathrm{op}} \to \tilde{\mathbb{O}}_{\mathrm{fin}}$ is an equivalence of categories.*

*Proof.* It is clear from the definition that $S^?$ is a faithful functor. Let $\Gamma, \Upsilon \in \mathbb{C}\mathrm{tx}^?$ be derivable contexts, write $\Gamma$ as $(x_1 : T_1, \dots, x_k : T_k)$, and $f : S^?\Gamma \to S^?\Upsilon$. For $\sigma_f$ the substitution $(f(x_1), \dots, f(x_k)) : \Gamma \to \Upsilon$, we clearly have $f = S^?\sigma_f$, showing that $S^?$ is fully faithful.

We now show that $S^?$ is essentially surjective. Take $X \in \tilde{\mathbb{O}}_{\mathrm{fin}}$, and enumerate its cells as $x_1 \in X_{\omega_1}, \dots, x_k \in X_{\omega_k}$, such that whenever $i < j$ we have $\dim \omega_i \le \dim \omega_j$. In other words, they are sorted by dimension. We produce a sequence of derivable contexts $\Gamma^{(0)} \subseteq \Gamma^{(1)} \subseteq \dots \subseteq \Gamma^{(k)}$, where $\Gamma^{(i)} = (\overline{x_1} : T_1, \dots, \overline{x_i} : T_i)$ is such that $\overline{x_i}^\flat = C^? (\omega_i) = C^? (x_i^\flat)$. For $i = 0$, let $\Gamma^{(0)} = ()$. Assume $1 \le i \le k$, and that $\Gamma^{(i-1)}$ is defined and derivable.

(1) If $\omega_i = \diamond$, let $\Gamma^{(i)}$ be given by the following proof tree:

$$ \frac{\Gamma^{(i-1)}}{\Gamma^{(i-1)}, \bar{x}_i : \diamond} \text{ point} $$

Note that in this case, $T_i = \diamond$.

(2) Assume $\omega_i \neq \diamond$ is not degenerate. By induction $\overline{x_j}^\flat = C^? (x_j^\flat)$ for all $1 \le j < i$. In particular, for every address $[p] \in \omega_i^\bullet$, we have $\overline{s_{[p]}x_i}^\flat = \mathbf{s}_{[p]}C^? (\omega_i)$. Further, $\overline{tx_i}^\flat = C^? ((\mathbf{t}x_i)^\flat) = \mathbf{t}C^? (x_i^\flat)$. We define $\Gamma^{(i)}$ by the following proof tree:

$$
\frac{\Gamma^{(i-1)}}{\Gamma^{(i-1)} \vdash \left\{ \begin{array}{@{}l@{}} \overline{[p_1]} \leftarrow \overline{s_{[p_1]} x_i} \\ \vdots \\ \overline{[p_i]} \leftarrow \overline{s_{[p_i]} x_i} \end{array} \right. \xrightarrow{\text{shift}} \Gamma^{(i-1)}, \bar{x}_i : \left\{ \begin{array}{@{}l@{}} \overline{[p_1]} \leftarrow \overline{s_{[p_1]} x_i} \\ \vdots \\ \overline{[p_i]} \leftarrow \overline{s_{[p_i]} x_i} \end{array} \right. \xrightarrow{\text{graft}} \Gamma^{(i-1)} \right\}} \text{ graft}
$$

where the pasting diagram has shape $C^? (\omega)$, and $\{[p_1], \dots\} := \omega_i^\bullet$. The side conditions of *graft* and *shift* are met since $X$ is an opetopic set.

(3) If $\omega_i$ is degenerate, then $\Gamma^{(i)}$ is given by the following proof tree:

$$
\frac{\Gamma^{(i-1)}}{\Gamma^{(i-1)} \vdash \left\{ \begin{array}{@{}l@{}} \overline{\Gamma^{(i-1)}} \text{ degen} \\ \overline{\Gamma^{(i-1)} \vdash \{\overline{\mathbf{t}}\mathbf{t}x_i\}} \end{array} \right.} \xrightarrow{\text{shift}} \Gamma^{(i-1)}, \bar{x}_i : \left\{ \begin{array}{@{}l@{}} \overline{\{\overline{\mathbf{t}}\mathbf{t}x_i\}} \xrightarrow{\text{shift}} \overline{\mathbf{t}}x_i \end{array} \right.
$$
Finally, the mapping $x_i \mapsto \bar{x}_i$ exhibits an isomorphism $X \to S^?\Gamma^{(k)}$, and $S^?$ is essentially surjective. $\square$

The category $\mathcal{C}\mathit{tx}^?$ has finite limits, induced from finite colimits in $\mathbb{O}_{\mathbb{fin}}$ through $S^?$. We conclude this section with a result similar to theorem 3.102, stating that system $\mathcal{OPTSET}^?$ is a theory for opetopic sets.

**Theorem 4.52.** We have an equivalence $\mathbb{O} \simeq \mathcal{L}\mathcal{E}\mathit{X}(\mathcal{C}\mathit{tx}^?, \mathcal{S}\mathit{et})$.

*Proof.* This follows directly from theorem 4.51 and from the Gabriel–Ulmer duality [6] [17, theorem 8]. $\square$

**4.8 Examples** In this section, we give example derivations in system $\mathcal{OPTSET}^?$. For clarity, we do not repeat the type of previously typed variables in proof trees.

**Example 4.53.** We show how to derive the following opetopic set, which is not representable:

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

First, we introduce all the points:

$$ \frac{\text{point}}{a, b : \diamond} $$

Then we introduce $f$, by first specifying its source pasting diagram with the **graft** rule, parameterized by $\bullet = \{ * \leftarrow \diamond \}$, and then applying the **shift** rule:

$$ \frac{\text{graft}}{a, b, f : \{ * \leftarrow a \longrightarrow b \}} $$

We proceed similarly for $g$ and $h$:

$$ \frac{\text{graft}}{a, b, f, g : \{ * \leftarrow a \longrightarrow b \}} $$

Lastly, we introduce $\alpha$, first by specifying its source with the **graft** rule, parameterized by $\mathbf{1} = \{ \emptyset \leftarrow \bullet \}$ (see the opetopic integers defined in example 4.36), and applying the **shift** rule:

$$ \frac{\text{graft}}{a, b, f, g, h, \alpha : \{ \emptyset \leftarrow f \longrightarrow g \}} $$
**Example 4.54.** The opetopic set

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

is straightforwardly derived as

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

**Example 4.55 (A classic, maximally folded).** We derive the following opetopic set

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

where all 0-cells are the same cell $a$, all 1-cells are $f$, the 2-cells on the left are $\alpha$, the 2-cell on the right is $\beta$, and the 3-cell is $A$. Note that those identifications make the opetopic set not representable. We first derive $a$ and $f$:

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

Then we introduce $\alpha$, by first specifying its source pasting diagram with the *graft* rule, parameterized by opetope **2** = $\begin{Bmatrix} \llbracket & \leftarrow \bullet \\ \llbracket & \leftarrow \bullet \end{Bmatrix}$ (see the opetopic integers defined in example 4.36), and applying the *shift* rule:

<figure><img src="image_96.png" /></figure>
<figure><img src="image_97.png" /><figcaption>Figure 4.5: Derivation of example 4.55 using opetopy.NamedOpetope</figcaption></figure>
# Appendix A: Polynomial monads and the Baez-Dolan (-)$^+$ construction

Starting from a polynomial monad $M$ with set of operations $B$, the Baez-Dolan construction gives a new polynomial monad $M^+$ having $B$ as its set of colors. In this chapter, we study the monad structure of $M^+$ in depth.

**A.1 Polynomial monads** In this section, we show that three definitions of polynomial monads are equivalent: the “official one” as a monoid object in $\mathcal{P}oly\&nd(I)$ (see definition 2.23), the definition as $(-)^*$-algebra (see definition 2.24), and the definition by so-called partial laws (in the style of partial composition in operads or placed composition in multicategories).

**Definition A.1 (Partial laws).** Let $P$ be the following polynomial endofunctor:

$$I \leftarrow^s E \xrightarrow{p} B \xrightarrow{t} I.$$

A set of partial laws on $P$ is the datum of the following:

(Unit) a map $\eta: I \to B$;

(Partial multiplication) a map $\wedge: E \times_I B \to B$, where for $(e, b) \in E \times_I B$ and $a := p(e)$ we write $a \wedge e b$ instead of $\wedge(e, b)$, and say that the expression $a \wedge e b$ is admissible; this will be tacitly assumed from now on;

(Partial readdressing) for $a, b$, and $e$ as above, a bijective map $\rho_{a \wedge e b} : (E(a) - \{e\}) + E(b) \to E(a \wedge e b)$ over $I$;

such that the following conditions are satisfied:

(Trivial) for $i \in I$, we have $t(\eta(i)) = i$, and $E(\eta(i))$ is a singleton whose unique element $e$ is such that $s(e) = i$;

(Left unit) for $i \in I$, $b \in B$, and $e$ the unique element of $E(\eta(i))$, we have$^8$ $\eta(i) \wedge e b = b$, and $\rho_{\eta(i) \wedge e b} : E(b) \to E(b)$ is the identity;

(Right unit) for $i \in I$, $b \in B$, and $e \in E(b)$, we have $b \wedge e \eta(i) = b$, and $\rho_{b \wedge e \eta(i)}$ is given by

$$\begin{align*}
\rho_{b \wedge e \eta(i)} : (E(b) - \{e\}) + E(\eta(i)) &\to E(b) \\
x \in E(b) - \{e\} &\mapsto x \\
y \in E(\eta(i)) &\mapsto e;
\end{align*}$$

(Disjoint multiplication) for $a \wedge e b$ and $a \wedge_f c$, where $e \neq f$, we have

$$(a \wedge b) \wedge c = (a \wedge c) \wedge b,$$

where $f' := \rho_{a \wedge e b}(f)$ and $e' := \rho_{a \wedge_f c}(e)$, and the following coherence diagram commutes:

$$\begin{tikzcd}
(E(a) - \{e, f\}) + E(b) + E(c) \arrow[r, "\rho_{a \wedge e b}"] & (E(a \wedge e b) - \{f'\}) + E(c) \arrow[d, "\rho_{a \wedge_f c}"] \\
(E(a \wedge_f c) - \{e'\}) + E(b) \arrow[r, "\rho_{(a \wedge e b) \wedge_{f'} c}"] & E((a \wedge e b) \wedge_{f'} c);
\end{tikzcd} \quad (A.2)$$

(Nested multiplication) for $a \wedge e b$ and $b \wedge_f c$, we have

$$(a \wedge b) \wedge c = a \wedge (b \wedge c),$$

<footnote>$^8$Recall that expressions of the form $\rho_{a \wedge e b}$ are tacitly admissible. In this case, it means that $t(b) = s(e) = i$.</footnote>
**Proof.** Since $P$ is an algebra over the monad $(-)^*$, the following two diagrams commute:

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

where $m: P^* \to P$ is the structure map of $P$. The result follows by (tediously) unfolding these diagrams, together with the definition of $\eta$ and $\mu$ given in definition 2.24. $\square$

**Proposition A.11.** $A(-)^*-algebra, m: P^* \to P$ has partial laws.

**Proof.** Let the function $\eta$ of (Unit) map $i \in I$ to $m_1(l_i) \in B$. For $(e, b) \in E \times_I B$ and $a:=p(e)$, let $T:=Y_a \circ_{[e]} Y_b$, and $a \wedge_e b:=m_1(T)$. Note that

$$T^1 = \{[f] \mid f \in E(a), f \neq e\} \cup \{[ef] \mid f \in E(b)\}.$$

From here, one can check that the partial readdressing is simply given by

$$\begin{align*}
\rho_{a \wedge_e b} : (E(a) - \{e\}) + E(b) &\to E(a \wedge b) \\
[f], f \in E(a) - \{e\} &\mapsto \wp_T[f] \\
[ef], f \in E(b) &\mapsto \wp_T[ef],
\end{align*}$$

and that the required properties follow from lemma A.7. $\square$

**Remark A.12.** Combining the results of propositions A.4, A.6 and A.11, we obtain the following triangle of implications, featuring from left to right, *total composition* (the composition of a whole tree in one shot), *partial composition* (or placed composition), and *classical composition* (the composition of a tree of uniform height 2):

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

It can be shown that each implication is the object part of a functor, and that these functors are isomorphisms (the inverse of each being the composite of the other two). The situation is similar to the three definitions of symmetric operad given in [19, sections 5.3 and 5.5], namely *combinatorial*, *partial* and *classical*. As a matter of fact, polynomial monads are the same as coloured operads with a free action of the symmetric group.

**A.2 A complete $(-)^+$ construction** Recall from definition 2.29 that if $M$ is a polynomial monad

$$I \leftarrow^s E \rightarrow^p B \rightarrow^t I,$$

then the underlying polynomial endofunctor of $M^+$ is

$$B \leftarrow^s \mathrm{tr}^\bullet M \rightarrow^u \mathrm{tr} M \rightarrow^t B, \qquad (A.13)$$

where for $T \in \mathrm{tr} M$, the fiber $u^{-1}T$ (which we shall also denote by $T^\bullet$) is the set of node addresses in $T$, and for $[p] \in T^\bullet$, $s[p] := s_{[p]} T$.
**Theorem A.14 ([16, section 3.2])**. The polynomial endofunctor $M^+$ has a canonical structure of a polynomial monad. Using the definition by partial laws (definition A.1):

(Unit) the unit $B \to \text{tr} M$ maps $b$ to $Y_b$;

(Partial multiplication) the partial multiplication $\wedge : \text{tr}^\bullet M \times_B \text{tr} M \to \text{tr} M$ is given by substitution of trees (see definition 2.19), i.e. for $U \wedge_{[p]} T$ an admissible expression,

$$U \wedge_{[p]} T := U \sqcap_{[p]} T;$$

(Partial readdressing) for $U \sqcap_{[p]} T$ admissible, define $\rho_{U \sqcap_{[p]} T}$ by (see remark A.18 for a graphical explanation)

$$(U^{\bullet} - \{[p]\}) + T^{\bullet} \to (U \sqcap_{[p]} T)^{\bullet} \qquad [q] \in T^{\bullet} \mapsto [pq] \qquad (A.15)$$

$$[p[e]p'] \in U^{\bullet} \mapsto [p] \cdot \wp_T^{-1}(e) \cdot [p'] \qquad (A.16)$$

$$[q] \in U^{\bullet}, [p] \notin [q] \mapsto [q]. \qquad (A.17)$$

*Remark A.18.* Let $T$ and $U$ be $M^+$-trees as below respectively (we omit the decorations for simplicity), and $[p] \in U^{\bullet}$ the address of a node of $U$, say $b_2$, written in blue on the right:

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

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

Assuming $tT = s_{[p]}U$, the expression $U \sqcap_{[p]} T$ is admissible, and its evaluation gives

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

$\sqcap_{[p]}$

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

=

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

The map $\rho_{U \sqcap_{[p]} T}$ establishes a bijection between $U^{\bullet} + T^{\bullet} - \{[p]\}$ and the set of node addresses of $U \sqcap_{[p]} T$. Its definition is based on three cases.

*Case (A.15).* If $[q] \in T^{\bullet}$, then the address of the corresponding node in $U \sqcap_{[p]} T$ is simply
[pq]. This reflects that the tree T has been inserted in U at address [p].

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

*Case (A.16).* If a node $d$ of $U$ is located “above” the node that will be replaced by $T$, i.e. if $[p] \nsubseteq \&d$, then $\&d$ necessarily decomposes as $\&d = [p[e]p']$, where $[e] \in (s_{[p]}U)^{\bullet}$. In the example below, $d = b_4$, so that $[p'] = []$. On the other hand, there is a bijection $\wp_T$ between the leaves of $T$ and the input edges of $b_2$. Assuming $\wp_T^{-1}[e] = [l]$, the new address of $b_4$ in $U^{\square[p]}T$ is $[p] \cdot \wp_T^{-1}(e) \cdot [p'] = [plp']$.

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

*Case (A.17).* The last case concerns nodes of $U$ that are not located above $b_2$, and states that their address does not change.

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

*Proof of theorem A.14, (Trivial).* For $b \in B$ we have $tY_b = b$. On the other hand, $Y_b^{\bullet} = []$ and $s_{[]}Y_b = b$. $\square$

*Proof of (Left unit).* Let $b \in B$ and $T \in \text{tr}M$ be such that $Y_b^{\square[]}T$ is admissible. Then, by definition, $Y_b^{\square[]}T = T$. Then, $Y_b^{\bullet} + T^{\bullet} - [] = T^{\bullet}$, and $\rho_{Y_b^{\square[]}T}$ maps $[q] \in T^{\bullet}$ to $[q]$, so it is indeed the identity. $\square$
*Proof of (Right unit).* Let $b \in B$, $T \in \mathrm{tr} M$, and $[p] \in T^\bullet$ be such that $T \circled_{[p]} Y_b$ is admissible. By definition, $T \circled_{[p]} Y_b = T$. Then, $\rho_{T \circled_{[p]} Y_b}$ is given by

$$ (T^{\bullet} - \{[p]\}) + \{[]\} \to T^{\bullet} \\ [pep'] \in T^{\bullet} - \{[p]\} \mapsto [p] \cdot \rho_{Y_b}^{-1} e \cdot [p'] = [pep'] \\ [p'] \in T^{\bullet} - \{[p]\} \text{ not as above} \mapsto [p'] \\ [] \in Y_b^{\bullet} \mapsto [p] $$

as indeed $\rho_{Y_b}$ maps $[e] \in (Y_b)^{\circ}$ to $e \in E(b)$. $\square$

*Proof of (Disjoint multiplication).* Let $A \circled_{[e]} B$ and $A \circled_{[f]} C$ be two admissible expressions, where $[e] \neq [f]$. Without loss of generality, we distinguish two cases: one where $[e] \subseteq [f]$, and one where $[e]$ and $[f]$ are $\sqsubseteq$-incomparable.

(1) Assume $[e] \subseteq [f]$, so that $[f] = [eqr]$ for some $e$ and $r$, and decompose $A$ as

$$ A = X \circ_{[e]} (Y_t B \bigcirc_{[v_i]} V_i) \circ_{[q]} Y \circ_{[r]} Y_t C \bigcirc_{[w_j]} Z_j, $$

where $q \in E(tB)$, $\{v_i\}_i \subseteq E(tB) - \{q\}$, and $\{w_j\}_j \subseteq E(tC)$. Then

$$ A \circled_{[e]} B = X \circ_{[e]} (B \bigcirc_{\rho_B^{-1} v_i} V_i) \circ_{\rho_B^{-1} q} Y \circ_{[r]} Y_t C \bigcirc_{[w_j]} Z_j, $$

and $\rho_{A \circled_{[e]} B}[f] = \rho_{A \circled_{[e]} B}[eqr] = [e] \cdot \rho_B^{-1} q \cdot [r]$. Thus,

$$ (A \circled_{[e]} B) \circled_{[e]} C = X \circ_{[e]} (B \bigcirc_{\rho_B^{-1} v_i} V_i) \circ_{\rho_B^{-1} q} Y \circ_{[r]} C \bigcirc_{\rho_C^{-1} w_j} Z_j, $$

and the reindexing $\rho_{(A \circled_{[e]} B) \circled_{\rho_{A \circled_{[e]} B}[f]} C} \rho_{A \circled_{[e]} B}$ is given by

$$ \begin{align*} [p] \in B^{\bullet} &\mapsto [ep] & & \mapsto [ep] \\ [p] \in C^{\bullet} &\mapsto [ep] & & \mapsto [ep] \cdot \rho_B^{-1} q \cdot [rp] \\ [ev_i s] &\mapsto [ep] \cdot \rho_B^{-1} v_i \cdot [s] & & \mapsto [ep] \cdot \rho_B^{-1} v_i \cdot [s] \\ [eqs] \nvdash [f] &\mapsto [ep] \cdot \rho_B^{-1} q \cdot [s] & & \mapsto [ep] \cdot \rho_B^{-1} q \cdot [s] \\ [fw_j s] &\mapsto [ep] \cdot \rho_B^{-1} q \cdot [r] \cdot [w_j s] & & \mapsto [ep] \cdot \rho_B^{-1} q \cdot [r] \cdot \rho_C^{-1} w_j \cdot [s] \\ [p] \in A^{\bullet} \text{ n.a.a.} &\mapsto [p] & & \mapsto [p] \end{align*} $$

(n.a.a. is an acronym for “not as above”). On the other hand, we have

$$ A \circled_{[f]} C = X \circ_{[e]} (Y_t B \bigcirc_{[v_i]} V_i) \circ_{[q]} Y \circ_{[r]} C \bigcirc_{\rho_C^{-1} w_j} Z_j. $$

The reindexing gives $\rho_{A \circled_{[f]} C}[e] = [e]$, and

$$ \begin{align*} (A \circled_{[f]} C) \circled_{[e]} B &= X \circ_{[e]} (B \bigcirc_{\rho_B^{-1} v_i} V_i) \circ_{\rho_B^{-1} q} Y \circ_{[r]} C \bigcirc_{\rho_C^{-1} w_j} Z_j \\ &= (A \circled_{[e]} B) \circled_{[e]} C. \end{align*} $$

The reindexing $\rho_{(A \circled_{[f]} C) \circled_{[e]} B} \rho_{A \circled_{[f]} C}$ is given by
<figure><img src="image_108.png" /></figure>

We see that the square equation (A.2) commutes in the case $[e] \sqsubseteq [f]$.

(2) Assume $[e]$ and $[f]$ are $\sqsubseteq$-incomparable, and write $A$ as

$$A = (X \circled{[e]} \mathcal{Y}_{tB} \mathcal{O}_{Y_i} \circled{[f]} \mathcal{Y}_{tC} \mathcal{O}_{Z_j}.$$

Then

$$A \sqsubseteq B = (X \circled{[e]} B \mathcal{O}_{Y_i} \circled{[f]} \mathcal{Y}_{tC} \mathcal{O}_{Z_j}$$

the reindexing gives $\rho_{A \sqsubseteq [e]} B[f] = [f]$,

$$(A \sqsubseteq B) \circled{[f]} C = (X \circled{[e]} B \mathcal{O}_{Y_i} \circled{[f]} C \mathcal{O}_{Z_j}$$

and the complete reindexing $\rho_{(A \sqsubseteq [e]) B \circled{[f]} C} \rho_{A \sqsubseteq [e]} B$ is given by

$$ \begin{array}{ccc} [p] \in B^{\bullet} & \mapsto & [ep] \\ & & [p] \in C^{\bullet} \\ [ev_i s] & \mapsto & [e] \cdot \rho_B^{-1} v_i \cdot [s] \\ [fw_j s] & \mapsto & [fw_j s] \\ [p] \in A^{\bullet} \text{ n.a.a.} & \mapsto & [p] \end{array} \quad \begin{array}{ccc} \mapsto & [ep] & \\ \mapsto & [fp] & \\ \mapsto & [e] \cdot \rho_B^{-1} v_i \cdot [s] & \\ \mapsto & [f] \cdot \rho_C^{-1} w_j \cdot [s] & \\ \mapsto & [p] & \end{array} $$

On the other hand,

$$A \sqsubseteq C = (X \circled{[e]} \mathcal{Y}_{tB} \mathcal{O}_{Y_i} \circled{[f]} C \mathcal{O}_{Z_j}$$

we have $\rho_{A \sqsubseteq [f]} C[e] = [e]$,

$$ \begin{aligned} (A \sqsubseteq C) \circled{[f]} B &= (X \circled{[e]} B \mathcal{O}_{Y_i} \circled{[f]} C \mathcal{O}_{Z_j} \\ &= (A \sqsubseteq B) \circled{[e]} C, \end{aligned} $$

and further

$$ \begin{array}{ccc} [p] \in B^{\bullet} & \mapsto & [ep] \\ [ep] & \mapsto & [fp] \\ [ev_i s] & \mapsto & [ev_i s] \\ [fw_j s] & \mapsto & [f] \cdot \rho_C^{-1} w_j \cdot [s] \\ [p] \in A^{\bullet} \text{ n.a.a.} & \mapsto & [p] \end{array} \quad \begin{array}{ccc} \mapsto & [ep] & \\ \mapsto & [fp] & \\ \mapsto & [e] \cdot \rho_B^{-1} v_i \cdot [s] & \\ \mapsto & [f] \cdot \rho_C^{-1} w_j \cdot [s] & \\ \mapsto & [p] & \end{array} $$

so that the square equation (A.2) commutes in the case where the addresses $[e]$ and $[f]$ are $\sqsubseteq$-incomparable too. Finally, the monad structure of $M^+$ satisfies condition (Disjoint multiplication) of definition A.1. $\square$

*Proof of (Nested multiplication)*. Let $A, B, C \in \text{tr} M$, $[e] \in A^{\bullet}$, $[f] \in B^{\bullet}$, such that $A \sqsubseteq [e] B$ and $B \sqsubseteq [f] C$ are admissible. Write $A$ and $B$ as:

$$A = (X \circled{[e]} \mathcal{Y}_{tB} \mathcal{O}_{Y_i}), \quad B = Z \circled{[f]} \mathcal{Y}_{tC} \mathcal{O}_{T_j}.$$
Then,

$$A \square [e] B = X \circled B \circled Y_i, \\ [e] \qquad [e] \qquad \rho_B^{-1} v_i$$

we have $\rho_{A\square[e]} B[f] = [ef]$, and

$$(A \square B) \square C = X \circ (Z \circ Y_{tC} \circled T_j) \circled Y_i, \\ [e] \qquad [ef] \qquad [f] \qquad [w_j] \qquad \alpha(\rho_B^{-1} v_i)$$

where

$$\alpha(\rho_B^{-1} v_i) = \begin{cases} [f] \cdot \rho_C^{-1} w_j \cdot [r] & \text{if } \rho_B^{-1} v_i \text{ of the form } [fw_jr], \\ \rho_B^{-1} v_i & \text{otherwise.} \end{cases}$$

Remark that $\alpha(\rho_B^{-1} v_i) = \rho_{B\square[f]}^{-1} v_i$. The reindexing $\rho_{(A\square[e])B\square[ef]} C \rho_{A\square[e]} B$ is given by:

$$\begin{align*} [fw_jr] \in B^\bullet &\quad \mapsto \quad [efp] \\ [p] \in B^\bullet, [f] \not\sqsubseteq [p] &\quad \mapsto \quad [ef] \cdot \rho_C^{-1} w_j \cdot [r] \\ [ev_i r] \in A^\bullet &\quad \mapsto \quad [ep] \\ [e] \cdot \rho_B^{-1} v_i \cdot [r] &\quad \mapsto \quad [ep] \\ [e] \cdot \rho_{B\square[f]}^{-1} v_i \cdot [r] &\quad \mapsto \quad [ef] \cdot \rho_C^{-1} w_j \cdot [r] \end{align*}$$

On the other hand, we have

$$B \square [f] C = Z \circled C \circled T_j, \\ [f] \qquad \rho_C^{-1} w_j$$

$$\begin{align*} A \square (B \square C) &= X \circ (Z \circled Y_{tC} \circled T_j) \circled Y_i \\ & \qquad \rho_{B\square[f]}^{-1} v_i \\ &= (A \square B) \square [ef] C \end{align*}$$

and the reindexing is given by

$$\begin{align*} [p] \in C^\bullet &\quad \mapsto \quad [fp] &\quad \mapsto \quad [efp] \\ [fw_jr] \in B^\bullet &\quad \mapsto \quad [f] \cdot \rho_C^{-1} w_j \cdot [r] &\quad \mapsto \quad [ef] \cdot \rho_C^{-1} w_j \cdot [r] \\ [p] \in B^\bullet, [f] \not\sqsubseteq [p] &\quad \mapsto \quad [p] &\quad \mapsto \quad [ep] \\ [ev_i r] \in A^\bullet &\quad \mapsto \quad [e] \cdot \rho_{B\square[f]}^{-1} v_i \cdot [r] \end{align*}$$

We thus see that the square equation (A.3) commutes, and that the monad structure of $M^+$ satisfies condition (Nested multiplication). $\square$

This completes the proof of theorem A.14, endowing $M^+$ with a canonical monad structure, whose partial law is given by substitution of $M$-trees.
## References

[1] John C. Baez and James Dolan. Higher-dimensional algebra. III. *n*-categories and the algebra of opetopes. *Advances in Mathematics*, 135(2):145–206, 1998.

[2] Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. *arXiv e-prints*, page arXiv:1612.01093, December 2016.

[3] Eugenia Cheng. The category of opetopes and the category of opetopic sets. *Theory and Applications of Categories*, 11:No. 16, 353–374, 2003.

[4] Eric Finster. Opetopic.net. http://opetopic.net, May 2016.

[5] Eric Finster and Samuel Mimram. A Type-Theoretical Definition of Weak $\omega$-Categories. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–12, 2017.

[6] Peter Gabriel and Friedrich Ulmer. *Lokal präsentierbare Kategorien*. Lecture Notes in Mathematics, Vol. 221. Springer-Verlag, Berlin-New York, 1971.

[7] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. *Mathematical Proceedings of the Cambridge Philosophical Society*, 154(1):153–192, 2013.

[8] David Gepner, Rune Haugseng, and Joachim Kock. $\infty$-Operads as Analytic Monads. *International Mathematics Research Notices*, 04 2021. rnaa332.

[9] Victor Harnik, Michael Makkai, and Marek Zawadowski. Computads and multitopic sets. *arXiv:0811.3215 [math.CT]*, 2008.

[10] Claudio Hermida, Michael Makkai, and John Power. On weak higher dimensional categories. I. 1. *Journal of Pure and Applied Algebra*, 154(1-3):221–246, 2000. Category theory and its applications (Montreal, QC, 1997).

[11] Claudio Hermida, Michael Makkai, and John Power. On weak higher-dimensional categories. I. 3. *Journal of Pure and Applied Algebra*, 166(1-2):83–104, 2002.

[12] Cédric Ho Thanh. The equivalence between opetopic sets and many-to-one polygraphs. *arXiv:1806.08645 [math.CT]*, 2018.

[13] Cédric Ho Thanh. opetopy. https://github.com/altaris/opetopy, April 2018.

[14] Martin Hofmann. Syntax and semantics of dependent types. In *Semantics and logics of computation (Cambridge, 1995)*, volume 14 of *Publ. Newton Inst.*, pages 79–130. Cambridge Univ. Press, Cambridge, 1997.

[15] Joachim Kock. Polynomial functors and trees. *International Mathematics Research Notices*, 2011(3):609–673, January 2011.

[16] Joachim Kock, André Joyal, Michael Batanin, and Jean-François Mascari. Polynomial functors and opetopes. *Advances in Mathematics*, 224(6):2690–2737, 2010.

[17] Stephen Lack and John Power. Gabriel-Ulmer duality and Lawvere theories enriched over a general base. *Journal of Functional Programming*, 19(3-4):265–286, 2009.
[18] Tom Leinster. *Higher Operads, Higher Categories*. Cambridge University Press, 2004.

[19] Jean-Louis Loday and Bruno Vallette. *Algebraic operads*, volume 346. Springer Science & Business Media, 2012.

[20] Michael Makkai. First order logic with dependent sorts, with applications to category theory. Available at https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf, November 1995.