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

HAL
open science

# Type theoretical approaches to opetopes

Cédric Ho Thanh, Pierre-Louis Curien, Samuel Mimram

► To cite this version:

Cédric Ho Thanh, Pierre-Louis Curien, Samuel Mimram. Type theoretical approaches to opetopes. Higher Structures, 2022, 6 (1), pp.80 - 181. 10.21136/hs.2022.02. hal-04244406

HAL Id: hal-04244406

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

Submitted on 16 Oct 2023

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

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

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Type theoretical approaches to opetopes

Pierre-Louis Curien<sup>a</sup>, Cédric Ho Thanh<sup>a</sup> and Samuel Mimram<sup>b</sup>

## Abstract

Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak $\omega$-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster's approach, or as zoom complexes in the formalism of Kock et al.), using abstract constructions making them difficult to manipulate with a computer.

In this paper, we present two purely syntactic descriptions of opetopes as sequent calculi, the first using variables to implement the compositional nature of opetopes, the second using a calculus of higher addresses. We prove that well-typed sequents in both systems are in bijection with opetopes as defined in the more traditional approaches. Additionally, we propose three variants to describe opetopic sets. We expect that the resulting structures can serve as natural foundations for mechanized tools based on opetopes.

Communicated by: Richard Garner.

Received: 26th April, 2019. Accepted: 12th April, 2022.

MSC: Primary 18D50; Secondary 03B15.

Keywords: Opetope, Opetopic set, Type theory, Polynomial functor.

## 1. Introduction

1.1 **Opetopes** Opetopes were originally introduced by Baez and Dolan in order to formulate a definition of weak $\omega$-categories [1]. Their name reflects the fact that they encode the possible shapes for higher-dimensional operations: they are *operation polytopes*. Over the recent years, they have been the subject of many efforts to provide a good definition that would allow exploring their combinatorics [3, 10, 18]. One of the most commonly used nowadays is the formulation based

<footnote><sup>a</sup>Research Institute for Foundations of Computer Science (IRIF),
Paris University and CNRS, France</footnote>

<footnote><sup>b</sup>Computer Science Laboratory of École Polytechnique (LIX), Palaiseau, France</footnote>

<footnote>Email addresses: curien@irif.fr (P.L. Curien)
cedric.hothanh@irif.fr (C. Ho Thanh)
samuel.mimram@lix.polytechnique.fr (S. Mimram)</footnote>

<footnote>© P.L. Curien, C. Ho Thanh and S. Mimram, 2022, under a Creative Commons Attribution 4.0 International License.</footnote>

<footnote>DOI: 10.21136/HS.2022.02</footnote>
on polynomial functors and the corresponding graphical representation using “zoom complexes”
[16].

In order to grasp quickly the nature of opetopes, consider a sequence of four composable arrows

$$
a \xrightarrow{f} b \xrightarrow{g} c \xrightarrow{h} d \xrightarrow{i} e
$$

There are various ways we can compose them. For instance, we can compose $f$ with $g$, as well
as $h$ with $i$, and then $g \circ f$ with $i \circ h$. Or we can compose $f$, $g$ and $h$ together all at once, and
then the result with $i$. These two diagrams for composing can respectively be pictured

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

and

$$
f \xrightarrow{b} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5] \draw (-0.7,0) -- (0,0) -- (0.7,0) -- cycle; \node[below=0.3em] at (-0.3,0) {$g$}; \node[above=0.3em] at (0,0) {$h$}; \node[above=0.3em] at (0.3,0) {$d$}; \node[left=0.2em] at (-0.5,0) {$a$}; \node[right=0.2em] at (0.5,0) {$c$}; \node[right=0.2em] at (0.7,0) {$e$}; \node[above=0.3em] at (0.5,0.3) {$i$}; \node[above=0.3em] at (-0.5,0.3) {$j$}; \node[above=0.3em] at (0.5,-0.3) {$k$}; \node[left=0.2em] at (-0.5,-0.3) {$l$}; \node[right=0.2em] at (0.5,-0.3) {$e$}; \draw[->] (-0.7,0) -- (-0.2,0.3); \draw[->] (0,0) -- (0.2,0.3); \draw[->] (0.7,0) -- (0.2,-0.3); \draw[->] (0.7,0) -- (0.2,0.3); \end{tikzpicture} \quad (1.1) \\
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5] \draw (-0.7,0) -- (0,0) -- (0.7,0) -- cycle; \node[below=0.3em] at (-0.3,0) {$g$}; \node[above=0.3em] at (0,0) {$h$}; \node[above=0.3em] at (0.3,0) {$d$}; \node[left=0.2em] at (-0.5,0) {$a$}; \node[right=0.2em] at (0.5,0) {$c$}; \node[right=0.2em] at (0.7,0) {$e$}; \node[above=0.3em] at (0.5,0.3) {$i$}; \node[above=0.3em] at (-0.5,0.3) {$j$}; \node[above=0.3em] at (0.5,-0.3) {$k$}; \node[left=0.2em] at (-0.5,-0.3) {$l$}; \node[right=0.2em] at (0.5,-0.3) {$e$}; \draw[->] (-0.7,0) -- (-0.2,0.3); \draw[->] (0,0) -- (0.2,0.3); \draw[->] (0.7,0) -- (0.2,-0.3); \draw[->] (0.7,0) -- (0.2,0.3); \end{tikzpicture}
$$

From there, the general idea of getting “higher-dimensional” is that we should take these com-
positions as “2-operations”, which can be composed in various ways. For instance, in the first
case, we can compose $\alpha$ with $\gamma$, and then $\beta$ with the result, or all three at once, and so on.
The opetopes describe all the ways in which these compositions can be meaningfully specified,
in arbitrary dimension. We are also interested in *opetopic sets*, which are the carriers of such
composition operations. It is in this setting that Baez and Dolan proposed a definition of weak
$\omega$-category in [1].

We can expect (and it is indeed the case) that the combinatorics of these objects is not easy to
describe. In particular, a representation which is adapted to computer manipulations and proofs
is desirable: we can for instance mention the *Opetopic* proof assistant for higher categories [4],
which is based on opetopes. Recently, Mimram and Finster have introduced a language of a
type-theoretical flavour to describe globular weak $\omega$-categories [5]. Our goal is to achieve a
similar type-theoretic presentation for opetopic weak $\omega$-categories [1, 11]. Here, type-theoretical
is meant in the very broad sense of typed languages: there is a syntax for raw expressions, that
is then filtered by a type system inferring valid judgments, where the judgments have the form of
a claim that a given term indeed represents an opetope (or an opetopic set) in a certain context.

Let us now informally define opetopes. At the basis of the architecture, there is a unique
0-opetope (i.e. opetope of dimension 0), drawn as a point. An (n+1)-opetope (i.e. an opetope of
dimension n + 1) is made out of n-opetopes, and has a source and a target. In small dimensions,
opedopes can be described using drawings of the kind above. For instance, the following are,
from left to right, the unique 0-opetope, the unique 1-opetope, drawn as an arrow, and three
2-opetopes, respectively,

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

while the following drawing represents a 3-opetope:

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

In these drawings, the target of the 1-opetope is a point, the target of the 2-opetopes is the arrow
at the bottom, and the target of the 3-opetope is the 2-opetope on the right, while the source of
the 1-opetope is again a point, the source of the 2-opetopes is a diagram made of arrows, and the source of the 3-opetope is the diagram made of 2-opetopes on the left of the central arrow.

At this stage, we can already make the following observations:

(1) each drawing contains only one top-dimensional cell, whose dimension determines the dimension of the opetope,

(2) if an opetope has a non empty source, then its source and target have the same source (which might be empty) and the same target,

(3) if an opetope has an empty source, then its target has the same source and target,

(4) an $(n+1)$-cell can have multiple $n$-cells in its source (including none) but always has exactly one $n$-cell in its target.

By the above remarks, an $n$-opetope has a unique top-dimensional cell $\alpha$, whose target consists of one cell $\beta$ whose source and target are the same as the ones of the source of $\alpha$. It follows recursively that the opetope is entirely determined by the source of $\alpha$, which we call the associated *pasting diagram*, which is of dimension $n-1$. The opetope associated to a pasting diagram of dimension $n$ can be obtained by adding a single cell $\beta$ of dimension $n$ parallel to the pasting diagram, and an $(n+1)$-cell $\alpha$ from the pasting diagram to $\beta$.

This article aims to provide type-theoretical tools making opetopes easier to manipulate than their classical definitions. The *unnamed* (or *anonymous*) approaches of section 4 are purely relying on a calculus of higher addresses, and on a syntactic notion of *preopetope*. Opetopes are then well-formed preopetopes according to the derivation system $OPT^?_{\alpha}$ presented in definition 4.17, while opetopic sets are derivable contexts in system $OPT_{\alpha}^?_{\beta}$. The *named* approaches of section 3, while slightly more complicated, leverage the idea of cell naming to produce user friendlier tools and results. As such it comes in two variants: $OPT^?_{\alpha}$ for describing opetopes, and $OPT_{\alpha}^?_{\beta}$ for opetopic sets, introduced in definitions 3.23 and 3.71 respectively. The Python implementation of [13] is also discussed.

## 1.2 Generating opetopes

Our two opetope derivation systems $OPT^?_{\alpha}$ (definition 3.23) and $OPT^?_{\beta}$ (definition 4.17) are based on the observation that opetopes are precisely all the shapes one can generate with the following operations.

(1) *Introduction of a point*. There is a unique 0-opetope (the *point*).

______ point

(2) *Shift to the next dimension*. Given an $n$-opetope $\omega$, we can form the $(n+1)$-globe whose source and target are $\omega$, as illustrated below. It can geometrically be thought of as the “extrusion” of $\omega$.

<figure><img src="image_6.png" /></figure>
(3) *Introduction of degeneracies*. Given an *n*-opetope $\omega$, we can build an (*n*+2)-opetope with empty source, whose target is the globe at $\omega$, as illustrated below for $n = 0$ and $n = 1$:

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

(4) *Grafting*. Given an (*n* + 1)-opetope $\alpha$ and an (*n* + 1)-pasting diagram $\beta$ such that the source of $\beta$ contains an *n*-cell of the same shape as the target of $\alpha$, we can graft $\alpha$ to $\beta$:

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

Ill-formed graftings may occur with *n*-pasting diagrams, for $n \ge 3$, and the side condition is necessary to rule them out. Here is an example the *graft* rule will not allow: we deal with a 3-pasting diagram on the right of the dashed arrow (that comprises a unique 3-opetope), and the dashed arrow indicates that we attempt to graft the 3-opetope on the left (whose target shape is a trapezoid) onto the triangle shaped cell on the right

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

However, grafting onto the lower trapezoid of the right opetope is possible:

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

As previously mentioned, an opetope is completely determined by its source pasting diagram, i.e. “arrangement” of source faces (the dichotomy between opetopes and pasting diagrams is more thoroughly discussed in section 2.2.2). We can reformulate rules **shift** and **graft** with this point of view to respectively obtain:

(1) *Filling of pasting diagrams*. Given an *n*-pasting diagram, we may “fill” it by adding a target *n*-cell, and a top dimensional (*n* + 1)-cell. We illustrate an instance of this rule on the left, and invite the reader to compare it with the instance of **shift** on the right:

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

(2) *Substitution*, which consists in replacing a cell in a pasting diagram by another “parallel” pasting diagram. As before, we illustrate an instance if this rule on the left, and invite
the reader to compare it with the instance of *graft* on the right:

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

Substitution can be further illustrated as follows:

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

Rules *point* and *degen* can also be reformulated in term of pasting diagrams, but representing them graphically is not as insightful.

**1.3 Plan** In section 2, we expound some prerequisites and general ideas motivating our syntactic approaches. We then present the “unnamed” and “named” systems for opetopes and opetopic sets in sections 3 and 4 respectively. Those two chapters can be read independently, but have a similar structure:

(1) firstly, we present the syntactic constructs and inference rules of systems $OPT^1$ (named) and $OPT^?$ (unnamed) for opetopes, in sections 3.1 and 4.1 respectively;

(2) we then prove the equivalence with opetopes as defined in [16] (which we shall refer to as *polynomial opetopes*) in sections 3.2 and 4.2;

(3) we showcase the $OPT^1$ and $OPT^?$ systems in examples in sections 3.3 and 4.3;

(4) we discuss the Python implementation of $OPT^1$ and $OPT^?$ of [13] in sections 3.4 and 4.5;

(5) in the second part of those chapters, we present the syntactic constructs and inference rules of systems $OPTSET^1$ (named) and $OPTSET^?$ (unnamed) for opetopic sets, in sections 3.5 and 4.6 respectively;

(6) we then prove the equivalence with opetopic sets of [12] in sections 3.6 and 4.7;

(7) we showcase the $OPTSET^1$ and $OPTSET^?$ systems in examples in sections 3.7 and 4.8;

(8) we discuss the Python implementation of $OPTSET^1$ and $OPTSET^?$ sections 3.8 and 4.9;

(9) for the named approach of section 3, we present the additional “mixed” system $OPTSET_M^1$ in section 3.9, with the same plan as previously presented.

The equivalence proofs with polynomial opetopes of sections 3.2 and 4.2 rely on a precise definition of the Baez-Dolan $(-)^+$ construction [16, 1], which is presented in appendix A.

**1.4 Related works** Our syntactic opetopes are shown in sections 3.2 and 4.2 to be equivalent to the polynomial opetopes (or “zoom complexes”) of Kock et al. [16], which are themselves equivalent to Leinster’s opetopes [18]. It is known that the latter are incompatible with Cheng’s opetopes [3], which should be thought of as being symmetric. There is a closely related notion of *multitope* [11, 9] which is defined in terms of multicategories (whence the *multi*) instead of operads (*ope*); the two notions can be shown to be equivalent [12]. A syntax for multitopes was
proposed in [11], where however not all the desired computations have been given algorithmic formulations.

The *Opetopic* proof assistant [4] for weak higher categories relies on the notion of higher-dimensional tree. In that system, the notion of opetope is built-in, so that we have to trust the implementation. In contrast, the present approach allows us to reason about the construction of opetopes. We moreover believe that the ability to reason by induction on the proof trees, together with the very explicit nature of our syntaxes, will allow for optimizations in the automated manipulations of opetopes.

Another proof assistant for weak higher categories, called *CaTT* [5], starts from the same idea of generating well-formed pasting diagrams through inference rules. However, it is based on globular shapes instead of opetopic ones, making a comparison with the present work difficult: since their introduction, people have unsuccessfully tried to compare the resulting respective categorical formalisms; we hope that their formulation in a common logical language might be of help in this task.

We should also mention here the *Globular* proof assistant [2], also based on globular shapes, which is quite popular, notably thanks to its nice graphical interface.

**Acknowledgments** We would like to thank the anonymous referee for their scrupulous review and valuable advices. The second author has received funding from the European Union's Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement №665850.

## 2. Preliminaries

This chapter introduces the theory of polynomial functors, trees, and monads of [15, 7], and applies it to the definition of opetopes in the style of Kock et. al. [16].

### 2.1 Polynomial endofunctors and trees

#### 2.1.1 Definitions

**Definition 2.1** (Polynomial endofunctor [7, paragraph 1.4]). A polynomial endofunctor $P$ is a diagram in Set of the form

$$ I \leftarrow^{s} E \rightarrow^{p} B \rightarrow^{t} I. \qquad (2.2) $$

We use the following terminology for a polynomial endofunctor $P$ as in equation (2.2), which is motivated by the intuition that a polynomial endofunctor encodes a multi-sorted signature of function symbols. The elements of $B$ are called the *nodes* or *operations* of $P$, and for every node $b$, the elements of the fibre $E(b) := p^{-1}(b)$ are called the *inputs* of $b$. The elements of $I$ are called the *colors* or *sorts* of $P$. For every input $e$ of a node $b$, we denote its color by $s_e(b) := s(e)$.

<figure><img src="image_14.png" /></figure>
In this paper, all polynomial functors are assumed to be *finitary*, meaning that all the fibers of $p$ in (2.2) are finite. In other words, every operation has finitely many inputs.

**Definition 2.3** (Morphism of polynomial endofunctor). A morphism $f$ from a polynomial endofunctor $P$ over $I$ (on the first row) to a polynomial endofunctor $P'$ over $I'$ (on the second row) is a commutative diagram of the form

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

where the middle square is cartesian (i.e. is a pullback square). If $P$ and $P'$ are both polynomial endofunctors over $I$, then a morphism from $P$ to $P'$ over $I$ is a commutative diagram as above, but where $f_0$ is required to be the identity [15, paragraph 0.1.3] [16, section 2.5]. Let $\mathcal{Poly\&nd}$ denote the category of polynomial endofunctors and morphisms of polynomial endofunctors, and $\mathcal{Poly\&nd}(I)$ the category of polynomial functors over $I$ and morphisms of polynomial endofunctors over $I$.

*Remark 2.4.* A polynomial functor $P$ as in equation (2.2) induces a functor $P = t_!p_*s^* : \mathcal{Set}/I \to \mathcal{Set}/I$, where $t_!$ is the dependent sum along $t$, $p_*$ is the dependent product along $p$, and $s^*$ is the pullback along $s$. Furthermore, morphisms between polynomial functors induce cartesian natural transformations<fnref n="1" /> [7, paragraph 2.1].

**Definition 2.5** (Polynomial tree [15, section 1.0.3]). A polynomial endofunctor $T$ given by

$$T_0 \leftarrow^s T_2 \xrightarrow{p} T_1 \xrightarrow{t} T_0$$

is a polynomial tree (or just tree) if

(1) the sets $T_0$, $T_1$ and $T_2$ are finite (in particular, each node has finitely many inputs); by convention we assume $T_0 \neq \emptyset$;

(2) the map $t$ is injective;

(3) the map $s$ is injective, and the complement of its image $T_0$ – im $s$ has a single element, called the *root*;

(4) let $T_0 = T_2 + \{r\}$, with $r$ the root, and define the *walk-to-root* function $\sigma$ by $\sigma(r) = r$, and otherwise $\sigma(e) = tp(e)$; then we ask that for all $x \in T_0$, there exists $k \in \mathbb{N}$ such that $\sigma^k(x) = r$.

We call the colors of a tree its *edges* and the inputs of a node the *input edges* of that node.

Let $\mathcal{Tree}$ be the full subcategory of $\mathcal{Poly\&nd}$ whose objects are trees. Note that it is the category of *symmetric* or *non-planar* trees (the automorphism group of a tree is in general non-trivial) and that its morphisms correspond to inclusions of non-planar subtrees. An *elementary tree* is a tree with at most one node, and we write $\mathcal{Tree}_{\text{elem}}$ for the full subcategory of $\mathcal{Tree}$ spanned by elementary trees.

**Definition 2.6** (*P*-tree). For $P \in \mathcal{Poly\&nd}$, the category tr $P$ of *P*-trees is a chosen skeleton of the slice category $\mathcal{Tree}/P$.

<footnote n="1">¹Recall that a natural transformation is *cartesian* if all its naturality squares are pullback squares.</footnote>
**Notation 2.7.** A P-tree $T \in \text{tr} P$ is a morphism from a polynomial tree, which we shall denote by $\langle T \rangle$, to $P$, as in $T: \langle T \rangle \to P$. We point out that $\langle T \rangle_1$ is the set of nodes of the P-tree $T$, while $T_1: \langle T \rangle_1 \to P_1$ provides a *decoration* of the nodes of $\langle T \rangle$ by operations of $P$, and likewise for edges.

**Definition 2.8 (Address).** Let $T: \langle T \rangle \to P$ be a P-tree, and $\sigma$ be its walk-to-root function (definition 2.5). We define the *address function* & on edges of $\langle T \rangle$ inductively as follows:

(1) if $r$ is the root edge of $\langle T \rangle$, let $\& r := []$;

(2) if $i \in \langle T \rangle_0 - \{r\}$ and if $\& \sigma(i) = [x]$, where $\sigma$ is the walk-to-root function of $\langle T \rangle$, define $\& i := [x T_2(e)]$, where $e \in \langle T \rangle_2$ is the unique element such that $s(e) = i$.

Thus an address is a sequence of elements of $P_2$, which we always enclose with brackets. The address of a node $b \in \langle T \rangle_1$ is simply $\& b := \& t(b)$. Note that this function is injective since $t$ is. Let $T^\bullet$ denote its image, the set of *node addresses* of $T$, and let $T^1$ be the set of addresses of leaf edges, i.e. those edges not in the image of $t$.

If $b \in \langle T \rangle_1$, let $\& b := \& t(b)$. Furthermore, & is still injective since the square

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

is cartesian. If $b \in \langle T \rangle_1$ has address $\& b = [p]$, write $s_{[p]} T := T_1(b)$ for the decoration of node $b$. Likewise, if an edge $i$ has address $[q]$, let $e_{[q]} T := T_0(i)$ be its decoration.

**Definition 2.9 (Elementary P-trees).** Let $P$ be a polynomial endofunctor as in equation (2.2). For $i \in I$, define $l_i \in \text{tr} P$ as having underlying tree

$$ \{i\} \leftarrow \emptyset \longrightarrow \emptyset \longrightarrow \{i\}, \qquad (2.10) $$

along with the obvious morphism to $P$, that which maps $i$ to $i \in I$. This corresponds to a tree with no nodes and a unique edge, decorated by $i$. For $b \in B$, define $Y_b \in \text{tr} P$, the *corolla* at $b$, as having underlying tree

$$ s(E(b)) + \{\ast\} \leftarrow^s E(b) \longrightarrow \{b\} \longrightarrow s(E(b)) + \{\ast\}, \qquad (2.11) $$

where the right map sends $b$ to $\ast$, and where the morphism $Y_b \to P$ is the identity on $s(E(b)) \subseteq I$, maps $\ast$ to $t(b) \in I$, is the identity on $E(b) \subseteq E$, and maps $b$ to $b \in B$. This corresponds to a P-tree with a unique node, decorated by $b$. Observe that for $T \in \text{tr} P$, giving a morphism $l_i \to T$ is equivalent to specifying the address $[p]$ of an edge of $T$ decorated by $i$. Likewise, morphisms of the form $Y_b \to T$ are in bijection with addresses of nodes of $T$ decorated by $b$.

**Remark 2.12.** Let $P$ be a polynomial endofunctor as in equation (2.2).

(1) Let $i \in I$ be a color of $P$. Since $l_i$ does not have any nodes, the set $l_i^\bullet$ of its node addresses is empty. On the other hand, the set of its leaf addresses is $l_i^! = \{[]\}$, since the unique leaf is the root edge.

(2) Let $b \in B$ be an operation of $P$. Then $Y_b^\bullet = \{[]\}$ since the only node is that above the root edge. For leaves, we have $Y_b^! = \{[e] | e \in E(b)\}$.
### 2.1.2 The polynomial Baez-Dolan (-)$^+$ construction
We now give a brief definition of the (-)$^+$ construction, see appendix A for details.

**Remark 2.22.** [7, section 1.11] The composite of two polynomial functors is polynomial. In details, if $P$ and $P'$ are as in

$$I \leftarrow^{s} E \longrightarrow B \longrightarrow^{t} I, \quad I \leftarrow^{u} F \longrightarrow C \longrightarrow^{v} I,$$

then the composite functor $P'P: \mathcal{S}et/I \to \mathcal{S}et/K$ is also polynomial. Its underlying diagram is given by

$$I \leftarrow^{x} G \longrightarrow D \longrightarrow^{y} I,$$

where

$$D := \{(a, (b_e | e \in F(a))) | a \in C, b_e \in B, t(b_e) = u_e(a)\}, \\ G(a, (b_e | e)) := \sum_{e \in F(a)} E(b_e),$$

where $y$ maps $(a, (b_e | e)) \in D$ to $v(a) \in K$, and if $f \in E(b_e)$, then $x_f$ maps $(a, (b_e | e))$ to $s_f(b_e)$. Intuitively, $D$ is just the set of trees of uniform height 2 (a.k.a. trees with two levels), where the root node is decorated by an element $C$, while the nodes on the second level are decorated by elements of $B$:

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

here, $a \in C$, $F(a) = \{e_1, \dots, e_k\}$, and $b_{e_i} \in B$ is such that $t(b_{e_i}) = u(e_i)$. The set of inputs of such a tree is $\sum_i E(b_{e_i})$.

This construction gives $\mathcal{P}oly\&nd(I)$, the structure of a monoidal category. Together with remark 2.4 we have a fully faithful functor

$$\mathcal{P}oly\&nd(I) \longrightarrow \mathcal{Cart}(\mathcal{S}et/I),$$

the latter being the category of endofunctors of $\mathcal{S}et/I$ and cartesian natural transformations$^2$.

**Definition 2.23** (Polynomial monad, classical definition). A polynomial monad over $I$ is a monoid object in $\mathcal{P}oly\&nd(I)$. Equivalently, it is a polynomial functor endowed with the structure of a cartesian monad$^3$. Let $\mathcal{P}oly\&nd(I)$ be the category of polynomial monads over $I$ and morphisms of polynomial endofunctors over $I$ that are also monad morphisms.

**Definition 2.24** ((-)*) construction. Given a polynomial endofunctor $P$ as in equation (2.2), we define a new polynomial endofunctor $P^*$ as

$$I \leftarrow^{s} \mathrm{tr}^1 P \longrightarrow \mathrm{tr} P \longrightarrow^{t} I \qquad (2.25)$$

where $\mathrm{tr}^1 P$ is the set of $P$-trees with a marked (or distinguished) leaf, where $s$ maps a $P$-tree with a marked leaf to the decoration of that leaf, $p$ forgets the marking, and $t$ maps a $P$-tree to

<footnote>$^2$We recall that a natural transformation is *cartesian* if all its naturality squares are cartesian.</footnote>

<footnote>$^3$Recall that a *cartesian monad* is a monad $(T, \eta, \mu)$ such that $T$ preserves pullbacks, and such that the natural transformations $\eta$ and $\mu$ are cartesian.</footnote>
the decoration of its root. Remark that for $T \in \text{tr} P$ we have $p^{-1}(T) \cong T^1$, and in particular, $P^*$ is finitary.

Clearly, there is an inclusion $\eta_P : P \to P^*$, mapping $b \in B$ to $Y_b \in \text{tr} P$, and $e \in E(b)$ to $[e] \in Y_b^1$ (see remark 2.12). There is also a morphism $\mu_P : P^{**} \to P^*$ defined inductively as follows:

$$ (\mu_P)_1 : \text{tr} P^* \to \text{tr} P \\ l_i \mapsto l_i \qquad i \in I \\ Y_T \bigcirc_{\substack{[[l]] \\ [l] \in T^1}} X_{[l]} \mapsto T \bigcirc_{\substack{[l] \in T^1 \\ [l] \in T^1}} (\mu_P)_1(X_{[l]}) \qquad T \in \text{tr} P, X_{[l]} \in \text{tr} P^*. $$

Informally, it maps a tree of $P$-tree $Y$ to the $P$-trees $(\mu_P)_1(Y)$ obtained by grafting all the $P$-trees decorating the nodes of $Y$ together.

Finally, the morphisms $\eta_P$ and $\mu_P$ are natural in $P$, and give $(-)^*$ the structure of a monad on $\text{Poly}\&\text{nd}(I)$.

**Theorem 2.26.** The polynomial functor $P^*$ has a canonical structure of polynomial monad. Further, the functor $(-)^*$ is left adjoint to the forgetful functor $\text{PolyMnd}(I) \to \text{Poly}\&\text{nd}(I)$, and the adjunction is monadic.

*Proof.* The first two claims are proved in [15, proposition 1.2.8], and monadicity is proved in appendix A.1. See also [8, corollary 5.1.5] where monadicity it is proved in the more general $\infty$-setting. $\square$

**Definition 2.27** (Target and readdressing map). Let $M$ be a polynomial functor as in

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

Assume further that $M$ is a $(-)^*$-algebra, and write its structure map $M^* \to M$ as

$$ \begin{tikzcd} I \arrow[r, "\text{tr}^1 M"] & \text{tr} M \arrow[r, "\simeq"] \arrow[d, "\wp"] & \text{tr} M \arrow[r, "t"] \arrow[d, "\downarrow"] & I \arrow[d, "s"] \\ I \arrow[r, "s"] & E \arrow[r, "p"] & B \arrow[r, "t"] & I. \end{tikzcd} \qquad (2.28) $$

For $T \in \text{tr} M$, we call $\wp_T : T^1 \xrightarrow{\cong} E(tT)$ the *readdressing function* of $T$, and $tT \in B$ is called the *target* of $T$. If we think of an element $b \in B$ as the corolla $Y_b$, then the target map $t$ “contracts” a tree to a corolla, and since the middle square is a pullback, the number of leaves is preserved. The map $\wp_T$ establishes a coherent correspondence between the set $T^1$ of leaf addresses of a tree $T$ and the elements of $E(tT)$.

**Definition 2.29** (Baez-Dolan $(-)^+$ construction). Let $M$ be a polynomial monad as in equation (2.2), and define its Baez-Dolan construction $M^+$ to be

$$ B \leftarrow^{s} \text{tr}^{\bullet} M \rightarrow^{p} \text{tr} M \rightarrow^{t} B \qquad (2.30) $$

where $\text{tr}^{\bullet} M$ is the set of $M$-trees with a marked (or distinguished) node, where $s$ maps an $M$-tree with a marked node to the label of that node, $p$ forgets the marking, and $t$ is the target map of definition 2.27. If $T \in \text{tr} M$, remark that $p^{-1}T = T^{\bullet}$ is the set of node addresses of $T$, and in particular, $P^+$ is finitary. If $[p] \in T^{\bullet}$, then $s[p] := s_{[p]} T$.
Remark 2.31 (Nested addresses). Let $M$ be a polynomial monad, and $T \in \mathrm{tr} M^+$. Then the nodes of $T$ are decorated in $M$-trees, and its edges by operations of $M$. Assume that $U \in \mathrm{tr} M$ decorates some node of $T$, say $U = s_{[p]} T$ for some node address $[p] \in T^\bullet$.

(1) The input edges of that node are in bijection with $U^\bullet$. In particular, the address of those input edges are of the form $[p[q]]$, where $[q]$ ranges over $U^\bullet$. This really motivates enclosing addresses in brackets.

(2) On the other hand, the output edge of that node is decorated by $tU$ (where $t$ is defined in definition 2.27).

**Theorem 2.32.** The polynomial endofunctor $M^+$ has a canonical structure of a polynomial monad.

*Proof.* The full construction of this structure is given in appendix A.2. □

## 2.2 Opetopes

### 2.2.1 Definition

**Definition 2.33** (The $\mathfrak{3}^n$ monad). Let $\mathfrak{3}^0$ be the identity polynomial monad on Set, which has one color and one operation with one input. We write it as

$$ \{\diamond\} \leftarrow \{*\} \longrightarrow \{\blacksquare\} \longrightarrow \{\diamond\}. $$

For $n \ge 1$, let $\mathfrak{3}^n := (\mathfrak{3}^{n-1})^+$, and write it as $\mathfrak{3}^n$ as

$$ \mathbb{O}_n \leftarrow \mathfrak{s} \quad E_{n+1} \xrightarrow{p} \mathbb{O}_{n+1} \xrightarrow{t} \mathbb{O}_n, \qquad (2.34) $$

i.e. for all $n \in \mathbb{N}$, $\mathbb{O}_n$ is the set of colors of $\mathfrak{3}^n$.

**Definition 2.35** (Opetope). An $n$-dimensional opetope (or $n$-opetope for short) $\omega$ is simply an element of $\mathbb{O}_n$, and we write $\dim \omega = n$. If $n \ge 2$, then $n$-opetopes are exactly the $\mathfrak{3}^{n-2}$-trees. In this case, an opetope $\omega \in \mathbb{O}_n$ is called degenerate if its underlying tree has no nodes (and thus consists of a unique edge), so that $\omega = l_\phi$ for some $\phi \in \mathbb{O}_{n-2}$. We say that $\omega$ is an endotope it its underlying tree has exactly one node, i.e. $\omega = Y_\psi$ for some $\psi \in \mathbb{O}_{n-1}$.

Following equation (2.28), for $n \ge 2$ and $\omega \in \mathbb{O}_n$, the structure of polynomial monad $(\mathfrak{3}^{n-2})^* \to \mathfrak{3}^{n-2}$ gives a bijection $\wp_\omega : \omega^1 \to (t\omega)^\bullet$ between the leaves of $\omega$ and the nodes of $t\omega$, preserving the decoration by $(n-2)$-opetopes.

**Example 2.36.** (1) The unique 0-opetope is denoted $\diamond$ and called the point.

(2) The unique 1-opetope is denoted $\blacksquare$ and called the arrow.

(3) If $n \ge 2$, then $\omega \in \mathbb{O}_n$ is a $\mathfrak{3}^{n-2}$-tree, i.e. a tree whose nodes are labeled in $(n-1)$-opetopes, and edges are labeled in $(n-2)$-opetopes. In particular, 2-opetopes are $\mathfrak{3}^0$-trees, i.e. linear trees, and thus in bijection with $\mathbb{N}$. We will refer to them as opetopic integers, and write $n$ for the 2-opetope having exactly $n$ nodes.

(4) A 3-opetope is a $\mathfrak{3}^1$-tree, i.e. a planar tree.

(5) A 4-opetope is a $\mathfrak{3}^2$-tree. Unfolding definitions, if $\omega : \langle\omega\rangle \to \mathfrak{3}^2$, then nodes of $\omega$ are decorated by elements of $\mathbb{O}_3$, i.e. planar trees. Further, if $x \in \langle\omega\rangle_1$ is a node of $\omega$, then $\omega_2$ exhibits a bijection between the input edges of $x$ and the nodes of $\omega_1(x) \in \mathbb{O}_3$.

**Proposition 2.37.** Let $\omega \in \mathbb{O}_n$ with $n \ge 2$. We have the following.
(1) If $\omega$ is degenerate, say $\omega = I_\phi$ for some $\phi \in \mathbb{O}_{n-2}$, then $t\omega = Y_\phi$, and $\wp_\omega : \omega' = \{[]\} \to Y_\phi^\bullet = \{[]\}$ obviously maps $[]$ to $[]$.

(2) If $\omega$ is an endotope, say $\omega = Y_\psi$ for some $\psi \in \mathbb{O}_{n-1}$, then $t\omega = \psi$. Further, $\omega' = \{[[q]]| [q] \in \psi^\bullet\}$, and $\wp_\omega$ maps $[[q]]$ to $[q]$.

(3) Otherwise, $\omega$ decomposes as $\omega = \nu \circ_{[l]} Y_\psi$, for some $\nu \in \mathbb{O}_n$, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu'$, and

$$t\omega = (t\nu) \underset{\wp_\nu[l]}{\sqcap} \psi.$$

The readdressing function $\wp_\omega : \omega' \to (t\omega)^\bullet$ is given as follows. Let $[j] \in \omega'$.

(a) If $[l] \subseteq [j]$, then $[j] = [l[q]]$ for some $[q] \in \psi^\bullet$, and $\wp_\omega[l[q]] = (\wp_\nu[l]) \cdot [q]$.

(b) If $[l] \not\subseteq [j]$, then $[j] \in \nu'$. Assume $\wp_\nu[l] \subseteq \wp_\nu[j]$. Then $\wp_\nu[j] = (\wp_\nu[l]) \cdot [[q]] \cdot [a]$, for some $[q] \in (s_{\wp_\nu[l]} t\nu)^\bullet = (t\psi)^\bullet$, and let $\wp_\omega[j] = (\wp_\nu[l]) \cdot (\wp_\psi^{-1}[q]) \cdot [a]$.

(c) If $\wp_\nu[l] \not\subseteq \wp_\nu[j]$, then $\wp_\omega[j] = \wp_\nu[j]$.

*Proof.* Direct consequence of lemma A.7 and theorem A.14. □

### 2.2.2 Opetopes vs. pasting diagrams

Opetopes are closely related to the notion of pasting diagram commonly used in higher category theory to describe composition of higher cells. Informally, a pasting diagram of dimension $n$ is a tree whose nodes are decorated with $n$-cells, edges with $(n-1)$-cells, and where the output edge of a node corresponds to its target, and the input edges to the cells in its source. For instance, the figure on the left below is a graphical representation of a 2-pasting diagram, and the corresponding decorated tree is drawn on the right:

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

If we consider the $k$-cells as $k$-opetopes for all $k$, then an $n$-pasting diagram $P$ with $n \ge 1$ induces a $3^{n-1}$-tree, i.e. a $(n+1)$-opetope, say $\omega$. We say that $P$ is the *source pasting diagram* of $\omega$. The opetope $\omega$ also has a target $t\omega \in \mathbb{O}_{n-1}$, and in the sequel, graphical representations of opetopes include both the source pasting diagram and the target. For instance, if $P$ is the pasting diagram above, then $\omega$ is represented by

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

The dichotomy between pasting diagrams and opetopes can lead to ambiguities. For example,

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

represents a 2-opetope (the opetopic integer **3**), but also a 2-pasting diagram having a unique 2-cell. In this work, such ambiguities shall be resolved by the surrounding context.
### 2.2.3 Higher addresses
By definition, an opetope $\omega$ of dimension $n \ge 2$ is a $\mathfrak{3}^{n-2}$-tree, and thus the formalism of tree addresses (definition 2.8 and remark 2.31) can be applied to reference nodes of $\omega$, also called its *source faces* or simply *sources*. In this section, we iterate this formalism into the concept of *higher dimensional address*.

**Definition 2.38 (Higher address).** The set $\mathbb{A}_n$ of $n$-addresses is defined as follows. Let $\mathbb{A}_{-1} := \emptyset$, and for $n \ge 0$, let $\mathbb{A}_n$ be the set of bracket-enclosed sequences of elements of $\mathbb{A}_{n-1}$,

$$ \mathbb{A}_{n+1} = \{[p] \mid p \in \mathbb{A}_n^*\}. $$

By convention, we also write the empty 0-address $[] \in \mathbb{A}_0$ as $*$. Note that the empty address $[]$, is in $\mathbb{A}_n$ for all $n \ge 0$. However, the surrounding context will always make the notation unambiguous.

**Example 2.39.** Since the unique element of $\mathbb{A}_0$ is $*$, the set of 1-addresses is

$$ \mathbb{A}_1 = \{[**\cdots*] \mid k \in \mathbb{N}\}. $$

A 1-address $[*\cdots*]$ where $*$ occurs $k$ times will be more concisely written $[*^k]$. The following are higher addresses$^4$:

$$ [[[*]]] \in \mathbb{A}_2, \quad [[[*][**]]][[*\cdots*]] \in \mathbb{A}_3, \quad [[[*]]]] \in \mathbb{A}_4. $$

The expression $[*[*]]$ is not a valid higher address, as $*$ and $[*]$ do not have the same dimension.

For $\omega \in \mathbb{O}$ an opetope, nodes of $\omega$ can be specified uniquely using higher addresses, as we now show. Recall that $E_{n-1}$ is the set of inputs of $\mathfrak{3}^{n-2}$ (equation (2.34)). In $\mathfrak{3}^0$, we set $E_1(\bullet) = \{*\}$, so that the unique “node address”$^5$ of $\bullet$ is $* \in \mathbb{A}_0$. Let $n \ge 2$, and assume by induction that for all $1 \le k < n$ and all $k$-opetopes $\psi$, the nodes of $\psi$ are assigned $(k-1)$-addresses, i.e. that we have an injective map $\& : \psi^\bullet \to \mathbb{A}_{k-1}$. In particular, we consider the set $\psi^\bullet$ as a subset of $\mathbb{A}_{k-1}$. Recall that an opetope $\omega \in \mathbb{O}_n$ is a $\mathfrak{3}^{n-2}$-tree $\omega : \langle\omega\rangle \to \mathfrak{3}^{n-2}$ (notation 2.7). Thus, addresses of nodes in $\omega$ are (bracket-enclosed) sequences of elements of $E_{n-1}$. By definition of $\mathfrak{3}^{n-2}$ and by definition 2.29, we have

$$ E_{n-1} = \bigcup_{\psi \in \mathbb{O}_{n-1}} \psi^\bullet \subseteq \mathbb{A}_{n-2}. $$

In conclusion, node and edge addresses of $\omega$ are $(n-1)$-addresses.

**Example 2.40.** Consider the 2-opetope on the left, called 3:

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

<footnote>$^4$Ambiguity with the dimension of addresses could be lifted altogether by indicating the dimension as e.g. $[]^1 \in \mathbb{A}_1$, $[*\cdots*]^1 \in \mathbb{A}_1$, $[[*]^1][*]^1 \in \mathbb{A}_2$, $[[[*]^1]^2]^3 \in \mathbb{A}_4$. However, this makes notations significantly heavier, so we avoid using this convention.</footnote>

<footnote>$^5$Of course, $\bullet$ is not a tree, but this abuse of terminology is convenient, as it allows us to talk about higher addresses and opetopes in a more uniform manner.</footnote>
Its underlying pasting diagram consists of 3 arrows ■ grafted linearly. Since the only node address of ■ is $* \in A_0$, the underlying tree of **3** can be depicted as on the right. On the left of that tree are the decorations: nodes are decorated with ■ $\in O_1$, while edges are decorated with ♦ $\in O_0$. For each node in the tree, the set of input edges of that node is in bijective correspondence with the node addresses of the decorating opetope, written on the right of each edge. In this low dimensional example, those addresses can only be *. Finally, on the right of each node of the tree is its 1-address, which is just a sequence of 0-addresses giving “walking instructions” to get from the root to that node.

The 2-opetope **3** can then be seen as a corolla in some 3-opetope as follows:

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

As previously mentioned, the set of input edges is in bijective correspondence with the set of node addresses of **3**. Here is now an example of a 3-opetope (already studied in section 2.2.2), with its annotated underlying tree on the right (the 2-opetopes **1** and **2** are analogous to **3**):

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

Further, the leaf addresses of this opetope are [[ ]], [[*][ ]], [[*][*]], and [[**][ ]].

**Definition 2.41.** (1) If $[p_1], [p_2] \in A_n$, then their concatenation is $[p_1] \cdot [p_2] := [p_1p_2]$. In particular, $[p_1] \cdot [] = [] \cdot [p_1] = [p_1]$.

(2) Let $\leq$ be the *prefix order* on $A_n$, i.e. $[p_1] \leq [p_2]$ if and only if there exists $[p_3] \in A_n$ such that $[p_1] \cdot [p_3] = [p_2]$.

(3) Let $\leq$ be the *lexicographical order* on $A_n$. It is trivial on $A_0$, given by the *prefix order* on $A_1$, and on $A_n$, it is induced by *lexicographical order* on $A_{n-1}$.

**Example 2.42.** Consider the 3-opetope of example 2.40:

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

On nodes, we have the ordering $[] < [[*]] < [[**]]$, and on edges, $[] < [[]] < [[*]] < [[*]] < [[**]] < [[**]] < [[**][]]$.
### 2.2.4 The category of opetopes
In this subsection, we define the category $\mathcal{O}$ of opetopes. We first begin by a result whose geometrical meaning is explained later in this section.

**Lemma 2.43 (Opetopic identities).** Let $\omega \in \mathcal{O}_n$ with $n \ge 2$.

*Inner edge.* For an inner edge $[p[q]] \in \omega^\bullet$ (the fact that $\omega$ has an inner edge implies that it is non-degenerate), we have $\mathrm{ts}_{[p[q]]} \omega = \mathrm{s}_{[q]} \mathrm{s}_{[p]} \omega$.

*Globularity 1.* If $\omega$ is non-degenerate, we have $\mathrm{ts}_{[q]} \omega = \mathrm{tt}\omega$.

*Globularity 2.* If $\omega$ is non-degenerate, and $[p[q]] \in \omega^\bullet$, we have $\mathrm{s}_{[q]} \mathrm{s}_{[p]} \omega = \mathrm{s}_{\wp\omega}[p[q]] \mathrm{t}\omega$.

*Degeneracy.* If $\omega$ is degenerate, we have $\mathrm{s}_{[q]} \mathrm{t}\omega = \mathrm{tt}\omega$.

*Proof.* *Inner edge.* By definition of a $\mathfrak{3}^{n-2}$-tree.

*Globularity 1 and 2.* By theorem 2.26, the monad structure on $\mathfrak{3}^{n-2}$ amounts to a structure map $(\mathfrak{3}^{n-2})^* \to \mathfrak{3}^{n-2}$, which, taking the notations of definition 2.27, is written as

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

The claims follow from the commutativity of the right and left square respectively.

*Degeneracy.* Let $\omega = \mathbf{I}_\phi$, for $\phi \in \mathcal{O}_{n-2}$. By proposition 2.37, $\mathrm{tt}\omega = \mathrm{t}\mathbf{Y}_\phi = \phi$, and clearly, $\phi = \mathrm{s}_{[q]} \mathbf{Y}_\phi = \mathrm{s}_{[q]} \mathrm{t}\omega$. $\square$

### Definition 2.44 (The category $\mathcal{O}$ of opetopes)
The identities of lemma 2.43 allow us to define the category $\mathcal{O}$ of opetopes by generators and relations as follows.

*Objects.* We set $\mathrm{ob}\,\mathcal{O} = \sum_{n \in \mathbb{N}} \mathcal{O}_n$.

*Generating morphisms.* Let $\omega \in \mathcal{O}_n$ with $n \ge 1$. We introduce a generator $\mathrm{t} : \mathrm{t}\omega \to \omega$, called the *target embedding*. If $[p] \in \omega^\bullet$, then we introduce a generator $\mathrm{s}_{[p]} : \mathrm{s}_{[p]} \omega \to \omega$, called a *source embedding*. An *elementary face embedding* is either a source or the target embedding.

*Relations.* We impose 4 relations described by the following commutative squares, which just enforce the identities of lemma 2.43. Let $\omega \in \mathcal{O}_n$ with $n \ge 2$.

(Inner) For $[p[q]] \in \omega^\bullet$ (forcing $\omega$ to be non-degenerate), the following square must commute:

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

(Glob1) If $\omega$ is non-degenerate, the following square must commute:

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

(Glob2) If $\omega$ is non-degenerate, and for $[p[q]] \in \omega^\bullet$, the following square must com-
mute:

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

(Degen) If $\omega$ is degenerate, the following square must commute:

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

**Definition 2.45.** An opetopic set is a Set-valued presheaf over $\mathcal{O}$. We write $\tilde{\mathcal{O}}$ for the category of opetopic sets and natural transformations, $O[-] : \mathcal{O} \to \tilde{\mathcal{O}}$ for the Yoneda embedding, and $\tilde{\mathcal{O}}_{\text{fin}}$ for the full subcategory of $\tilde{\mathcal{O}}$ spanned by finite opetopic sets, i.e. those $X \in \tilde{\mathcal{O}}$ such that $\sum_{\omega \in \mathcal{O}} X_\omega$ is a finite set. Equivalently, $\tilde{\mathcal{O}}_{\text{fin}}$ is the completion of $\mathcal{O}$ under finite colimits.

*Remark 2.46.* Let us explain this definition a little more. Opetopes are trees whose nodes (and edges) are decorated by opetopes. The decoration is now interpreted as a geometrical feature, namely as an embedding of a lower dimensional opetope. Further, the target of an opetope, while not an intrinsic data, is also represented as an embedding. The relations can be understood as follows.

(Inner) The inner edge at $[p[q]] \in \omega^{\bullet}$ is decorated by the target of the decoration of the node “above” it (here $s_{[p[q]]} \omega$), and in the $[q]$-source of the node “below” it (here $s_{[p]} \omega$). By construction, those two decorations match, and this relation makes the two corresponding embeddings $s_{[q]} s_{[p]} \omega \to \omega$ match as well. On the left is an informal diagram about $\omega$ as a tree (reversed gray triangle), and on the right is an example of pasting diagram represented by an opetope, with the relevant features of the (Inner) relation colored or thickened.

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

(Glob1-2) If we consider the underlying tree of $\omega$ as its “geometrical source”, and the corolla $Y_{t\omega}$ as its “geometrical target”, then they should be parallel. The relation (Glob1) expresses this idea by “gluing” the root edges of $\omega$ and $Y_{t\omega}$ together, while (Glob2) glues the leaves according to $\wp_\omega$.

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

(Degen) If $\omega$ is a degenerate opetope, depicted as on the right, then its target should be a “loop”, i.e. its only source and its target should be glued together.

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

### 3. Named approach

#### 3.1 The system for opetopes

**3.1.1 Syntax** In this section, we define the underlying syntax of OPT¹, our named derivation system for opetopes. As explained in the introduction, a typical pasting diagram is pictured below:

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

We shall use the names of the cells of this picture as variables, and encode the pasting diagram as the following expression:

$$ \gamma(j \leftarrow \alpha, k \leftarrow \beta). $$

Here, $j, k, \alpha, \beta$, and $\gamma$ are now variables, equipped with a dimension (1 for $j$ and $k$, and 2 for $\alpha, \beta$, and $\gamma$), and the notation is meant to be read as “the variable $\gamma$ in which $\alpha$ (resp. $\beta$) has been formally grafted on the input labeled by $j$ (resp. $k$)”. Such a term will be given a type:

$$ i(t \leftarrow h(z \leftarrow g(y \leftarrow f))) \mapsto a \mapsto \emptyset, $$

which expresses the fact that the source is the “composite” $i \cdot h \cdot g \cdot f$, and that the source of the source is $a$. Since the pasting diagram is 2-dimensional, there is no further iterated source, and we conclude the sequence by a $\emptyset$ symbol. Similarly, the degenerate pasting diagram on the left below will be denoted by the typed term figured on the right:

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

where the term $\underline{x}$ denotes a degenerate 1-dimensional pasting diagram with $x$ as source.
**Definition 3.1 (Term).** We assume that we have an $\mathbb{N}$-graded set $\mathbb{V}$ of variables. Elements of $\mathbb{V}_n$ represent $n$-dimensional cells. An $n$-term is constructed according to the following grammar:

$$ 
\begin{align*}
\mathbb{T}_{-1} &::= \emptyset & \text{by convention} \\
\mathbb{T}_0 &::= \mathbb{V}_0 \\
\mathbb{T}_{n+1} &::= \underline{\mathbb{V}}_n \mid \mathbb{T}'_{n+1} \\
\mathbb{T}'_{n+1} &::= \mathbb{V}_{n+1}(\mathbb{V}_n \leftarrow \mathbb{T}'_{n+1}, \dots)
\end{align*}
$$

where the expression “$\mathbb{V}_n \leftarrow \mathbb{T}'_{n+1}, \dots$” signifies that there is 0 or more instances of the “$\mathbb{V}_n \leftarrow \mathbb{T}'_{n+1}$” part between the parentheses. Terms of the form $\underline{u}$ are called degenerate terms, or empty syntactic pasting diagrams. Note that there are no degenerate 0-terms.

**Example 3.2.** If $f, g \in \mathbb{V}_1$, and $a \in \mathbb{V}_0$, then the following is an element of $\mathbb{T}_1$:

$$ g(a \leftarrow f()) $$

To make notations lighter, we omit empty parentheses “()”, so the previous 1-term can be more concisely written as $g(a \leftarrow f)$. Since $f \in \mathbb{V}_1$, the expression $\underline{f}$ is a degenerate term in $\mathbb{T}_2$.

**Notation 3.3.** A term of the form $g(a_1 \leftarrow f_1, \dots, a_k \leftarrow f_k)$ will oftentimes be abbreviated as $g(a_i \leftarrow \underline{f_i})$, leaving $k$ implicit. By convention, the sequence $a_1 \leftarrow f_1, \dots, a_k \leftarrow f_k$ above is always considered up to permutation, i.e. for $\sigma$ a bijection of the set $\{1, \dots, k\}$, the terms $g(a_1 \leftarrow f_1, \dots, a_k \leftarrow f_k)$ and $g(a_{\sigma(1)} \leftarrow f_{\sigma(1)}, \dots, a_{\sigma(k)} \leftarrow f_{\sigma(k)})$ are considered equal.

**Notation 3.4.** For $t \in \mathbb{T}_n$, write $t^\bullet$ for the set of $n$-variables occurring in $t$. In the previous example, $(g(a \leftarrow f))^\bullet = \{f, g\}$. Note that $x \in x^\bullet$ for all $x \in \mathbb{V}_n$.

**Definition 3.5 (Type).** An $n$-type $T$ is a sequence of terms of the form

$$ s_1 \dashv s_2 \dashv \dots \dashv s_n \dashv \emptyset, \qquad (3.6) $$

where $s_i \in \mathbb{T}_{n-i}$. As we will see in proposition 3.53 (see also remark 4.18), the $\dashv$ symbols hints the existence of a bijection between the “leaves” of the term on its left and the “nodes” of the term on its right.

**Definition 3.7 (Typing).** A *typing* of a term $t \in \mathbb{T}_n$ is an expression of the form $t : T$, for $T$ an $n$-type. If $T$ is as in equation (3.6), then $s_i$ is thought of as the $i$-th (iterated) source of $t$. We then write $st := s_1$ (which tacitly depends on the type $T$), and more generally $s^i t := s_i$. By convention, $s^0 t := t$.

**Example 3.8.** The pasting diagram on top will be described by the typing below:

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

Remark that the term $s^2 A = h(c \leftarrow g(b \leftarrow f))$ is the source pasting diagram of the target of $A$, as in $ssA = stA$. Targets are not represented in this syntax, but already, we see that the information they carry is not lost (here, $\gamma$ does not appear in the syntactical description of $A$, but it source does). Refer to proposition 3.53 for a formal account of this observation.
**Definition 3.9** (Context). A context Γ is a set of typings of distinct variables, and is more commonly written as a list.

Notation 3.10. Write $V_{\Gamma,k}$ for the set of $k$-variables typed in $\Gamma$, let $V_{\Gamma} := \sum_{k \in \mathbb{N}} V_{\Gamma,k}$, write $T_{\Gamma,k}$ for the set of $k$-terms whose variables (in any dimension) are in $V_{\Gamma}$, and $T_{\Gamma} := \sum_{k \in \mathbb{N}} T_{\Gamma,k}$.

Remark 3.11. As we will see (inference rules in definition 3.23), for a derivable context $\Gamma$, if $x$ occurs in the typing of a variable of $\Gamma$, then $x \in V_{\Gamma}$. Note that in any context $\Gamma$, if a variable $x \in V_{\Gamma,k}$ occurs in the type of $y \in V_{\Gamma,l}$, then $k < l$. In particular, there is no cyclic dependency among variables.

**Definition 3.12** (Equational theory). Let $\Gamma$ be a context. An equational theory $E$ on $V_{\Gamma}$ is a set of formal equalities between variables of $\Gamma$. We write $=_{E}$ for the equivalence relation on $V_{\Gamma}$ generated by $E$ (or just $=$ if the $E$ is clearly implied).

**Definition 3.13** (Sequent). A sequent is an expression of the form

$$E \triangleright \Gamma \vdash t : T$$

where $\Gamma$ is a context, $E$ is an equational theory on $V_{\Gamma}$, and the right hand side is a typing. We may write $\vdash_n$ to signify that $t \in T_n$. The equivalence relation $=_{E}$ on $V_{\Gamma}$ extends to $T_{\Gamma}$ in an obvious way. If the equational theory $E$ is clear, and if $x =_{E} y$ with $y \in t^{\bullet}$, then by convention, we consider that $x \in t^{\bullet}$, so that $x$ and $y$ really are interchangeable.

Remark 3.14. As illustrated below, grafting degenerate terms produces identifications of lower dimensional variables, which must be accounted for. This will be the role of the equational theories.

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

This example will be treated in detail in example 3.69.

**Definition 3.15** (Equivalence of sequents). If $(E \triangleright \Gamma \vdash t : T)$ and $(F \triangleright \Upsilon \vdash u : U)$ are sequents, and if there exists a bijection $\sigma : V_{\Upsilon} \to V_{\Gamma}$ such that

$$(E \triangleright \Gamma \vdash t : T) = (F^{\sigma} \triangleright \Upsilon^{\sigma} \vdash u^{\sigma} : U^{\sigma}),$$

where $(-)^{\sigma}$ is the substitution according to $\sigma$, then we say that both sequents are $\alpha$-equivalent (or just equivalent), denoted by

$$(E \triangleright \Gamma \vdash t : T) \cong (F \triangleright \Upsilon \vdash u : U).$$

**Definition 3.16** (Leaves of a term). Let $\Gamma$ be a context and $t \in T_{\Gamma,n}$ be an $n$-term such that all variables in $t^{\bullet}$ are typed in $\Gamma$. The set $t^{\downarrow}$ of leaves of $t$ is defined as follows.

(1) If $n = 0$, then $t^{\downarrow} = \emptyset$.

(2) If $t = \underline{a}$ is degenerate, with $a \in V_{\Gamma,n-1}$, then $t^{\downarrow} = \{a\}$.
(3) If $t \in \mathbb{V}_{\Gamma,n}$ is a variable, then by assumption, it is typed in $\Gamma$, and thus has a source st. We define $t^1 := (st)^{\bullet}$.

(4) Otherwise, $t$ decomposes as $t = x(\overrightarrow{y_i \leftarrow u_i})$, where $x \in \mathbb{V}_{\Gamma,n}$, $y_i \in \mathbb{V}_{\Gamma,n-1}$, and $u_i \in \mathbb{T}_{\Gamma,n}$. We define

$$t^1 := (x^1 - \{y_1, \dots\}) \bigcup_i u_i^1.$$

Note that without any assumption, the set $\{y_1, \dots\}$ is not necessarily a subset of $x^1$, and so by $x^1 - \{y_1, \dots\}$ we of course mean $x^1 - (x^1 \cap \{y_1, \dots\})$.

**Definition 3.17** (Well-formed term). Let $\Gamma$ be a context. We define the set of *well-formed terms* inductively as follows.

(1) Degenerate terms are well-formed.

(2) Variables are well-formed terms.

(3) Consider a term $t \in \mathbb{T}_{\Gamma,n}$ of the form $x(\overrightarrow{y_i \leftarrow u_i})$, where $x \in \mathbb{V}_{\Gamma,n}$, $y_i \in \mathbb{V}_{\Gamma,n-1}$, and $u_i \in \mathbb{T}_{\Gamma,n}$. Then $t$ is well-formed if

(a) $x$ is typed in $\Gamma$, and $\{y_1, \dots\} \subset x^1$;

(b) the $u_i$'s are themselves well-formed.

Note that if $t$ is well-formed, then all variables in $t^\bullet$ are typed in $\Gamma$.

### 3.1.2 Inference rules
We present the inference rules of the OPT$^1$ system in definition 3.23. Rule graft requires the so-called graft notation and substitution operation, which we introduce now.

**Definition 3.18** (Grafting of terms). Let $\Gamma$ be a context and $E$ be an equational theory on $\mathbb{V}_{\Gamma}$. For $t \in \mathbb{T}_{\Gamma,n}$ a well-formed term, $a \in \mathbb{V}_{n-1}$, and $x \in \mathbb{V}_{\Gamma,n}$, the graft notation $t(a \leftarrow x)$ can be iteratively simplified depending on the structure of $t$, according to the following rewriting rules.

(1) If $t$ is degenerate, say $t = \underline{b}$, then

$$t(a \leftarrow x) \mapsto \begin{cases} t & \text{if } a \neq_E b, \\ x & \text{if } a =_E b. \end{cases}$$

(2) If $t$ is not degenerate, then we can write it as $t = y(\overrightarrow{z_i \leftarrow u_i})$ with $y \in \mathbb{V}_{\Gamma,n}$, $z_i \in \mathbb{V}_{\Gamma,n-1}$ and $u_i \in \mathbb{T}_{\Gamma,n}$. Then,

$$t(a \leftarrow x) \mapsto \begin{cases} y(\overrightarrow{z_i \leftarrow u_i(a \leftarrow x))} & \text{if } a \notin y^1, \\ y(\overrightarrow{z_i \leftarrow u_i}, a \leftarrow x) & \text{if } a \in y^1. \end{cases} \qquad (3.19)$$

In particular, note that if $a \notin y^1$, then $y(a \leftarrow x)$ rewrites to $y()$, and with the “empty parentheses convention”, this gives $y(a \leftarrow x) \mapsto y$.

Clearly, in both cases, the resulting term is well-formed.

**Lemma 3.20.** Let $\Gamma$ be a context and $E$ be an equational theory on $\mathbb{V}_{\Gamma}$, $t \in \mathbb{T}_{\Gamma,n}$ be a well-formed term, $a \in \mathbb{V}_{n-1}$, and $x \in \mathbb{V}_{\Gamma,n}$ be a variable typed in $\Gamma$. If $a \in t^1$, then

$$t(a \leftarrow x)^1 = (t^1 - \{a\}) \cup x^1.$$

*Proof.* We proceed by induction.

(1) Assume that $t$ is degenerate, say $t = \underline{b}$ for some $b \in \mathbb{V}_{\Gamma,n-1}$. Since $a \in t^1 = \{b\}$, we have $a = b$, and then by definition, $t(a \leftarrow x)$ rewrites to $x$. The result follows trivially.
(2) Assume that $t \in \mathbb{V}_{\Gamma,n}$ is a variable. Since $a \in t^1$, $t(a \leftarrow x)$ can only rewrite to $t(a \leftarrow x)$, i.e. the $a \leftarrow x$ expression is not discarded. The result follows by definition 3.16.

(3) Assume that $t \in \mathbb{V}_{\Gamma,n}$ is not degenerate nor a variable, and decompose it as $t = y(\overrightarrow{z_i \leftarrow u_i})$ with $y \in \mathbb{V}_{\Gamma,n}$, $z_i \in \mathbb{V}_{\Gamma,n-1}$ and $u_i \in \mathbb{T}_{\Gamma,n}$. By definition 3.18, $t(a \leftarrow x)$ rewrites to

$$y(\overrightarrow{z'_j \leftarrow u'_j}) = \begin{cases} y(\overrightarrow{z_i \leftarrow u_i}(a \leftarrow x)) & \text{if } a \notin y^1, \\ y(\overrightarrow{z_i \leftarrow u_i}, a \leftarrow x) & \text{if } a \in y^1. \end{cases}$$

However, since $a \in t^1 = (st)^\bullet$, $x \in t(a \leftarrow x)^\bullet$, or in other words, the expression $a \leftarrow x$ is not discarded. In particular, there exists at least one index $k$ such that $x \in u'_k(a \leftarrow x)^\bullet$. Let $K$ be the set of such indices. We now distinguish cases:

(a) If $a \notin y^1$, then $z'_i = z_i$ for all $i$, $u'_i = u_i$ for $i \notin K$, and $u'_k = u_k(a \leftarrow x)$ for all $k \in K$. Then,

$$\begin{align*}
t(a \leftarrow x)^1 &= y(\overrightarrow{z'_j \leftarrow u'_j})^1 \\
&= \left( (y^1 - \{z_1, \dots\}) \bigcup_{i \notin K} u'_i \right) \bigcup_{k \in K} u_k(a \leftarrow x)^1 \\
&= \left( (y^1 - \{z_1, \dots\}) \bigcup_{i \notin K} u'_i \right) \bigcup_{k \in K} (u'_k - \{a\}) \cup x^1 && \text{by induction} \\
&= \left( \left( (y^1 - \{z_1, \dots\}) \bigcup_{i \in K} u'_i \right) - \{a\} \right) \cup x^1 \\
&= (t^1 - \{a\}) \cup x^1.
\end{align*}$$

(b) If $a \in y^1$, then $t(a \leftarrow x) = y(\overrightarrow{z_i \leftarrow u_i}, a \leftarrow x)$, and

$$\begin{align*}
t(a \leftarrow x)^1 &= (x^1 - \{a, y_1, \dots\}) \cup x^1 + \bigcup_i u'_i \\
&= (t^1 - \{a\}) \cup x^1.
\end{align*}$$

□

**Definition 3.21** (Substitution in terms). Let $\Gamma$ be a context, $E$ be an equational theory on $\mathbb{V}_{\Gamma}$, $u, v \in \mathbb{T}_{\Gamma,n}$ be well-formed terms, and $a \in \mathbb{V}_{\Gamma,n-1}$ be a typed variable such that $a \in u^\bullet$. Assume that $v^1 = a^1$. The *substitution* of $a$ for $v$ in the term $u$, denoted by $u[v/a]$, is defined as follows. If $u$ is degenerate, then $u[v/a] := u$. Otherwise, $u$ decomposes as $u = y(\overrightarrow{z_i \leftarrow w_i})$ with $y \in \mathbb{V}_{\Gamma,n}$, $z_i \in \mathbb{V}_{\Gamma,n-1}$ and $w_i \in \mathbb{T}_{\Gamma,n}$.

(Subst1) If $v$ is not degenerate, then

$$u[v/a] := \begin{cases} y(\overrightarrow{z_i \leftarrow w_i[v/a]}) & \text{if } a \neq E y, \\ v(\overrightarrow{z_i \leftarrow w_i}) & \text{if } a = E y, \end{cases} \qquad (3.22)$$

and in the second case, definition 3.18 is applied to evaluate the resulting term.

(Subst2) If $v$ is degenerate, say $v = \underline{b}$ for $b \in \mathbb{V}_{\Gamma,n-1}$, then, $u[\underline{b}/a]$ is defined by cases on the form of $u$:

(Subst2a) if $u =_E a$, then $u[\underline{b}/a] := \underline{b}$;

(Subst2b) if $u$ is of the form $a(b_1 \leftarrow r_1, \dots, b_k \leftarrow r_k)$, then since $\{b_1, \dots, b_k\} \subseteq a^1 = v^1 = \underline{b}^1 = \{b\}$, we have $k = 1$ and $b_1 = b$, and we define $u[\underline{b}/a] := r_1$;
(Subst2c) if $u$ is of the form $y(..., z \leftarrow a, ...)$, then we remove the grafting $z \leftarrow a$, and we add the equality $b = z$ to the ambient equational theory as a *side effect*;

(Subst2d) if $u$ is of the form $y(..., z \leftarrow a(b_1 \leftarrow r_1, ..., b_k \leftarrow r_k), ...)$, then following the same argument as in (Subst2b), $k = 1$, $b_1 = b$, and

$$u[\underline{b}/a] := y(..., z \leftarrow r_1, ...),$$

but we also add the equality $b = z$ to the ambient equational theory as a *side effect*;

(Subst2e) otherwise, if $u$ is of the form $y(\overrightarrow{z_i \leftarrow w_i})$, and if the previous cases do not apply (i.e. $a$ is not the front variable of $u$ or $w_i$ for all $i$), then we recursively evaluate the substitution:

$$u[\underline{b}/a] := y(\overrightarrow{z_i \leftarrow w_i[\underline{b}/a]}).$$

We emphasize that cases (Subst2c) and (Subst2d) potentially incur a side effect on the ambient equational theory. In each case, it is straightforward to check that the resulting term is well-formed. Further, note that $u[v/a]^\bullet = (u^\bullet - \{a\}) \cup v^\bullet$.

**Definition 3.23** (The OPT' system). *Introduction of points.* This rule introduces 0-cells, also called points. If $x \in \mathbb{V}_0$, then

$$\overline{\triangleright x : \emptyset \vdash_0 x : \emptyset} \text{ point}$$

*Introduction of degeneracies.* This rule derives empty pasting diagrams. If $x \in \mathbb{V}_n$, then

$$\frac{E \triangleright \Gamma \vdash_n x : T}{E \triangleright \Gamma \vdash_{n+1} \underline{x} : x \mapsto T} \text{ degen}$$

*Shift to the next dimension.* This rule takes a term $t$ and introduces a new cell $x$ having $t$ as source. If $x \in \mathbb{V}_{n+1} - \mathbb{V}_\Gamma$, then

$$\frac{E \triangleright \Gamma \vdash_n t : T}{E \triangleright \Gamma, x : t \mapsto T \vdash_{n+1} x : t \mapsto T} \text{ shift}$$

*Grafting.* This rule glues an $n$-cell $x$ onto an $n$-term $t$ along a variable $a \in s_1^\bullet := (st)^\bullet$. We assume that $\Gamma$ and $\Upsilon$ are compatible, in that for all $y \in \mathbb{V}$, if $y \in \mathbb{V}_\Gamma \cap \mathbb{V}_\Upsilon$, then the typing of $y$ in both contexts match modulo the equational theory $E \cup F$. Further, the only variables typed in both $\Gamma$ and $\Upsilon$ are the variables occurring in the sources of $a$ (i.e. $s^i a$, for $1 \le i \le n-1$). If $x \in \mathbb{V}_n$, $t \in \mathbb{T}_n$ is not degenerate, $a \in (st)^\bullet$ is such that $sa = E \cup F \SS x$ $^7$, then

$$\frac{E \triangleright \Gamma \vdash_n t : s_1 \mapsto s_2 \mapsto \dots \quad F \triangleright \Upsilon \vdash_n x : U}{G \triangleright \Gamma \cup \Upsilon \vdash_n t(a \leftarrow x) : s_1[\underline{sx/a}] \mapsto s_2 \mapsto \dots} \text{ graft}$$

where the grafting $t(a \leftarrow x)$ is simplified as in definition 3.18, $s_1[\underline{sx/a}]$ is defined in definition 3.21, and where $G$ is the union of $E$ and $F$, and potentially a set of additional equalities incurred by the evaluation of $s_1[\underline{sx/a}]$. We also write **graft-a** to make explicit that we grafted onto $a$.
**Remarks 3.24.** (1) Note that for each rule, the conclusion is still a sequent, in that variables in the context are only typed once. Further, it is easy to see that derivable sequents necessarily type well-formed terms. In particular, all terms occurring on either side of the turnstile $\vdash$ must be well-formed.

(2) In the **graft rule**, by minimality of the intersection of $\Gamma$ and $\Upsilon$, we can conclude that $t^1 = s_1^\bullet$ and $x^1 = (sx)^\bullet$ are disjoint. We can then improve lemma 3.20:

$$t(a \leftarrow x)^1 = s_1[\mathfrak{sx}/a]^\bullet = s_1^\bullet - \{a\} + (sx)^\bullet = t^1 - \{a\} + x^1 \quad (3.25)$$

(3) From the formulation of system OPT$^1$, it is clear that a sequent that is equivalent to a derivable one is itself derivable. Let us now turn our attention to rule **shift** above. It takes a term $t$, thought of as a pasting diagram, and creates a new variable having $t$ as source. One may thus think of it as a rule creating “fillers”, akin to Kan filler condition on simplicial sets.

**Lemma 3.26.** Let $n \ge 1$. For $(E \triangleright \Gamma \vdash_n t : s_1 \to \dots)$ a derivable sequent, we have $t^1 = s_1^\bullet$.

*Proof.* (1) It $t$ is degenerate, say $t = \underline{x}$ for $x \in V_{\Gamma,n-1}$, then the last rule in the proof tree of $(E \triangleright \Gamma \vdash_n t : s_1 \to \dots)$ was an instance of the **degen** rule, and

$$ \begin{align*} t^1 &= \underline{x}^1 \\ &= \{x\} & \text{by definition 3.16} \\ &= x^\bullet. \end{align*} $$

(2) If $t$ is variable, then since $n \ge 1$, the last step in the proof tree was an instance of the **shift** rule, and the result is tautological.

(3) Otherwise, the last step in the proof tree was an instance of the **graft** rule. For convenience, let us change notations: consider the following instance

$$ \frac{E \triangleright \Gamma \vdash_n t : s_1 \to \dots \quad F \triangleright \Upsilon \vdash_n x : u_1 \to \dots}{G \triangleright \Gamma \cup \Upsilon \vdash_n t(a \leftarrow x) : s_1[u_1/a] \to \dots} \text{ graft} $$

and assume that the result holds for the premise sequents, i.e. that $t^1 = s_1^\bullet$ and $x^1 = u_1^\bullet$ (which again, is a tautology, since $x$ is a variable). We show that $t(a \leftarrow x)^1 = s_1[u_1/a]^\bullet$:

$$ \begin{align*} t(a \leftarrow x)^1 &= t^1 - \{a\} + x^1 && \text{by (3.25)} \\ &= s_1^\bullet - \{a\} + u_1^\bullet && \text{by inductive assumption} \\ &= s_1[u_1/a]^\bullet && \text{by definition 3.21.} \end{align*} $$

□

**Example 3.27.** Consider the term $t = \alpha(g \leftarrow \beta)$ in a suitable context $\Gamma$:

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

<footnote>$^6$This ensures that $a$ has not been used for grafting beforehand.</footnote>

<footnote>$^7$Recall that by example 3.8, we can understand this condition as $sa = stx$, so that the variable $x$ may indeed be glued onto $a$.</footnote>
and two variables $\gamma : j \mapsto x \mapsto \emptyset$ and $\gamma' : j' \mapsto z \mapsto \emptyset$. We evaluate the following simple graftings:

$$ 
\begin{aligned}
t(f \leftarrow \gamma) &= \alpha(g \leftarrow \beta)(f \leftarrow \gamma) & \text{well-def. since } ss\gamma = x = s\bar{f} \\
&= \alpha(f \leftarrow \gamma, g \leftarrow \beta) & \text{since } f \in (s\alpha)^{\bullet}
\end{aligned}
 $$

$$ 
\begin{aligned}
t(i \leftarrow \gamma') &= \alpha(g \leftarrow \beta)(i \leftarrow \gamma') & \text{well-def. since } ss\gamma' = z = s\bar{i} \\
&= \alpha(g \leftarrow \beta(i \leftarrow \gamma')) & \text{since } i \notin (s\alpha)^{\bullet}
\end{aligned}
 $$

$$ 
\begin{aligned}
t(f \leftarrow \gamma)(i \leftarrow \gamma') &= \alpha(f \leftarrow \gamma, g \leftarrow \beta)(i \leftarrow \gamma') & \text{as seen previously} \\
&= \alpha(f \leftarrow \gamma(i \leftarrow \gamma'), g \leftarrow \beta(i \leftarrow \gamma')) & \text{since } i \notin (s\alpha)^{\bullet} \\
&= \alpha(f \leftarrow \gamma, g \leftarrow \beta(i \leftarrow \gamma')) & \text{since } i \notin (s\gamma)^{\bullet}.
\end{aligned}
 $$

They can respectively be represented as:

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

**Example 3.28.** Consider variables $\alpha : g(y \leftarrow f) \mapsto x \mapsto \emptyset$, $\delta_x : \underline{x} \mapsto x \mapsto \emptyset$, and $\delta_y : \underline{y} \mapsto y \mapsto \emptyset$. Then $\alpha$, $\alpha(f \leftarrow \delta_x)$, and $\alpha(g \leftarrow \delta_y)$ can respectively be represented as:

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

Then the sources $\alpha(f \leftarrow \delta_x)$ and $\alpha(g \leftarrow \delta_y)$ are respectively

$$ g(y \leftarrow f)[\underline{x}/f] = g \qquad \text{by (Subst2c),} $$

$$ g(y \leftarrow f)[\underline{y}/g] = f \qquad \text{by (Subst2b),} $$

and in the first case, the equation $x = y$ is added to the ambient equational theory.

**Remark 3.29.** The **degen** rule may be replaced by the following **degen-shift** rule without changing the set of derivable sequents of the form $(E \triangleright \Gamma \vdash y : T)$ with $y \in \mathbb{V}$: if $x \in \mathbb{V}_n$ and $d \in \mathbb{V}_{n+2}$ such that $d \notin \mathbb{V}_{\Gamma,n+2}$, then

$$ \frac{E \triangleright \Gamma \vdash_n x : T}{E \triangleright \Gamma, d : \underline{x} \mapsto x \mapsto T \vdash_{n+2} d : \underline{x} \mapsto x \mapsto T} \text{ degen-shift} $$

However, note that sequents of the form $(E \triangleright \Gamma \vdash \underline{y} : T)$ are then no longer derivable.

**3.1.3 Properties of derivable sequents** Let $(E \triangleright \Gamma \vdash x : X)$ be a derivable sequent. We prove in theorem 3.31 that the type $X = (sx \mapsto ssx \mapsto \dots)$ is completely determined by $sx$ and $\Gamma$.

**Definition 3.30.** We extend the source map $s : \mathbb{V}_{\Gamma,n} \to \mathbb{T}_{\Gamma,n-1}$ to a map $\bar{s} : \mathbb{T}_{\Gamma,n} \to \mathbb{T}_{\Gamma,n-1}$ as follows:

$$ 
\begin{array}{rcl@{\qquad}rcl}
\bar{s} : \mathbb{T}_{\Gamma,n} & \to & \mathbb{T}_{\Gamma,n-1} & & \\
x & \mapsto & s\bar{x} & & x \in \mathbb{V}_{\Gamma}, \\
\underline{x} & \mapsto & x & & x \in \mathbb{V}_{\Gamma}, \\
x(\overrightarrow{y_i \leftarrow u_i}) & \mapsto & (s\bar{x})[\overrightarrow{\bar{s}u_i/y_i}] & & x, \overrightarrow{y_i} \in \mathbb{V}_{\Gamma}, \overrightarrow{u_i} \in \mathbb{T}_{\Gamma}.
\end{array}
 $$

Note that by definition, it agrees with $s$ on variables.
**Theorem 3.31.** Let $(E \triangleright \Gamma \vdash t : s_1 \dashv s_2 \dashv \dots \dashv s_n \dashv \emptyset)$ be a derivable sequent. Then for $1 \le k \le n$ we have $s_k = \bar{s}^k t$. Equivalently, for $0 \le i \le n$, we have $\bar{s} s_i = s_{i+1}$, where by convention, $s_0 := t$.

*Proof.* We proceed by induction on the proof tree of the sequent. For readability, we omit equational theories and contexts.

(1) If the sequent is obtained by the following proof tree:

$$ \overline{x : \emptyset \vdash x : \emptyset} \text{ point} $$

then $\bar{s}x = sx = \emptyset$, since $x \in \mathbb{V}$, and the result trivially holds.

(2) If the last inference of the proof tree is the following instance of **degen**

$$ \frac{\dots \vdash s_1 : s_2 \dashv \dots \dashv s_n \dashv \emptyset}{\dots \vdash t : s_1 \dashv s_2 \dashv \dots \dashv s_n \dashv \emptyset} \text{ degen} $$

then $s_1 \in \mathbb{V}$ and $t = s_1$. Thus, $\bar{s}t = s_1$, while for $1 \le i \le n$, the equality $\bar{s}s_i = s_{i+1}$ holds by induction.

(3) If the last inference of the proof tree is the following instance of **shift**

$$ \frac{\dots \vdash s_1 : s_2 \dashv \dots \dashv s_n \dashv \emptyset}{\dots \vdash t : s_1 \dashv s_2 \dashv \dots \dashv s_n \dashv \emptyset} \text{ shift} $$

then $t \in \mathbb{V}$, so $\bar{s}t = st = s_1$, while for $1 \le i \le n$, the equality $\bar{s}s_i = s_{i+1}$ holds by induction.

(4) Assume now that the last inference of the proof tree is the following instance of **graft**:

$$ \frac{\dots \vdash u : r_1 \dashv r_2 \dashv s_3 \dashv \dots \dashv s_n \dashv \emptyset \quad \dots \vdash x : X}{\dots \vdash t : s_1 \dashv s_2 \dashv \dots \dashv s_n \dashv \emptyset} \text{ graft-a} $$

with $a \in r_1^\bullet$ and $x \in \mathbb{V}$ such that $sx = sa$. Then $t = u(a \leftarrow x)$, $s_1 = r_1[\mathfrak{s}x/a]$, and $s_i = r_i$ for $2 \le i \le n$. On the one hand, we have

$$ \begin{align*} \bar{s}t &= \bar{s}(u(a \leftarrow x)) \\ &= (\bar{s}u)[\bar{s}x/a] \\ &= (\bar{s}u)[\mathfrak{s}x/a] && \text{since } x \in \mathbb{V} \\ &= r_1[\mathfrak{s}x/a] && \text{by induction} \\ &= s_1 && \text{by definition.} \end{align*} $$

On the other hand, write $r_1 = v(y \leftarrow a(\overrightarrow{z_i \leftarrow \overrightarrow{w_i}}))$, for some $v, \overrightarrow{w_i} \in \mathbb{T}_{n-1}$ and $y \in \mathbb{V}_{n-2}$. This decomposition exhibits $r_1$ as a grafting (in the sense of definition 3.18) of a term $a(\cdots)$ whose head variable is $a$ onto some term $v$. We then compute:

$$ \begin{align*} \bar{s}s_1 &= \bar{s}(r_1[\mathfrak{s}x/a]) \\ &= \bar{s} \left( v(y \leftarrow a(\overrightarrow{z_i \leftarrow \overrightarrow{w_i}})) \quad [\mathfrak{s}x/a] \right) \\ &= \bar{s} \left( v(y \leftarrow (\mathfrak{s}x)(\overrightarrow{z_i \leftarrow \overrightarrow{w_i}})) \quad \right) \\ &= (\bar{s}v) \left[ (\bar{s}\mathfrak{s}x)[\overline{\bar{s}w_i/z_i}] / y \right] && \text{by definition of } \bar{s} \\ &= (\bar{s}v) \left[ (\mathfrak{s}\mathfrak{s}x)[\overline{\bar{s}w_i/z_i}] / y \right] && \text{by induction} \\ &= (\bar{s}v) \left[ (\mathfrak{s}a)[\overline{\bar{s}w_i/z_i}] / y \right] && \text{hypothesis of } \textbf{graft-a} \\ &= \bar{s}r_1 && \text{recall } r_1 = v(y \leftarrow a(\overrightarrow{z_i \leftarrow \overrightarrow{w_i}})) \\ &= r_2 = s_2. \end{align*} $$

Finally, for $1 \le i \le n$, the equality $\bar{s}s_i = s_{i+1}$ holds by induction. $\square$

<figure><img src="image_41.png" /></figure>
**Corollary 3.32.** Let $(E \triangleright \Gamma \vdash t : T)$ be a derivable sequent, and $x : s_1 \mapsto s_2 \mapsto \dots \mapsto s_n \mapsto \emptyset$ be a typing in $\Gamma$. Then for $1 \le k \le n$ we have $s_k = \bar{s}^k t$, or equivalently, for $0 \le i \le n$, we have $\bar{s}_{s_i} = s_{i+1}$, with $s_0 := x$.

*Proof.* If $x : s_1 \mapsto s_2 \mapsto \dots \mapsto s_n \mapsto \emptyset$ is a typing in $\Gamma$, then somewhere in the proof tree of $(E \triangleright \Gamma \vdash t : T)$ appears a sequent of the form $(F \triangleright \Upsilon \vdash x : s_1 \mapsto s_2 \mapsto \dots \mapsto s_n \mapsto \emptyset)$, which is necessarily derivable. We conclude by applying theorem 3.31 □

**Remark 3.33.** A consequence of theorem 3.31 and corollary 3.32 is that at any stage, a context $\Gamma$ may be replaced by its “meager form” $\bar{\Gamma}$, obtained by replacing “full typings” $y : Y$ by $y : sy$, i.e. by removing all but the top term of the type $Y$. Using meager context comes with a cost however: checking the hypothesis of rule *graft* requires to compute the second source $sx$ of $x$, which is not contained in $\bar{\Gamma}$. For clarity, we shall not make use of meager forms throughout the rest of this work.

**Convention 3.34.** By definition, $\bar{s}$ extends $s$ to a function $T_\Gamma \to T_\Gamma$, and for convenience, we just write it as $s$ in the sequel, and call it the *source* of a term.

**Example 3.35.** Consider the term on the right, representing the pasting diagram on the left:

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

Then its source is computed as follows:

$$
\begin{align*}
s(\alpha(f \leftarrow \gamma, g \leftarrow \beta)) &= (s\alpha)[(s\gamma)/f, (s\beta)/g] & \text{by definition} \\
&= (g(y \leftarrow f))[ (s\gamma)/f, (s\beta)/g] & \text{since } s\alpha = g(y \leftarrow f) \\
&= (g(y \leftarrow f))[j/f, (s\beta)/g] & \text{since } s\gamma = j \\
&= (g(y \leftarrow f))[j/f, i(z \leftarrow h)/g] & \text{since } s\beta = i(z \leftarrow h) \\
&= (g(y \leftarrow j))[i(z \leftarrow h)/g] & \text{see equation (3.22)} \\
&= (i(z \leftarrow h))(y \leftarrow j) & \text{see equation (3.22)} \\
&= i(z \leftarrow h(y \leftarrow j)) & \text{since } y \in (sh)^{\bullet}.
\end{align*}
$$

The latter term indeed corresponds to the source of the pasting diagram, which is the arrow composition on the top.

**Lemma 3.36 (Unique occurence lemma).** Let $(E \triangleright \Gamma \vdash_n t : s_1 \mapsto \dots)$ be a derivable sequent, where $t \in T_n$ is not degenerate, say $t = x(\overrightarrow{a_i \leftarrow u_i})$.

(1) Let $y \in t^{\bullet}$. Then either $y =_E x$, or $y \in u_i^{\bullet}$ for a unique $i$.

(2) Let $b \in t^1$. Then either $b \in x^1 - \{a_1, \dots\}$, or $b \in u_i^1$ for a unique $i$.

*Proof.* (1) By assumption of the *graft* rule, each $n$-variable of $t$ occurs only once in $t$.

(2) By the first point, each $(n-1)$-variable of $s_1$ occurs exactly once. By theorem 3.31, $s_1 = (sx)[\overrightarrow{\bar{s}u_i/a_i}]$. Thus $b$ either occurs in $sx$ or on $su_i$ for a unique $i$. □

**Proposition 3.37.** Let $(E \triangleright \Gamma \vdash t : T)$ be a derivable sequent, where $t \in T_\Gamma$.

(1) Let $a \in V_\Gamma$ be a variable of type $A$. Then the sequent $(E|_a \triangleright \Gamma|_a \vdash a : A)$ is derivable, where $E|_a$ (resp. $\Gamma|_a$) is the restriction of $E$ (resp. $\Gamma$) to $a$ and variables occurring in $A$.
(2) If $u$ is a subterm of $t$, then the restricted sequent $(E|_u \triangleright \Gamma|_u \vdash u : U)$ is derivable, where $U = su \mapsto s^2u \mapsto \dots$, and where $E|_u$ (resp. $\Gamma|_u$) is the restriction of $E$ (resp. $\Gamma$) to variables occurring in $u$ and $U$.

*Proof.* (1) (a) If $a$ is 0-dimensional, then $(E|_a \triangleright \Gamma|_a \vdash a : A) = (\triangleright a : \emptyset \vdash a : \emptyset)$ can be obtained by an instance of rule **point**.

(b) If $a = x$, then $(E|_a \triangleright \Gamma|_a \vdash a : A) = (E \triangleright \Gamma \vdash x : X)$ is derivable by assumption.

(c) Otherwise, $a$ first appears in the conclusion of an instance of **shift** in the proof tree of $(E \triangleright \Gamma \vdash x : X)$. Then $(E|_a \triangleright \Gamma|_a \vdash a : A)$ is the conclusion of that instance, and is derivable.

(2) (a) If $u = t$, then the claim trivially holds.

(b) If $t = x(\overline{y_i \leftarrow v_i})$, $1 \le i \le k$ and $u = v_j$ for some $j$, then on the bottom of the proof tree of $(E \triangleright \Gamma \vdash t : T)$ is a sequence of $k$ instances of the **graft rule**, and $(E|_u \triangleright \Gamma|_u \vdash u : U)$ was the right premise of one of them.

(c) If $t = x(\overline{y_i \leftarrow v_i})$, and $u$ is a subterm of $v_j$ for some $j$, then by the previous point, $(E|_{v_j} \triangleright \Gamma|_{v_j} \vdash v_j : V_j)$ is derivable, and inductively, $((E|_{v_j})_u \triangleright (\Gamma|_{v_j})_u \vdash U : U) = (E|_u \triangleright \Gamma|_u \vdash u : U)$ is derivable. $\square$

**3.2 Equivalence with polynomial opetopes** In this section, all sequents are assumed derivable in $\text{OPT}^1$. We show that sequents typing a variable (up to $\alpha$-equivalence) are in bijective correspondence with the “polynomial” opetopes of definition 2.35. To this end, we define the polynomial coding operation $[\text{--}]_{n+1}$ that maps a sequent $(E \triangleright \Gamma \vdash_n t : T)$ typing an $n$-term $t \in \mathbb{T}_n$, to an $(n+1)$-opetope $[E \triangleright \Gamma \vdash_n t : T]_{n+1} \in \mathbb{O}_{n+1}$, written $[[t : T]]_{n+1}$ or even $[[t]]_{n+1}$ for short, if no ambiguity arises.

The idea of the polynomial coding is to map a pasting diagram described by a term (on the left) to its underlying composition tree, and reapply the coding recursively (on the right):

$$[[\alpha(g \leftarrow \beta)]] = \left[ \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] 
    % Vertices
    \node[circle, fill, inner sep=1.5pt] (y_i) at (0,0) {};
    \node[circle, fill, inner sep=1.5pt] (alpha) at (1,0) {};
    \node[circle, fill, inner sep=1.5pt] (g) at (0.5,0.5) {};
    \node[circle, fill, inner sep=1.5pt] (v_i) at (0.5,-0.5) {};
    \draw[->] (y_i) -- (alpha) node[left] {$\beta$};
    \draw[->] (y_i) -- (g) node[right] {$g$};
    \draw[->] (alpha) -- (v_i) node[right] {$v_i$};
    \end{tikzpicture} \\ \\
    \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] 
    % Vertices
    \node[circle, fill, inner sep=1.5pt] (y_i) at (0,0) {};
    \node[circle, fill, inner sep=1.5pt] (alpha) at (1,0) {};
    \node[circle, fill, inner sep=1.5pt] (f) at (0.5,0.5) {};
    \node[circle, fill, inner sep=1.5pt] (g) at (0.5,-0.5) {};
    \draw[->] (y_i) -- (alpha) node[left] {$\alpha$};
    \draw[->] (y_i) -- (f) node[right] {$g$};
    \draw[->] (alpha) -- (g) node[right] {$\beta$};
    \end{tikzpicture} \\ \\
    \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] 
    % Vertices
    \node[circle, fill, inner sep=1.5pt] (f) at (0,0) {};
    \node[circle, fill, inner sep=1.5pt] (g) at (0.5,0.5) {};
    \node[circle, fill, inner sep=1.5pt] (v_i) at (0.5,-0.5) {};
    \draw[->] (f) -- (g) node[right] {$\alpha$};
    \draw[->] (v_i) -- (g) node[right] {$\beta$};
    \end{tikzpicture} \\ \\
    \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] 
    % Vertices
    \node[circle, fill, inner sep=1.5pt] (f) at (0,0) {};
    \node[circle, fill, inner sep=1.5pt] (g) at (0.5,0.5) {};
    \node[circle, fill, inner sep=1.5pt] (v_i) at (0.5,-0.5) {};
    \draw[->] (f) -- (g) node[right] {$\alpha$};
    \draw[->] (v_i) -- (g) node[right] {$\beta$};
    \end{tikzpicture} 
\end{array} \right] :=$$

For $t \in \mathbb{T}_n$ and $z \in t^\bullet$, the address $\&_t z \in \mathbb{A}_n$ of $z$ in $t$ is an $n$-address (see section 2.2.3) that, much like in trees (definition 2.8), indicates “where $z$ is located in $t$”:

**Definition 3.38 (Address in a term).** Let $(E \triangleright \Gamma \vdash \dots)$ be a derivable sequent, $t \in \mathbb{T}_\Gamma$ be a non-degenerate typed term, say $t = x(\overline{y_i \leftarrow u_i})$. From proposition 3.37, we can extract a typing for each of the $u_i$s from the proof tree of $(E \triangleright \Gamma \vdash \dots)$. Assume further that for all subterms $z(a_j \leftarrow v_j)$ that occur in $t$, we have $a_j \in (\mathfrak{s}z)^\bullet$, for all $j$.

(1) Let $z \in t^\bullet$. By lemma 3.36, either $z =_E x$, or $z \in u_i^\bullet$ for a unique $i$. The address $\&_t z \in \mathbb{A}_n$ of $z$ in $t$ is defined as

$$\&_t z := \begin{cases} [] & \text{if } z =_E x, \\ [\&_{sx} y_i] \cdot \&_{u_i} z & \text{if } z \in u_i^\bullet. \end{cases}$$

If $[p] = \&_t z$, then we write $v_{[p]} t := z$ for the variable of $t$ at address $[p]$. In particular, $v_{[\,]} t = x$.
(2) Let $a \in t^1$. By lemma 3.36, either $a \in x^1 - \{y_1, \dots\}$, or $a \in u_i^1$ for a unique $i$. The address $\&_t a \in A_n$ of $a$ in $t$ is defined as

$$ \&_t a := \begin{cases} [\&_{sx} a] & \text{if } a \in x^1, \\ [\&_{sx} y_i] \cdot \&_{u_i} a & \text{if } a \in u_i^1. \end{cases} $$

Of course, those addresses tacitly depend on the surrounding sequent.

**Example 3.39.** The context describing the pasting diagram:

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

contains the following typings: $x, y, z : \emptyset$, $f : x \mapsto \emptyset$, $g : y \mapsto \emptyset$, $h : y \mapsto \emptyset$, $i : z \mapsto \emptyset$, $\alpha : g(y \leftarrow f) \mapsto a \mapsto \emptyset$, and $\beta : i(z \leftarrow h) \mapsto b \mapsto \emptyset$. Write $t := \alpha(g \leftarrow \beta)$. Then,

$$ \&_t \alpha = [] $$

$$ \&_t \beta = [\&_{s\alpha} g] \cdot \&_{\beta} \beta = [[]] \cdot [] = [[]], $$

$$ \&_t i = [\&_{s\alpha} g] \cdot \&_{\beta} i = [[]] \cdot [\&_{s\beta} i] = [[]] \cdot [[]] = [[][]], $$

$$ \&_t h = [\&_{s\alpha} g] \cdot \&_{\beta} h = [[]] \cdot [\&_{s\beta} h] = [[]] \cdot [[\&_{si} z] \cdot \&_h h] = [[][][]] = [[][*]], $$

$$ \&_t f = [\&_{s\alpha} f] = [[\&_{sg} y] \cdot \&_f f] = [[*]]. $$

Those addresses indeed match with those of the (intuitively) corresponding opetope:

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

We now present the polynomial coding operation $[-]$, mapping the derivable sequents of system OPT¹ to opetopes. In theorem 3.64, we prove that it is a bijection. Unsurprisingly, $[-]$ needs to be defined by induction on the dimension of the term being typed by the sequent. However, as we shall see, a secondary induction is also needed, this time on the number of variables in the term. In the sequel, between definition 3.40 and theorem 3.64 (included), every definition and result is stated assuming that theorem 3.64 holds by induction.

**Definition 3.40 (Polynomial coding for variables).** The polynomial coding operation $[-]_n$ is defined on derivable sequents typing $n$-variables as follows:

$$ [E \triangleright \Gamma \vdash_0 x : \emptyset]_0 := \diamond, \qquad (3.41) $$

$$ [E \triangleright \Gamma \vdash_1 x : a \mapsto \emptyset]_1 := \blacksquare, \qquad (3.42) $$

$$ [E \triangleright \Gamma, x : t \mapsto T \vdash_n x : t \mapsto T]_n := [E \triangleright \Gamma \vdash_{n-1} t : T]_n, \qquad (3.43) $$

where in the case (3.43), the value of $[t]_{n-1}$ is given in definition 3.44.
**Definition 3.44** (Polynomial coding). The polynomial coding operation $[[\cdot]]_{n+1}$ is defined on derivable sequents typing an $n$-term inductively as follows:

$$ [[E \triangleright \Gamma \vdash_{n+1} \underline{x} : x \to \dots]]_{n+2} := I_{[[x]]_n}, \qquad (3.45) $$

$$ [[E \triangleright \Gamma \vdash_n x (\overrightarrow{y_i \leftarrow u_i}) : \dots]]_{n+1} := Y_{[[x]]_n} \bigcirc_{[\&_{s,x} y_i]} [[u_i]]_{n+1}. \qquad (3.46) $$

By proposition 3.37, in equation (3.46), we can extract a typing for each of the $u_i$s from the proof tree of $(E \triangleright \Gamma \vdash_n x (\overrightarrow{y_i \leftarrow u_i}) : \dots)$. Further, if $x \in \mathbb{V}_n$ is seen as an $n$-term, then $[[x]]_{n+1} = Y_{[[x]]_n}$. If $(E \triangleright \Gamma \vdash \dots)$ is a derivable sequent, and $a \in \mathbb{V}_\Gamma$, then the restricted sequent $(E|_a \triangleright \Gamma|_a \vdash a : A)$ is also derivable by proposition 3.37, and we may construct an opetope $[[a]] = [[E|_a \triangleright \Gamma|_a \vdash a : A]$.

Note that definitions 3.40 and 3.44 are mutually dependent. The coding function $[[\cdot]]_n$ can be considered in two ways: first as mapping derivable sequents typing $n$-variables to $n$-opetopes, for any $n$ (definition 3.40), or as mapping derivable sequents typing an $(n-1)$-term to an $n$-opetope, for $n \ge 2$ (definition 3.44). The former is more faithful to the geometrical intuition that an $n$-opetope is first and foremost an $n$-dimensional shape, in this case encoded by an $n$-variable (see also example 3.8). However it is the latter version that we need to study in details. For example, it is clear that the coding function is well-defined in cases (3.41), (3.42), and (3.45), and if $n=1$, then case (3.46) is well-defined too, as there is a unique 1-opetope. But in order to establish that case (3.46) is always well-defined, we need to inductively rely on properties of $[[\cdot]]$ proved in the sequel.

**Lemma 3.47.** Let $(E \triangleright \Gamma \vdash_n t : T)$ be a sequent such that $[[t]]_{n+1}$ is well-defined. Then $[[t]]_{n+1}^\bullet = \{\&_t x \mid x \in t^\bullet\}$, i.e. the node addresses of the opetope $[[t]]_{n+1}$ are exactly the addresses of the $n$-variables of $t$.

*Proof.* If $n=0$, or if $t$ is degenerate, then the result trivially holds. If $t = x(\overrightarrow{y_i \leftarrow u_i})$ as in equation (3.46), we have

$$ \begin{aligned} [[t]]_{n+1}^\bullet &= [x(\overrightarrow{y_i \leftarrow u_i})]_{n+1}^\bullet \\ &= \left( Y_{[[x]]_n} \bigcirc_{[\&_{s,x} y_i]} [[u_i]]_{n+1} \right)^\bullet \qquad \text{by equation (3.46)} \\ &= \{[]\} \bigcup_i \{[\&_{s,x} y_i] \cdot [p] \mid [p] \in ([[u_i]]_{n+1})^\bullet\} \\ &= \{[]\} \bigcup_i \{[\&_{s,x} y_i] \cdot \&_t x \mid x \in u_i^\bullet\} \qquad \text{by induction} \\ &= \{\&_t x \mid x \in t^\bullet\} \qquad \text{see definition 3.38.} \end{aligned} $$

□

**Proposition 3.48.** Let $(E \triangleright \Gamma \vdash_n t : T)$ be a derivable sequent where $t$ is not degenerate, say $t = x(\overrightarrow{y_i \leftarrow u_i})$. Assume that $[[t]]_{n+1}$ is well-defined. For $[p] \in [[t]]_{n+1}^\bullet$ and $z := v_{[p]} t$ we have $s_{[p]} [[t]]_{n+1} = [[z]]_n$.

*Proof.* If $n=0$, then $t$ is necessarily a 0-variable, so the only possible address in $t$ is $[]$. Then, $s_{[p]} [[t]]_1 = s_{[p]} \bullet = \diamond = [[t]]_0 = [[v_{[p]} t]]_0$. Assume that $n \ge 1$. By definition,

$$ [[t]]_{n+1} = Y_{[[x]]_n} \bigcirc_{[\&_{s,x} y_i]} [[u_i]]_{n+1}, $$
and we distinguish two cases. If $z = x$, then $[p] = []$, and the result clearly holds. Otherwise, $[p] = [\&_{sx} y_j] \cdot \&_{u_j} z$, where $j$ is the unique index such that $z \in u_j^\bullet$ (see lemma 3.36). Then,

$$
\begin{align*}
\mathfrak{s}[p][t]_{n+1} &= \mathfrak{s}[\&_{sx} y_j] \cdot \&_{u_i} z \left( \mathbb{Y}_{[x]_n} \bigcirc_{[\&_{sx} y_i]} [[u_i]]_{n+1} \right) \\
&= \mathfrak{s} \&_{u_j} z [[u_j]]_{n+1} \\
&= [z]_n \qquad \text{by induction.}
\end{align*}
$$

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

**Corollary 3.49.** Let $x$ and $y_i$ be as in equation (3.46), and assume that $[[x]]_n$ and $[[y_i]]_{n-1}$ are both well-defined. Then for $[p_i] := \&_{sx} y_i$ we have $\mathfrak{s}_{[p_i]}[[x]]_n = [[y_i]]_{n-1}$.

*Proof.* We simply have

$$
\begin{align*}
\mathfrak{s}_{[p_i]}[[x]]_n &= \mathfrak{s}_{[p_i]}[[sx]]_n && \text{see equation (3.43)} \\
&= [[y_i]]_{n-1} && \text{by proposition 3.48.}
\end{align*}
$$

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

**Lemma 3.50.** Let $n \ge 1$, and consider the following instance of the graft rule:

$$
\frac{\cdots \vdash_n t : T \quad \cdots \vdash_n x : X}{\cdots \vdash_n t(a \leftarrow x) : R} \text{ graft-a}
$$

where $(\cdots \vdash_n t : T)$ and $(\cdots \vdash_n x : X)$ are derivable. Writing $r := t(a \leftarrow x)$, and assuming that $[[r]]_{n+1}$ is well-defined, we have $[[r]]_{n+1} = [[t]]_{n+1} \circled{\&} t a \mathbb{Y}_{[x]_n}$.

*Proof.* By equation (3.46), $[[r]]_{n+1} = [[t]]_{n+1} \circ [l] \mathbb{Y}_{[x]_n}$, for some leaf address $[l]$. By assumption of the graft rule, $t$ is non-degenerate, and write it as $t = z(\overline{y_i \leftarrow u_i})$. According to definition 3.18,

$$
r = z(\overline{y_i \leftarrow u_i})(a \leftarrow x) = \begin{cases} z(\overline{y_i \leftarrow u_i}, a \leftarrow x) & \text{if } a \in (sz)^\bullet, \\ z(\overline{y_i \leftarrow u_i}(a \leftarrow x)) & \text{if } a \notin (sz)^\bullet, \end{cases}
$$

so there are two cases.

(1) If $a \in (sz)^\bullet$, then $[l] = [\&_{sz} a] = \&_t a$.

(2) If $a \notin (sz)^\bullet$, then

$$
[[r]]_{n+1} = \mathbb{Y}_{[z]_n} \bigcirc_{[\&_{sz} y_i]} [[u_i(a \leftarrow x)]]_{n+1} .
$$

Let $j$ be the unique index such that $a \in (su_j)^\bullet$. By induction,

$$
[[u_j(a \leftarrow x)]]_{n+1} = [[u_j]]_{n+1} \circ_{\&_{u_j} a} \mathbb{Y}_{[x]_n},
$$

$$
thus $[l] = [\&_{sz} y_j] \cdot \&_{u_j} a = \&_t a$. \hfill $\square$
$$

**Lemma 3.51** (Named readdressing lemma). Let $n \ge 1$ and $(E \triangleright \Gamma \vdash_n r : R)$ be a derivable sequent such that $[[r]]_{n+1}$ is well-defined. For $b \in (sr)^\bullet$, we have $\&_{sr} b = \wp_{[r]_{n+1}} \&_r b$ (recall the readdressing map $\wp$ from definition 2.27).
Proof. If $r$ is a variable, then by equation (3.46), $[[r]]_{n+1} = Y_{[[sr]]_n}$, and

$$ 
\begin{aligned}
\&_{sr} b &= \wp_{Y_{[r]_n}} [\&_{sr} b] && \text{by the results of appendix A.1} \\
&= \wp_{[[r]]_{n+1}} \&_r b && \text{see definition 3.38.}
\end{aligned}
$$

If $r$ is degenerate, say $r = \underline{x}$, then the result trivially holds as $sr = x$ only has one variable address. Otherwise, the sequent follows from an instance of the graft rule, say

$$ \frac{\dots \vdash_n t : T \quad \dots \vdash_n x : X}{\dots \vdash_n r : R} \text{ graft-a} $$

where by induction, $\&_{st} a = \wp_{[[t]]_{n+1}} \&_t a$ for all $a \in (st)^{\bullet}$. Since $sr = (st)[sx/a]$, we have

$$ 
\begin{aligned}
\&_{sr} b &= \left\{ 
\begin{array}{ll}
\&_{st} a \cdot \&_{sx} b & \text{if } b \in (sx)^{\bullet}, \\
\&_{st} a \cdot \&_{sx} c \cdot [p] & \text{if } b \in (st)^{\bullet}, \&_{st} a \subseteq \&_{st} b, \\
\&_{st} b & \text{say } \&_{st} b = \&_{st} a \cdot [\&_{sa} c] \cdot [p], \\
\&_{st} b & \text{if } b \in (st)^{\bullet}, \&_{st} a \not\subseteq \&_{st} b.
\end{array}
\right. \\
&= \wp([t]_{n+1} \circledast_t a Y_{[x]_n}) \&_r b && \text{see theorem A.14} \\
&= \wp_{[r]_{n+1}} \&_r b && \text{by equation (3.46).}
\end{aligned}
$$

□

**Lemma 3.52.** Let $(E \triangleright \Gamma \vdash \dots)$ be a derivable sequent, $u, v \in T_{\Gamma,n}$ be $n$-terms, where $u$ is non-degenerate, say $u = y(\overline{a_i \leftarrow \overrightarrow{w_i}})$. Let $x \in u^{\bullet}$ be a variable such that $sx = sv$. In particular, the substitution $u[v/x]$ is well-defined. Further, assume that $t[[v]]_{n+1} = [[x]]_n$. Then $[[u[v/x]]]_{n+1} = [[u]]_{n+1} \square \&_u x [[v]]_{n+1}$.

Proof. (1) If $x =_E y$, then

$$ 
\begin{aligned}
& [[u[v/x]]_{n+1} \\
&= [[v(\overline{a_i \leftarrow \overrightarrow{w_i}})]_{n+1} \\
&= [[v]]_{n+1} \bigcirc_{\&_v a_i} [[w_i]]_{n+1} \\
&= \left( Y_{[[x]]_n} \bigcirc_{[[\wp_{[[v]]_{n+1}} \&_v a_i]} [[w_i]]_{n+1} \right) \Box_{\Box} [[v]]_{n+1} && \text{since } t[[v]]_{n+1} = [[x]]_n \\
&= \left( Y_{[[x]]_n} \bigcirc_{[\&_{sv} a_i]} [[w_i]]_{n+1} \right) \Box_{\Box} [[v]]_{n+1} && \diamond \\
&= \left( Y_{[[x]]_n} \bigcirc_{[\&_{sx} a_i]} [[w_i]]_{n+1} \right) \Box_{\Box} [[v]]_{n+1} && \text{by assumption} \\
&= [[u]]_{n+1} \Box_{\Box} [[v]]_{n+1} \\
&= [[u]]_{n+1} \&_{u} x [[v]]_{n+1} && \spadesuit
\end{aligned}
$$

where $\spadesuit$ is by equation (3.46), $\diamond$ follows from lemma 3.51, and $\spadesuit$ follows from the fact that $x$ is the head variable of $u$ (see definition 3.38).
(2) If $x \neq_E y$, then by lemma 3.36, there is a unique index $j$ such that $x \in w_j^\bullet$. We have

$$ \begin{align*} \llbracket u[v/x] \rrbracket_{n+1} &= \llbracket y(\dots, a_j \leftarrow w_j[v/x], \dots) \rrbracket_{n+1} \\ &= \left( Y_{\llbracket y \rrbracket_n} \bigcirc_{[\&_{s_y} a_i], i \neq j} \llbracket w_i \rrbracket_{n+1} \right) \circ_{[\&_{s_y} a_j]} \llbracket w_j[v/x] \rrbracket_{n+1} \quad \spadesuit \\ &= \left( Y_{\llbracket y \rrbracket_n} \bigcirc_{[\&_{s_y} a_i], i \neq j} \llbracket w_i \rrbracket_{n+1} \right) \circ_{[\&_{s_y} a_j]} \left( \llbracket w_j \rrbracket_{n+1} \bigcirc_{w_j} x \llbracket v \rrbracket_{n+1} \right) \quad \text{by induction} \\ &= \llbracket u \rrbracket_{n+1} \llbracket \&_{s_y} a_j \rrbracket \&_{w_j} x \llbracket v \rrbracket_{n+1} \quad \diamond \\ &= \llbracket u \rrbracket_{n+1} \llbracket \&_u x \rrbracket \llbracket v \rrbracket_{n+1} \quad \spadesuit \end{align*} $$

where $\spadesuit$ is by equation (3.46), $\diamond$ is just a rearrangement of terms, and $\spadesuit$ is definition 3.38.

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

**Proposition 3.53.** Let $n \ge 1$ and $(E \triangleright \Gamma \vdash_n r : R)$ be a derivable sequent such that $\llbracket r \rrbracket_{n+1}$ is well-defined. Then $t \llbracket r \rrbracket_{n+1} = \llbracket sr \rrbracket_n$.

*Proof.* (1) If $r \in \mathbb{V}_n$ is a variable, then

$$ \begin{align*} t \llbracket r \rrbracket_{n+1} &= t Y_{\llbracket r \rrbracket_n} && \text{by equation (3.46)} \\ &= \llbracket r \rrbracket_n. \end{align*} $$

(2) If $r$ is a degenerate term, say $r = \underline{x}$ for $x \in \mathbb{V}_{n-1}$, then

$$ \begin{align*} t \llbracket r \rrbracket_{n+1} &= t l_{\llbracket x \rrbracket_{n-1}} && \text{by equation (3.45)} \\ &= Y_{\llbracket x \rrbracket_{n-1}} \\ &= \llbracket x \rrbracket_n && \text{by equation (3.46)} \\ &= \llbracket sr \rrbracket_n && \text{see rule degen.} \end{align*} $$

(3) Otherwise, the sequent follows from an instance of the **graft rule**, say

$$ \frac{\dots \vdash_n t : T \quad \dots \vdash_n x : X}{\dots \vdash_n r : R} \text{ graft-a} $$

Let $[p] := \wp_{\llbracket t \rrbracket_{n+1}} \&_t a$. We have

$$ \begin{align*} t \llbracket r \rrbracket_{n+1} &= t \llbracket t(a \leftarrow x) \rrbracket_{n+1} && \text{by definition of graft-a} \\ &= t \left( \llbracket t \rrbracket_{n+1} \circ_{[\&_s a]} Y_{\llbracket x \rrbracket_n} \right) && \text{by lemma 3.50} \\ &= t \llbracket t \rrbracket_{n+1} \llbracket \underline{[p]} \rrbracket_n && \text{by proposition 2.37} \\ &= \llbracket st \rrbracket_n \llbracket \underline{[p]} \rrbracket_n && \text{by induction} \\ &= \llbracket st \rrbracket_n \&_{[\&_s a]} \llbracket \underline{[p]} \rrbracket_n && \text{by lemma 3.51} \\ &= \llbracket (st)[x/a] \rrbracket_n && \text{by lemma 3.52} \\ &= \llbracket sr \rrbracket_n && \text{by definition of graft-a.} \end{align*} $$
**Corollary 3.54.** Let $n \ge 1$ and $(E \triangleright \Gamma \vdash_n t : T)$ be a derivable sequent such that $[[t]]_{n+1}$ is well-defined. Then $\&_t$ exhibits a bijection

$$ (st)^{\bullet} \xrightarrow{\cong} [[t]]_{n+1}^{\prime}. $$

*Proof.* Since the readdressing map $\wp_{[[t]]_{n+1}}$ is a bijection, $\&_t$ can be expressed as the following composite:

$$ (st)^{\bullet} \xrightarrow{\&_t} \{\&_t a \mid a \in (st)^{\bullet}\} $$

$$ \xrightarrow{\wp_{[[t]]_{n+1}}} \{\&_{st} a \mid a \in (st)^{\bullet}\} \qquad \text{by lemma 3.51} $$

$$ = [[st]]_n^{\bullet} \qquad \text{by lemma 3.47} $$

$$ = (t[[t]]_{n+1})^{\bullet} \qquad \text{by proposition 3.53} $$

$$ \xrightarrow{\wp_{[[t]]_{n+1}}^{-1}} [[t]]_{n+1}^{\prime}. $$

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

**Proposition 3.55.** With variables as in equation (3.46), we have that for all $i$

$$ e_{[}[[u_i]]_{n+1} = s_{\&_{sx}} y_i [[x]]_n, $$

and the graftings are well-defined.

*Proof.* Write $u_i$ as $a(\overrightarrow{b_j \leftarrow v_j})$, and consider

$$ \begin{align*} e_{[}[[u_i]]_{n+1} &= t s_{[}[[u_i]]_{n+1} \\ &= t[[a]]_n && \text{by proposition 3.48} \\ &= t[[sa]]_n && \text{see equation (3.43)} \\ &= [[ssa]]_{n-1} && \text{by proposition 3.53} \\ &= [[sy_i]]_{n-1} && \text{by the conditions of graft} \\ &= [[y_i]]_{n-1} && \text{see equation (3.43)} \\ &= s_{\&_{sx}} y_i [[x]]_n && \text{by corollary 3.49.} \end{align*} $$

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

This result concludes the proof that cases (3.41), (3.42), (3.45), and (3.46). The rest of this section is dedicated to proving theorem 3.64 stating that $[[\cdot]]_n$ is a bijection modulo $\alpha$-equivalence. Recall that we are still in an induction spanning from definition 3.40 to theorem 3.64.

**Definition 3.56.** We define the *named coding function* $C^!$, that maps an $n$-opetope to a sequent typing an $n$-variable, as follows.

(1) Trivially, $C^!(\diamond)$ is obtained by the following proof tree:

$$ \overline{C^!(\diamond)} \text{ point} \qquad (3.57) $$

with an arbitrary choice of variable (different choices lead to equivalent sequents).
(2) For $\phi \in \mathbb{O}_{n-2}$ the sequent $C^!(I_\phi)$ is obtained by the following proof tree:

$$ \frac{C^!(\phi) = (E \triangleright \Gamma \vdash_{n-2} x : X)}{E \triangleright \Gamma \vdash_{n-1} \underline{x} : x \dashv\!\!\!\dashv\!\!\! X} \text{degen} \qquad (3.58) $$
$$ C^!(I_\phi) $$

(3) For $\psi \in \mathbb{O}_{n-1}$, the sequent $C^!(Y_\psi)$ is obtained by the following proof tree:

$$ \frac{C^!(\psi)}{C^!(Y_\psi)} \text{shift} \qquad (3.59) $$

with an arbitrary choice of fresh variable (different choices lead to equivalent sequents).

(4) Let $n \ge 2$, $\nu \in \mathbb{O}_n$ having at least one node, $[l] \in \nu^!$, and $\psi \in \mathbb{O}_{n-1}$ be such that the grafting $\nu \circ_{[l]} Y_\psi$ is well-defined. By induction, the proof trees of $C^!(\nu)$ and $C^!(\psi)$ both end with an instance of rule **shift**, and write the former as

$$ \frac{E \triangleright \Gamma \vdash_{n-1} t : T}{C^!(\nu)} \text{shift} $$

Then the sequent $C^!(\nu \circ_{[l]} Y_\psi)$ is obtained by the following proof tree:

$$ \frac{E \triangleright \Gamma \vdash_{n-1} t : T \quad C^!(\psi)}{F \triangleright \Upsilon \vdash_{n-1} u : U} \text{graft-a} \qquad (3.60) $$
$$ \frac{C^!(\nu \circ_{[l]} Y_\psi)}{C^!(\psi)} \text{shift} $$

where the variable $a \in (st)^{\bullet}$ is an $(n-2)$-variable such that $\&_{st} a = \wp_\nu[l]$ (see corollary 3.54), and where the adequate $\alpha$-conversions have been performed to fulfill the side conditions of **graft**.

**Proposition 3.61.** In proof tree (3.60), the instance of **graft** is well-defined.

*Proof.* If $n=2$, then all graftings are well-defined, as there exists only one 1-opetope. Assume that $n>2$, write $C^!(\psi) = (\cdots \vdash_{n-1} p : P)$, where $p \in \mathbb{V}_n$, and let $[q] := \wp_\nu[l]$. By induction on the number of nodes, and by theorem 3.64, we have that $[[t]]_n = [[C^!(\nu)]_n = \nu$. We have

$$ [[sa]]_{n-2} = [[a]]_{n-2} \qquad \text{see equation (3.43)} $$

$$ = [v_{[q]} st]_{n-2} \qquad \text{by definition of a} $$

$$ = s_{[q]} [[st]]_{n-1} \qquad \text{by proposition 3.48} $$

$$ = s_{[q]} t [[t]]_n \qquad \text{by proposition 3.53} $$

$$ = s_{[q]} t \nu \qquad \text{by inductively applying theorem 3.64} $$

$$ = e_{[l]} \nu \qquad \text{by (Glob2)} $$

$$ = t \psi \qquad \text{by assumption} $$

$$ = t [[p]]_{n-1} \qquad \text{by definition} $$

$$ = t [[sp]]_{n-1} \qquad \text{see equation (3.43)} $$

$$ = [[ssp]]_{n-2} \qquad \text{by proposition 3.53.} $$
By applying theorem 3.64 inductively, the polynomial coding $[[ - ]]_{n-2}$ is injective modulo $\alpha$-equivalence. Hence without loss of generality, we can assume $s = s \cdot s p$, and finally, the instance of the graft rule is well-defined. $\square$

**Proposition 3.62.** Let $n \ge 2$ and $\omega \in \mathbb{O}_n$ have at least three nodes. The sequent $C^!(\omega)$ does not depend on the decomposition of $\omega$ in corollas. Explicitly, for any two decompositions of $\omega$, say

$$ \omega = \left( \dots \left( Y_{s_{[p_1]}} \omega \circ_{[p_2]} Y_{s_{[p_2]}} \omega \right) \circ_{[p_3]} Y_{s_{[p_3]}} \omega \dots \right) \circ_{[p_k]} Y_{s_{[p_k]}} \omega \\ = \left( \dots \left( Y_{s_{[q_1]}} \omega \circ_{[q_2]} Y_{s_{[q_2]}} \omega \right) \circ_{[q_3]} Y_{s_{[q_3]}} \omega \dots \right) \circ_{[q_k]} Y_{s_{[q_k]}} \omega, $$

we have

$$ C^!\left(\left(Y_{s_{[p_1]}} \omega \circ_{[p_2]} Y_{s_{[p_2]}} \omega\right) \cdots \circ_{[p_k]} Y_{s_{[p_k]}} \omega\right) \approx C^!\left(\left(Y_{s_{[q_1]}} \omega \circ_{[q_2]} Y_{s_{[q_2]}} \omega\right) \cdots \circ_{[q_k]} Y_{s_{[q_k]}} \omega\right). $$

*Proof.* By definition, the sequence $[p_1], \dots, [p_k]$ (and likewise for $[q_1], \dots, [q_k]$) has the following property: for $1 \le i \le j \le k$, either $[p_i] \subseteq [p_j]$ or $[p_i]$ and $[p_j]$ are $\subseteq$-incomparable (recall that $\subseteq$ is the prefix order on $A_{n-1}$, see definition 2.41). Further, $\{[p_1], \dots, [p_k]\} = \omega^\bullet = \{[q_1], \dots, [q_k]\}$, i.e. the two sequences have the same elements. Consequently, the sequence $[q_1], \dots, [q_k]$ can be obtained from $[p_1], \dots, [p_k]$ by a series of transpositions of consecutive $\subseteq$-incomparable addresses.

It is thus enough to check the following: for $\nu \in \mathbb{O}_n$, two different leaf addresses $[l], [l'] \in \nu^1$ (which are necessarily $\subseteq$-incomparable), and $\psi, \psi' \in \mathbb{O}_{n-1}$ such that $t\psi = e_{[l]}\nu$ and $t\psi' = e_{[l']}\nu$, we have

$$ C^!\left(\left(\nu \circ_{[l]} Y_{\psi}\right) \circ_{[l']} Y_{\psi'}\right) = C^!\left(\left(\nu \circ_{[l']} Y_{\psi'}\right) \circ_{[l]} Y_{\psi}\right). $$

Write

$$ \begin{align*} C^!(\nu) &= (E_\nu \triangleright \Gamma_\nu \vdash_n t_\nu : s_\nu \mapsto X_\nu), \\ C^!(Y_\psi) &= (E_\psi \triangleright \Gamma_\psi \vdash_n x_\psi : s_\psi \mapsto X_\psi), \\ C^!(Y'_\psi) &= (E_{\psi'} \triangleright \Gamma_{\psi'} \vdash_n x_{\psi'} : s_{\psi'} \mapsto X_{\psi'}), \end{align*} $$

with $t_\nu \in \mathbb{T}_n$ and $x_\psi, x_{\psi'} \in \mathbb{V}_n$. Let $a, a' \in (s\nu)^\bullet$ be such that $\&_{s\nu} a = [l]$ and $\&_{s\nu} a' = [l']$ (see corollary 3.54). The sequents above are respectively obtained by the following proof trees:

$$ \begin{array}{l} \begin{array}{c} \dots \vdash t_\nu : s_\nu \mapsto X_\nu \quad \dots \vdash x_\psi : s_\psi \mapsto X_\psi \\ F \triangleright \Gamma_\nu \cup \Gamma_\psi \vdash t_\nu (a \leftarrow x_\psi) : s_\nu [s_\psi/a] \mapsto X_\nu \end{array} \text{ graft-}a \\ \begin{array}{c} \dots \vdash x_{\psi'} : s_{\psi'} \mapsto X_{\psi'} \\ G \triangleright \Gamma_\nu \cup \Gamma_\psi \cup \Gamma_{\psi'} \vdash t_\nu (a \leftarrow x_\psi)(a' \leftarrow x_{\psi'}) : s_\nu [s_\psi/a][s_{\psi'}/a'] \mapsto X_\nu \end{array} \text{ graft-}a' \\ \\ \begin{array}{c} \dots \vdash t_\nu : s_\nu \mapsto X_\nu \quad \dots \vdash x_{\psi'} : s_{\psi'} \mapsto X_{\psi'} \\ F' \triangleright \Gamma_\nu \cup \Gamma_{\psi'} \vdash t_\nu (a' \leftarrow x_{\psi'}) : s_\nu [s_{\psi'}/a'] \mapsto X_\nu \end{array} \text{ graft-}a' \\ \begin{array}{c} \dots \vdash x_\psi : s_\psi \mapsto X_\psi \\ G' \triangleright \Gamma_\nu \cup \Gamma_{\psi'} \cup \Gamma_\psi \vdash t_\nu (a' \leftarrow x_{\psi'})(a \leftarrow x_\psi) : s_\nu [s_{\psi'}/a'][s_\psi/a] \mapsto X_\nu \end{array} \text{ graft-}a \end{array} $$

It remains to prove that both those conclusions are $\alpha$-equivalent.

(1) By assumption on the graft rule, $a \notin s_{\psi'}^\bullet$ and $a' \notin s_\psi^\bullet$, and clearly,

$$ t_\nu(a \leftarrow x_\psi)(a' \leftarrow x_{\psi'}) = t_\nu(a' \leftarrow x_{\psi'})(a \leftarrow x_\psi). $$

(2) Again, since $a \notin s_{\psi'}^\bullet$ and $a' \notin s_\psi^\bullet$, we have $s_\nu[s_\psi/a][s_{\psi'}/a'] = s_\nu[s_{\psi'}/a'][s_\psi/a]$.
(3) Lastly, the equational theories $G$ and $G'$ are the union of $E_\nu$, $E_\psi$, and $E_{\psi'}$, and the potential additional equalities incurred by the independent substitutions $s_\psi/a$ and $s_{\psi'}/a'$. Hence $G = G'$. $\square$

**Corollary 3.63.** For any opetope $\omega \in \mathcal{O}$, the sequent $C^!(\omega)$ is uniquely defined up to $\alpha$-equivalence.

*Proof.* Clearly, proof trees (3.57), (3.58), and (3.59) are correct. In proposition 3.61, we have shown that the same holds for proof tree (3.60). Finally, in proposition 3.62, we have shown that for a non-degenerate opetope $\omega \in \mathcal{O}_n$, the sequent $C^!(\omega)$ does not depend on the decomposition of $\omega$. $\square$

**Theorem 3.64.** (1) The polynomial coding $[[-]_n$ is a bijection between the set of derivable sequents typing an $n$-variable (up to $\alpha$-equivalence), and $\mathcal{O}_n$. Its inverse is $C^!(-)$ restricted to $\mathcal{O}_n$.

(2) If $n \ge 1$, the polynomial coding $[[-]_n$ is a bijection between the set of derivable sequents typing an $(n-1)$-terms (up to $\alpha$-equivalence), and $\mathcal{O}_n$.

*Proof.* We prove point (1) first. The result is trivial if $n = 0, 1$, so we assume $n \ge 2$. We first show that for $\omega \in \mathcal{O}_n$ we have $[[C^!(\omega)]_n = \omega$.

(1) By definition of $[[-, [[C^!(\bullet)]_0 = \bullet$.

(2) With the same notations as in (3.58), and by induction, we have

$$[[C^!(I_\phi)]_n = I_{[[C^!(\phi)]_{n-2}} = I_\phi.$$

(3) With the same notations as in (3.59), and by induction, we have,

$$[[C^!(Y_\psi)]_n = Y_{[[C^!(\psi)]_{n-1}} = Y_\psi.$$

(4) With the same notations as in (3.60), and by induction, we have

$$\begin{align*}
[[C^!(\nu \circ Y_\psi)]_n &= [[C^!(\nu)]_n \circ_{[\&_{ss} u a]} [[C^!(Y_\psi)]_n \\
&= [[C^!(\nu)]_n \circ_{[l]} [[C^!(Y_\psi)]_n \\
&= \nu \circ Y_\psi.
\end{align*}$$

Conversely, we now show that for a derivable sequent $(E \triangleright \Gamma \vdash \alpha : T)$, we have an isomorphism $(E \triangleright \Gamma \vdash \alpha : T) \simeq C^!([E \triangleright \Gamma \vdash \alpha : T]_n)$.

(1) We have that $C^!([x : \emptyset]_0) = C^!(\bullet) \simeq (\triangleright x : \emptyset \vdash x : \emptyset)$.

(2) With the same notations as in equation (3.45), we have

$$C^!([\cdots \vdash \delta : \underline{x} \mapsto x \mapsto X]_n) = C^! (I_{[[x:X]]_n})$$

and both sequents $C^!([x:X]_n)$ and $(\cdots \vdash \delta : \underline{x} \mapsto x \mapsto X)$ are obtained by applying **degen** and **shift** to $(\cdots \vdash x : X)$. Thus $C^!([\cdots \vdash \delta : \underline{x} \mapsto x \mapsto X]_n) \simeq (\cdots \vdash \delta : \underline{x} \mapsto x \mapsto X)$.

(3) Lastly, consider the sequent $(\cdots \vdash \alpha : x(\overline{y_i \leftarrow u_i}) \mapsto T)$ as in equation (3.46). Then

$$\begin{align*}
C^!([\cdots \vdash \alpha : x(\overline{y_i \leftarrow u_i}) \mapsto T]_{n+1}) &= C^! \left( Y_{[x]_n} \bigcirc_{[\&_{sx} y_i]} [u_i]_{n+1} \right) \\
&\simeq (\cdots \vdash \alpha : x(\overline{y_i \leftarrow u_i}) \mapsto T').
\end{align*}$$
$$ \frac{\overline{\vdash_0 c : \emptyset} \text{ point} \qquad \overline{\vdash_0 a : \emptyset} \text{ point} \qquad \overline{\vdash_1 h : c \mapsto \emptyset} \text{ shift} \qquad \overline{\vdash_1 i : a \mapsto \emptyset} \text{ shift} \qquad \overline{\vdash_1 h(c \leftarrow i) : c[a/c] \mapsto \emptyset} \text{ graft-c}}{\vdash_1 h(c \leftarrow i) : c[a/c] \mapsto \emptyset} $$

and $c[a/c] = a$. Then,

$$ \vdots \qquad \frac{\vdash_1 h(c \leftarrow i) : a \mapsto \emptyset \qquad \vdash_2 \beta : h(c \leftarrow i) \mapsto a \mapsto \emptyset \qquad \text{shift}}{\vdash_2 \beta : h(c \leftarrow i) \mapsto a \mapsto \emptyset} $$

On the other hand we have

$$ \frac{\overline{\vdash_0 b : \emptyset} \text{ point} \qquad \overline{\vdash_0 a : \emptyset} \text{ point} \qquad \overline{\vdash_1 g : b \mapsto \emptyset} \text{ shift} \qquad \overline{\vdash_1 f : a \mapsto \emptyset} \text{ shift} \qquad \overline{\vdash_1 g(b \leftarrow f) : b[a/b] \mapsto \emptyset} \text{ graft-b}}{\vdash_1 g(b \leftarrow f) : b[a/b] \mapsto \emptyset} $$

and $b[a/b] = a$. Then,

$$ \vdots \qquad \frac{\vdash_2 \beta : h(c \leftarrow i) \mapsto a \mapsto \emptyset \qquad \vdash_1 g(b \leftarrow f) : \mapsto \emptyset \qquad \vdash_2 \alpha : g(b \leftarrow f) \mapsto a \mapsto \emptyset \qquad \text{shift} \qquad \vdash_2 \beta(i \leftarrow \alpha) : h(c \leftarrow i)[g(b \leftarrow f)/i] \mapsto a \mapsto \emptyset \qquad \text{graft-i}}{\vdash_2 \beta(i \leftarrow \alpha) : h(c \leftarrow i)[g(b \leftarrow f)/i] \mapsto a \mapsto \emptyset} $$

The last grafting is correct as $si = a = ss\alpha$, and $h(c \leftarrow i)[g(b \leftarrow f)/i] = h(c \leftarrow g(b \leftarrow f))$. Finally

$$ \vdots \qquad \frac{\vdash_2 \beta(i \leftarrow \alpha) : h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset \qquad \vdash_3 A : \beta(i \leftarrow \alpha) \mapsto h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset \qquad \text{shift}}{\vdash_3 A : \beta(i \leftarrow \alpha) \mapsto h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset} $$

The complete proof tree is as follows, where p, s, and g are abbreviations for point, shift, and graft, respectively:

$$ \frac{\overline{\vdash c : \emptyset} \text{ p} \qquad \overline{\vdash a : \emptyset} \text{ p} \qquad \overline{\vdash b : \emptyset} \text{ p} \qquad \overline{\vdash a : \emptyset} \text{ p} \qquad \overline{\vdash h : c \mapsto \emptyset} \text{ s} \qquad \overline{\vdash i : a \mapsto \emptyset} \text{ s} \qquad \overline{\vdash h(c \leftarrow i) : a \mapsto \emptyset} \text{ g-c} \qquad \overline{\vdash g : b \mapsto \emptyset} \text{ s} \qquad \overline{\vdash f : a \mapsto \emptyset} \text{ s} \qquad \overline{\vdash g(b \leftarrow f) : a \mapsto \emptyset} \text{ g-b} \qquad \overline{\vdash \beta : h(c \leftarrow i) \mapsto a \mapsto \emptyset} \text{ s} \qquad \overline{\vdash \alpha : g(b \leftarrow f) \mapsto a \mapsto \emptyset} \text{ s} \qquad \overline{\vdash \beta(i \leftarrow \alpha) : h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset} \text{ g-i} \qquad \overline{\vdash A : \beta(i \leftarrow \alpha) \mapsto h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset} \text{ s}}{\vdash A : \beta(i \leftarrow \alpha) \mapsto h(c \leftarrow g(b \leftarrow f)) \mapsto a \mapsto \emptyset} $$

This proof tree can be graphically represented as follows:
<figure><img src="image_50.png" /><figcaption>**Example 3.68 (A degenerate case).** The 3-opetope</figcaption></figure>

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

is derived as follows:

$$ \begin{array}{ccc} \text{point} & & \text{point} \\ \vdash a : \emptyset & \xrightarrow{\text{shift}} & \vdash a : \emptyset \\ \vdash f : a \mapsto \emptyset & & \vdash a : a \mapsto \emptyset \\ \text{shift} & & \text{shift} \\ \hline \text{graft-f} & & \text{graft-f} \\ \text{shift} & & \text{shift} \\ \hline \end{array} $$

<figure><img src="image_52.png" /><figcaption>**Example 3.69 (Another degenerate case).** The 3-opetope</figcaption></figure>

is derived as follows:

$$ \begin{array}{ccc} \text{point} & & \text{point} \\ \vdash b : \emptyset & \xrightarrow{\text{shift}} & \vdash a : \emptyset \\ \vdash g : b \mapsto \emptyset & & \vdash f : a \mapsto \emptyset \\ \text{shift} & & \text{shift} \\ \hline \text{graft-b} & & \text{graft-b} \\ \text{shift} & & \text{shift} \\ \hline \text{graft-f} & & \text{graft-f} \\ \hline \end{array} $$

and $g(b \leftarrow f)[a/f] = g$, with the added equality $a = b$.
$$ \frac{a = b \vdash \beta(f \leftarrow \delta) : g \mapsto a \mapsto \emptyset}{a = b \vdash A : \beta(f \leftarrow \delta) \mapsto g \mapsto a \mapsto \emptyset} \text{shift} $$

This proof tree can be graphically represented as follows:

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

**3.4 Python implementation** In this section, we briefly discuss the Python implementation [13] of the present work. System `OPT`¹ and all required syntactic constructs are implemented in `opetopy.NamedOpetope`. The rules are represented by functions `point`, `degen`, `shift`, `graft`, as well as `degen-shift` for the alternative rule presented in remark 3.29. Those rules are further encapsulated in rule instance classes `Point`, `Degen`, `shift`, `Graft`, and `DegenShift`, which represent rule instances in a proof tree, so constructing a derivation amounts to writing a Python term using those four classes. If that term evaluates without raising any exception, then the proof tree is considered correct.

<caption>Figure 3.1: Derivation of the arrow sequent using `opetopy.NamedOpetope`</caption>

```python
from opetopy.NamedOpetope import *

# We first derive the point that will act as the source of the arrow by
# invoking the point rule on variable "a".
a = Point("a")

# We then apply the shift rule on a by providing a fresh variable, here "f".
f = Shift(a, "f")

# Since we use names, the following sequent, while corresponding to the same
# opetope, is different from f

g = Shift(Point("b"), "g")

# Note that the function opetopy.NamedOpetope.Arrow can be used to concisely
# get a proof tree of ■.
```
<figure><img src="image_54.png" /><figcaption>Figure 3.3: Derivation of example 3.67 using `opetopy.NamedOpetope`</figcaption></figure>

<figure><img src="image_55.png" /><figcaption>Figure 3.4: Derivation of example 3.69 using `opetopy.NamedOpetope`</figcaption></figure>

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

**3.5 The system for opetopic sets** We now present `OPTSET'`, a derivation system for opetopic sets that is based on `OPT'`. We first present the required syntactic constructs and conventions in section 3.1.1, and present the inference rules in definition 3.71.
**3.5.1 Syntax** An interesting aspect of the named approach is that only the source faces are specified in the type of terms:

$$x : s.x \mapsto s.s.x \mapsto \dots$$

Nonetheless, as proven in proposition 3.53, all the information about targets remain. This comes from the intuition that any two opetopes with the same source are equal. In opetopic sets however, two cells with the same source faces need not be equal, nor have the same target. To adapt OPT¹ to opetopic sets, all faces, including targets, need to be explicitly specified. This will be part of rule **repr** of system OPTSET¹, presented in definition 3.71. Lastly, recall that a typical sequent in system OPT¹ looks like this:

$$E \triangleright \Gamma \vdash t : T.$$

Here, *t* represents a pasting diagram that will ultimately serve as the source of a new variable, which will be introduced using rule **shift**. It does not provide any additional information about the variables of Γ and their adjacencies. Thus, when describing opetopic sets, we will drop the right hand side of the sequent, and deal with expressions of the form (*E* ▷ Γ), called *opetopic contexts modulo theory* (or OCMT for short).

**Example 3.70.** As a preliminary example, the OCMT describing the opetopic set:

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

is given by

$$ \left( \begin{array}{l} b = tf, a = tg = tt\alpha = th = tt\beta \\ h = t\beta = t\alpha \end{array} \right. \quad \left( \begin{array}{l} a : \emptyset, b : \emptyset, tf : \emptyset, tg : \emptyset, tt\alpha : \emptyset, \\ th : \emptyset, tt\beta : \emptyset \\ \triangleright f : a \mapsto \emptyset, g : a \mapsto \emptyset, t\alpha : a \mapsto \emptyset, \\ h : a \mapsto \emptyset, t\beta : a \mapsto \emptyset \\ \alpha : g(b \leftarrow f) \mapsto a \mapsto \emptyset, \beta : h \mapsto a \mapsto \emptyset \end{array} \right) $$

On the right of ▷, we have all the variables and types, much like a context in OPT¹. The novelties are variables of the form *tx*, which indicate targets. For example, *tα*, the target of *α*, has type *a* ↦ *∅*, meaning that it is an arrow of source *a*. On the left hand side is an equational theory as in OPT¹, identifying variables. Note that *tα* is identified with *h*, as shown by the diagram above. See example 3.104 for a full treatment of this case.

**3.5.2 Inference rules** Our derivation system for opetopic sets, presented in definition 3.71, has four rules:

(1) **repr** that takes an opetope in our previous system and turns it into the representable opetopic set of that opetope by adding all the target faces;

(2) **zero** that constructs the empty OCMT, corresponding to the empty opetopic set;

(3) **sum** that takes the disjoint union of two opetopic sets;

(4) **glue** that identifies cells of an opetopic set.

Every finite opetopic set is a quotient of a finite sum of representables. Therefore, those rules should be enough to derive all finite opetopic sets, which is formally demonstrated in theorem 3.101.
**Definition 3.71** (The OPTSET' system). *Introduction of all targets.* This rule takes a sequent $(E \vdash \Gamma \vdash_n x : X)$ typing a variable $x \in \mathbb{V}_n$, and completes it by adding all the targets cells, and turning it into an OCMT:

$$ \frac{E \vdash \Gamma \vdash_n x : X}{E' \vdash \Gamma'} \text{ repr} $$

where

$$ \Gamma' := \Gamma \cup \{t^k a : s^{k+1} a \dashv s^{k+2} a \dashv \dots | a \in \mathbb{V}_{\Gamma',l}, 1 \le k \le l \le n\}, $$

and

$$ E' := E \cup \{ta = b \mid \text{for all } b \leftarrow a(\dots) \text{ occurring in a type in } \Gamma\} \quad (3.72) $$

$$ \cup \{tta = tv_{[k]}sa \mid a \in \mathbb{V}_{\Gamma',k}, sa \text{ non degen.}, 2 \le k \le n\} \quad (3.73) $$

$$ \cup \{t^2 a = b \mid \text{if } a: \underline{b} \dashv b \dashv \dots, a \in \mathbb{V}_{\Gamma',k} \ 2 \le k \le n\}. \quad (3.74) $$

Here, $t^k a = t \cdots ta$ can be thought of as a “tagging” on the variable $a \in \mathbb{V}_l$, but for simplicity, we consider it as a variable of its own: $t^k a \in \mathbb{V}_{l-k}$. We also assume that variables of this form can only arise from applications of this rule. By convention, $t^0 a := a$, and if $a = b$, then $ta = tb$, for all $a, b \in \Gamma'$. In line (3.73), the source of $a$ is assumed non-degenerate, thus $sa$ is a term of the form $x(\overline{y_i \leftarrow u_i})$, and $v_{[k]}sa = x$ (see definition 3.38).

**Zero.** This rules introduces the empty OCMT:

$$ \vdash \text{ zero} $$

**Binary sums.** This rule takes two disjoint opetopic sets (i.e. whose cells have different names), and produces their sum. If $\Gamma \cap \Upsilon = \emptyset$ (which implies that $E \cap F = \emptyset$), then

$$ \frac{E \vdash \Gamma \quad F \vdash \Upsilon}{E, F \vdash \Gamma, \Upsilon} \text{ sum} $$

**Quotients.** This rule identifies two parallel cells in an opetopic set by extending the underlying equational theory. If $a, b \in \mathbb{V}_\Gamma$ are such that $sa =_E sb$ and $ta =_E tb$, then

$$ \frac{E \vdash \Gamma}{E, a = b \vdash \Gamma} \text{ glue} $$

We also write glue-(a=b) to make explicit that we added {a=b} to the theory.

**Remark 3.75.** In rule repr, the additional equalities of (3.72) enforce (Inner), those of (3.73) enforce (Glob1), and those of (3.74) enforce (Degen). Condition (Glob2) is implemented in (3.72), by the definition of the type of the target variables ta: the bookkeeping of the readdressing map is completely transparent, as for an n-variable x, the correspondence between the (n-1)-variables of sx and (n-1)-variables of stx is already established by their name! See also remark 4.18.

**Remark 3.76.** Akin to OPT', in OPTSET', an OCMT that is equivalent to a derivable one is itself derivable.
Remark 3.77. The sum and zero rules may be replaced by the following usum rule (unbiased sum) without changing the set of derivable OCMTs. For $k \ge 0$, and for $(E_1 \triangleright \Gamma_1), \dots, (E_k \triangleright \Gamma_k)$ OCMTs such that $\Gamma_i \cap \Gamma_j = \emptyset$ for all $i \neq j$, then

$$ \frac{E_1 \triangleright \Gamma_1 \quad \dots \quad E_k \triangleright \Gamma_k}{E_1, \dots, E_k \triangleright \Gamma_1, \dots, \Gamma_k} \text{ usum} $$

## 3.6 Equivalence with opetopic sets

### 3.6.1 Opetopic sets from OCTMs

Notation 3.78. Let $E \triangleright \Gamma$ be an OCMT. We write $\Gamma/E$ for the set $\mathbb{V}_\Gamma$ quotiented by the equivalence relation generated by the equational theory $E$.

**Definition 3.79 (OCMT of a variable).** For $(E \triangleright \Gamma \vdash_n x : X)$ a derivable sequent in system $OPT^!$, where $x \in \mathbb{V}_n$, let $(T_x \triangleright C_x)$, the OCMT of $x$ (leaving the sequent around $x$ implicit), be given by the following instance of repr:

$$ \frac{E \triangleright \Gamma \vdash_n x : X}{T_x \triangleright C_x} \text{ repr} $$

We now establish a series of results to prove that $C_x/T_x$ carries a natural structure of representable opetopic set. We proceed in 4 steps:

(1) we start by noting that $C_x/T_x$ is naturally a set over $\emptyset$ via the polynomial coding map $[-]$ (proposition 3.81);

(2) then, in proposition 3.83, we construct source and target maps in $C_x/T_x$, i.e. the structure maps of an opetopic set;

(3) we show in theorem 3.84 that the opetopic identities of definition 2.44 are satisfied, and that consequently, $C_x/T_x$ has the structure of an opetopic set;

(4) finally, we show in proposition 3.91 that $C_x/T_x$ is in fact a representable opetopic set, using a counting argument.

From there, we define a structure of opetopic set on an arbitrary OCMT by induction on its proof tree in definition 3.92.

**Definition 3.80.** Let $(E \triangleright \Gamma \vdash_n x : X)$ be a derivable sequent on $OPT^!$, where $x \in \mathbb{V}_n$, and $a \in \mathbb{V}_{C_x,k}$. If $a \in \mathbb{V}_{\Gamma,k}$, recall that by proposition 3.37, $a$ is typed by the derivable sequent $(E|_a \triangleright \Gamma|_a \vdash_k a : A)$, where $(-)|_a$ denotes restriction of contexts and theories to $a$ and to the variables occurring in the type $A$. Thus we have a well-defined opetope $[[a]]_k = [[E|_a \triangleright \Gamma|_a \vdash_k a : A]]_k \in \emptyset_k$. Otherwise, if $a = t^l b$ for some $b \in \mathbb{V}_{\Gamma,k+l}$, then $sa = s^{l+1} b$, and define $[[a]]_k := [[s^{l+1} b]]_k$. We thus have a map $[-] : \mathbb{V}_{C_x} \to \emptyset$.

**Proposition 3.81.** The map $[-] : \mathbb{V}_{C_x} \to \emptyset$ factors through $C_x/T_x$.

*Proof.* By construction, the theory $T_x$ identifies variables $a, b \in \mathbb{V}_{C_x,k}$ only if $sa = sb$, thus $[[a]]_k = [[sa]]_k = [[sb]]_k = [[b]]_k$. $\square$

**Definition 3.82.** For $\psi \in \emptyset_k$, write

$$ (C_x/T_x)_\psi = \{a \in \mathbb{V}_{C_x,k} | [[a]]_k = \psi\}. $$

We now construct source and target maps between those subsets.
**Sources.** If $[p] \in [[a]]_k^\bullet$, then by corollary 3.54, there is a unique $b \in \mathbb{V}_{C_x|a,k-1}$ such that $\&_{sa} b = [p]$. Let $v_{[p]} a := b$.

**Target.** For $a \in \mathbb{V}_{C_x,k}$, $k > 0$, we set $t(a) := ta$, the latter being a variable introduced by the repr rule.

**Proposition 3.83.** Let $a \in \mathbb{V}_{C_x,k}$.

(1) For $[p] \in [[a]]_k^\bullet$ we have $[v_{[p]} s a]_{k-1} = s_{[p]} [[a]]_k$.

(2) We have $[ta]_{k-1} = t[[a]]_k$.

*Proof.* (1) It $a$ is not a target i.e. $a \neq tb$ for any $b \in \mathbb{V}_{C_x,k}$, then this is already proven by proposition 3.48. If $a = t^l b$ for some $b \in \mathbb{V}_{C_x,k+l}$ that is not a target, and $l \in \mathbb{N}$, then

$$ 
\begin{align*}
[\mathbf{v}_{[p]} \mathbf{s} \mathbf{a}]_{k-1} &= [\mathbf{v}_{[p]} \mathbf{s} t^l \mathbf{b}]_{k-1} && \text{see definition of repr} \\
&= [\mathbf{v}_{[p]} \mathbf{s}^{l+1} \mathbf{b}]_{k-1} && \text{by proposition 3.48} \\
&= \mathbf{s}_{[p]} [\mathbf{s} \mathbf{s}^l \mathbf{b}]_k && \text{see equation (3.43)} \\
&= \mathbf{s}_{[p]} [\mathbf{s} \mathbf{a}]_k && \text{see equation (3.43)} \\
&= \mathbf{s}_{[p]} [\mathbf{a}]_k && \text{see equation (3.43)}.
\end{align*}
$$

(2) If $a$ is not a target, then

$$ 
\begin{align*}
t[[a]]_k &= t[[s a]]_k && \text{see equation (3.43)} \\
&= [[s s a]]_{k-1} && \text{by proposition 3.53} \\
&= [[s t a]]_{k-1} && \text{see definition of repr} \\
&= [[t a]]_{k-1} && \text{see equation (3.43)}.
\end{align*}
$$

If $a = t^l b$ for some $b \in \mathbb{V}_{C_x,k+l}$ that is not a target, and $l \in \mathbb{N}$, then

$$ 
\begin{align*}
t[[a]]_k &= t[[s a]]_k && \text{see equation (3.43)} \\
&= t[[s t^l b]]_k && \text{see equation (3.43)} \\
&= t[[s^{l+1} b]]_k && \text{see definition of repr} \\
&= [[s^{l+2} b]]_{k-1} && \text{see definition of repr} \\
&= t[[s t^{l+1} b]]_k && \text{see definition of repr} \\
&= [[s t a]]_{k-1} && \text{see equation (3.43)} \\
&= [[t a]]_{k-1} && \text{see equation (3.43)}.
\end{align*}
$$

□

**Theorem 3.84.** With all the structure of definition 3.82, $C_x/T_x$ is an opetopic set.

*Proof.* We check the opetopic identities of definition 2.44. Take $a \in \mathbb{V}_{C_x,k}$.

(Inner) Take $[p[q]] \in [[a]]_k^\bullet$, and write $d = v_{[p[q}}} s a$. In $s a$, the variable $d$ occurs as

$$ s a = \dots, b(\dots, c \leftarrow d(\dots), \dots), \dots $$

where $b = v_{[p]} s a$ and $c = v_{[q]} s b$. By equation (3.72), $v_{[q]} v_{[p]} a = v_{[q]} b = c = t d = t v_{[p[q]}} a$.

(Glob1) Assume that $s a$ is not degenerate. Then, by equation (3.73), we have $t t a = t v_{[l]} a$.
(Glob2) Assume that $sa$ is not degenerate, take $[p[q]] \in [[a]]_k^!$, and let $c := v_{[q]} v_{[p]} a$. Then

$$
\begin{align*}
\wp_{[a]}[p[q]] &= \wp_{[sa]}[p[q]] && \text{see equation (3.43)} \\
&= \wp_{[sa]} &\&_{sa} c && \text{by definition} \\
&= \&_{ssa} c && \text{by lemma 3.51} \\
&= \&_{sta} c && \text{see definition of repr.}
\end{align*}
$$

and thus $v_{[q]} v_{[p]} a = c = v_{& sta} c ta = v_{\wp_{[a]}[p[q}}} ta$.

(Degen) Assume that $sa$ is degenerate, say $sa = \underline{b}$. Then by equation (3.74), $v_{[l]} ta = b = tta = t^0 a = a$. $\square$

**Lemma 3.85.** The opetopic set $C_x/T_x$ is a quotient of the representable $\mathcal{O}[[x]]_n$.

*Proof.* The category of elements $\mathcal{O}/(C_x/T_x)$ of $C_x/T_x$ is a direct category since $\mathcal{O}$ is too. It has a terminal object, namely the equivalence class of variable $x$ itself. Moreover, that element is in the $[[x]]_n$ component of $C_x/T_x$. By the Yoneda lemma, there is a map $f: \mathcal{O}[[x]]_n \to C_x/T_x$ which induces a discrete fibration $\mathcal{O}/\mathcal{O}[[x]]_n = \mathcal{O}/[[x]]_n \to \mathcal{O}/(C_x/T_x)$ between the categories of elements. Since $f$ has the terminal object $x$ in its image, it is surjective on objects. $\square$

Let $(E \to \Gamma \vdash_n x : X)$ be a derivable sequent, with $x \in V_n$. In lemma 3.85, we established that $C_x/T_x$ is a quotient of the representable opetopic set $\mathcal{O}[[x]]_n$. We now aim to show that the two are actually isomorphic (proposition 3.91) by showing that they have the same number of cells.

**Definition 3.86.** for $\omega \in \mathcal{O}$, let

$$
\#\omega := \sum_{\psi \in \mathcal{O}} \#\mathcal{O}[\omega]_{\psi} = \sum_{\psi \in \mathcal{O}} \#\mathcal{O}(\psi, \omega),
$$

which is a finite number since the slice category $\mathcal{O}/\omega$ is finite.

The strategy of the proof of proposition 3.91 is to show that the number of cells in $C_x/T_x$ is precisely $\#[[x]]_n$. We need some preliminary results first.

**Proposition 3.87.** (1) We have $\#\diamond = 1$, and $\#\blacksquare = 3$.

(2) If $\omega$ is an endotope, say $\omega = Y_\psi$, then $\#\omega = 2 + \#\psi$.

(3) If $\omega$ is a degenerate opetope, say $\omega = I_\phi$, then $\#\omega = 2 + \#\phi$.

(4) If $\omega = \nu \circ_{[l]} Y_\psi$, for some $\nu \in \mathcal{O}_n$, $[l] \in \nu^!$, and $\psi \in \mathcal{O}_{n-1}$, then $\#\omega = \#\nu + \#\psi - \#e_{[l]} \nu$.

*Proof.* Point (1) is clear. We now prove point (2). Since source and target embeddings are generators of $\mathcal{O}$ (see definition 2.44), a non-identity morphism $f$ with codomain $\omega$ necessarily factors through a source or the target embedding of $\omega$; in this case, through $s_{[\cdot]} : \psi \to \omega$ or $t : \psi \to \omega$ (or both). However, by relations (Glob1) and (Glob2), if $f$ is not the target embedding of $\omega$, then it necessarily factors through $s_{[\cdot]} : \psi \to \omega$. By inspection of the opetopic identities of definition 2.44, $s_{[\cdot]} : \psi \to \omega$ is a monomorphism. Indeed, it is impossible to paste the relation squares of definition 2.44 into one of the form

<figure><img src="image_58.png" /></figure>
with $f \neq g$. Consequently, as sets,

$$ \mathcal{O}/\omega \cong \mathcal{O}/\psi + \{t : \psi \to \omega\} + \{\mathrm{id}_{\omega} : \omega \to \omega\}, $$

and the result follows. Points (3) and (4) follow the same type of argument. $\square$

**Corollary 3.88.** If $\omega \in \mathcal{O}_{\ge 2}$ is not degenerate, then

$$ \#\omega = 2 + \left( \sum_{[p] \in \omega^{\bullet}} \#s_{[p]}\omega \right) - \left( \sum_{[p[q]] \in \omega^{\bullet}} \#s_{[q]}s_{[p]}\omega \right) $$

*Proof.* If $\omega$ is an endotope, the result is already proved in proposition 3.87. Otherwise, decompose $\omega$ as $\nu \circ_{[l]} Y_{\psi}$, and assume by induction that the result holds for $\nu$. We have

$$ \begin{align*} \#\omega &= \#\nu + \#\psi - \#e_{[l]}\nu & \blacksquare \\ &= 2 + \left( \#\psi + \sum_{[p] \in \nu^{\bullet}} \#s_{[p]}\nu \right) - \left( \#e_{[l]}\nu + \sum_{[p[q]] \in \nu^{\bullet}} \#s_{[q]}s_{[p]}\nu \right) & \diamond \\ &= 2 + \left( \#s_{[l]}\nu + \sum_{\substack{[p] \in \omega^{\bullet} \\ [p] \neq [l]}} \#s_{[p]}\nu \right) - \left( \#e_{[l]}\nu + \sum_{\substack{[p[q]] \in \omega^{\bullet} \\ [p[q]] \neq [l]}} \#s_{[q]}s_{[p]}\nu \right) \\ &= 2 + \left( \sum_{[p] \in \omega^{\bullet}} \#s_{[p]}\nu \right) - \left( \sum_{[p[q]] \in \omega^{\bullet}} \#s_{[q]}s_{[p]}\nu \right), \end{align*} $$

where $\blacksquare$ is by proposition 3.87, and $\diamond$ is by induction. $\square$

**Example 3.89.** Consider the opetopic integer $n \in \mathcal{O}_2$ from example 2.36:

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

We show that $\#n = 2n + 3$. If $n = 0$, then $\#0 = \#1_{\blacksquare} = 2 + \#\diamond = 3$. This can be read on the graphical representation of $0$, that has one point, one simple arrow, and one double arrow, for a total of 3 cells. If $n = 1$, then $\#1 = \#Y_{\blacksquare} = 2 + \#\blacksquare = 5$. Otherwise,

$$ \begin{align*} \#\mathbf{n} &= \#\left( (\mathbf{n}-\mathbf{1}) \circ_{[*^{n-1}]} Y_{\blacksquare} \right) && \text{by definition of } \mathbf{n} \\ &= \#(\mathbf{n}-\mathbf{1}) + \#\blacksquare - \#e_{[*^{n-1}]}(\mathbf{n}-\mathbf{1}) && \text{by proposition 3.87} \\ &= (2n+1)+3-\#\diamond && \text{by induction} \\ &= (2n+1)+3-1 = 2n+3. \end{align*} $$

**Example 3.90.** Consider the 3-opetope $\omega = Y_2 \circ_{[[*]]} Y_0$ of example 3.69:

<figure><img src="image_60.png" /></figure>
Then,

$$
\begin{align*}
\#\omega &= \#\left(\mathbb{Y}_2 \circ_{[[*]]} \mathbb{Y}_0\right) \\
&= \#\mathbb{Y}_2 + \#\mathbf{0} - \#\mathbf{e}_{[[*]]} \mathbb{Y}_2 && \text{by proposition 3.87} \\
&= 2 + \#\mathbf{2} + \#\mathbf{0} - \#\blacksquare && \text{by proposition 3.87} \\
&= 9 && \text{since } \#\mathbf{n} = 2n + 3.
\end{align*}
$$

**Proposition 3.91.** We have $C_x/T_x \cong O[[x]]_n$.

Proof. (1) If $x = \diamond$, then $\mathbb{V}_{C_x} = \diamond$, while $T_x = \emptyset$. Thus $\#C_x/T_x = 1 = \#\diamond$ by proposition 3.87. We know by lemma 3.85 that $C_x/T_x$ is a quotient of $O[[x]]_n$, and we just showed that the two have the same number of cells, namely $\#\diamond = 1$. Consequently, $C_x/T_x \cong O[[x]]_0$.

(2) Likewise, if $x = \blacksquare$, then $\mathbb{V}_{C_x} = \{\diamond, \blacksquare, \blacksquare\}$, while $T_x = \emptyset$. Thus $\#C_x/T_x = 3 = \#\blacksquare$ by proposition 3.87, and by the argument above, $C_x/T_x \cong O[[x]]_1$.

(3) Assume now that $x \in \mathbb{V}_n$ for $n \ge 2$. We proceed by case analysis on the form of $\mathfrak{s}x$.

(a) If $\mathfrak{s}x = y \in \mathbb{V}_{n-1}$, then $[[x]]_n = \mathbb{Y}_{[y]_{n-1}}$, and by proposition 3.87, $\#[[x]]_n = 2 + \#[[y]]_{n-1}$. Then $C_x = C_y + \{\mathfrak{t}^k x \mid 0 \le k \le n\}$, and $\mathfrak{t}tx =_{T_x} \mathfrak{t}v_{[1]} x = \mathfrak{t}y$. Consequently, $T_x$ is equivalent to the theory $T_y + \{\mathfrak{t}tx = \mathfrak{t}y\}$, and thus

$$
C_x/T_x \cong C_y/T_y + \{x, tx\}.
$$

By induction, $C_y/T_y \cong O[[y]]_{n-1}$, and $\#C_x/T_x = 2 + \#C_y/T_y = 2 + \#[[y]]_{n-1} = \#[[x]]_n$, which, by the same argument as above, proves the isomorphism $C_x/T_x \cong O[[x]]_n$.

(b) If $\mathfrak{s}x = \underline{a}$ for some $a \in \mathbb{V}_{n-2}$, then $[[x]]_n = \mathfrak{l}_{[a]_{n-2}}$, and by proposition 3.87, $\#[[x]]_n = 2 + \#[[a]]_{n-2}$. Then $C_x = C_a + \{\mathfrak{t}^k x \mid 0 \le k \le n\}$, and $\mathfrak{t}tx =_{T_x} a$. Therefore $T_x$ is equivalent to the theory $T_a + \{\mathfrak{t}tx = a\}$, and thus

$$
C_x/T_x \cong C_a/T_a + \{x, tx\}.
$$

Consequently, $\#C_x/T_x = 2 + \#C_a/T_a = 2 + \#[[a]]_{n-2} = \#[[x]]_n$.

(c) Assume $\mathfrak{s}x = t(a \leftarrow y)$, for some $t \in \mathbb{T}_{n-1}$, $a \in \mathbb{V}_{n-2}$, and $y \in \mathbb{V}_{n-1}$. Let $z : t \mapsto \dots$ be a fresh $n$-variable. Clearly, $C_z - \{z, tz\} \subseteq C_x$, thus

$$
C_x = C_y \cup (C_z - \{\mathfrak{t}^k z \mid 0 \le k \le n\}) + \{\mathfrak{t}^k x \mid 0 \le k \le n\},
$$

while $T_x$ is equivalent to $T_y \cup T_z + \{\mathfrak{t}y = a, \mathfrak{t}tx = \mathfrak{t}v_{[1]} x\}$. Since $v_{[1]} \mathfrak{s}x = v_{[1]} t = v_{[1]} \mathfrak{s}z$, and $\mathfrak{t}v_{[1]} \mathfrak{s}z =_{T_z} \mathfrak{t}tz$ (see equation (3.73)), we have

$$
C_x/T_x = C_y/T_y \cup C_z/T_z + \{x,tx\} - \{z,tz\}.
$$

By hypothesis of the **graft rule**, $C_z/T_z \cap C_y/T_y = C_a/T_a$, and thus we have

$$
\begin{align*}
\#C_x/T_x &= \#C_y/T_y + \#C_z/T_z - \#C_a/T_a \\
&= \#[[y]]_{n-1} + \#[[z]]_n - \#[[a]]_{n-2} \\
&= \#([[t]]_n \circ_{\&t a} \mathbb{Y}_{[y]_{n-1}}) && \text{by proposition 3.87} \\
&= \#[[x]]_n.
\end{align*}
$$

□
We now extend the structure of opetopic set defined in definition 3.82 to all OCMTs.

**Definition 3.92.** Let $(E \triangleright \Gamma)$ and $(F \triangleright \Upsilon)$ be two OCMTs, and assume by induction that $\Gamma/E$ and $\Upsilon/F$ have a structure of opetopic set.

(1) If $(G \triangleright \Xi)$ is given by

$$ \frac{E \triangleright \Gamma \quad F \triangleright \Upsilon}{G \triangleright \Xi} \text{ sum} $$

then we have $\Xi = \Gamma + \Upsilon$, and $G = E + F$. There are natural set maps $i: \Gamma/E \to \Xi/G$ and $j: \Upsilon/F \to \Xi/G$, and clearly, there is a unique structure of opetopic set on $\Xi/G$ making $i$ and $j$ into morphisms of opetopic sets. Further, $\Xi/G$ is the coproduct of $\Gamma/E$ and $\Upsilon/F$, and $i$ and $j$ are the coprojections.

(2) Let $a, b \in \mathbb{V}_{\Gamma,k}$ be such that $sa =_E sb$ and $ta =_E tb$. Note that $O[[a]]_k = O[[b]]_k$. Then, by definition of rule *glue*, and for $(F \triangleright \Gamma)$ given by

$$ \frac{E \triangleright \Gamma}{F \triangleright \Gamma} \text{ glue-}(a=b) $$

we have $F = E + \{a = b\}$. There is an obvious surjective set-map $p: \Gamma/E \to \Gamma/F$, that identifies $a$ and $b$, and preserves the other elements. From here, it is easy to see that there is a unique structure of opetopic set on $\Gamma/F$ such that $p$ is a morphism. In more details, if $x \in \Gamma/F$ is not the class of $a$ or $b$, then its shape, sources, and target are the same as its unique preimage in $\Gamma/E$. Otherwise, since $sa =_E sb$ and $ta =_E tb$, $a$ and $b$ have the same shape, sources, and target (i.e. they are parallel), and so we can assign those of $x$ accordingly.

Furthermore, it is easy to see that the following diagram exhibits $p$ as the coequalizer of the maps $a$ and $b$:

$$ O[[a]]_k \xrightarrow{a \atop b} \Gamma/E \xrightarrow{p} \Gamma/F. \qquad (3.93) $$

**Proposition 3.94.** For $(E \triangleright \Gamma)$ a derivable OCMT in $\text{OPTSET}^!$, the structure of opetopic set on $\Gamma/E$ does not depend on the proof tree of $(E \triangleright \Gamma)$.

*Proof.* If $\Gamma = \emptyset$, i.e. if the OCMT is obtained using the **zero rule**, then the result trivially holds. Otherwise, it is easy to see that the opetopic set $\Gamma/E$ is given by the following expression that does not depend on the proof tree of $(E \triangleright \Gamma)$:

$$ \Gamma/E \cong \frac{\sum_{k \in \mathbb{N}, a \in \mathbb{V}_{\Gamma,k}} O[[a]]_k}{a \sim b, \text{ for all } a, b \in \mathbb{V}_{\Gamma} \text{ s.t. } a =_E b}. $$

By definition 3.80, for $a \in \mathbb{V}_{\Gamma}$, the opetope $[[a]]_k$ only depends on the sequent. $\square$

### 3.6.2 The equivalence
Recall that $\mathbb{O}_{\text{fin}}$ is the full subcategory of $\mathbb{O}$ spanned by finite opetopic sets. In this subsection, we provide the last results needed to establish the equivalence between the category of derivable OCMTs and $\mathbb{O}_{\text{fin}}$.

*Notation 3.95.* For $(E \triangleright \Gamma)$ an OCMT, and $a, b \in \mathbb{V}$, the substitution $\Gamma[a/b]$ is defined in the obvious manner, by applying it to all typings in $\Gamma$.

**Definition 3.96 (Morphism of OCMTs).** Let $(E \triangleright \Gamma)$ and $(F \triangleright \Upsilon)$ be OCMTs. A morphism $f: (E \triangleright \Gamma) \to (F \triangleright \Upsilon)$ is a (non necessarily bijective) map $f: \mathbb{V}_{\Gamma} \to \mathbb{V}_{\Upsilon}$ compatible with $E$ and
F, such that if $x: X$ is a typing in $\Gamma$, then $f(x): f(X)$ is a typing in $\Upsilon$, where $f(X)$ is the result of applying $f$ to every variable in $X$. Further, we require that for $n \ge 1$ and $x \in \mathbb{V}_{\Gamma,n}$, we have $f(t \cdot x) = t f(x)$. Note that this condition implies that $f$ preserves the dimension of variables. Also, if $f,g: (E \triangleright \Gamma) \rightarrow (F \triangleright \Upsilon)$, and if for all $x \in \mathbb{V}_{\Gamma}$ we have $f(x)=_F g(x)$, then we consider $f$ and $g$ to be equivalent, and only consider maps up to equivalence.

**Lemma 3.97.** *Morphisms of OCMTs preserve the shape of variables, i.e. for $f: (E \triangleright \Gamma) \rightarrow (F \triangleright \Upsilon)$ a morphism and $a \in \mathbb{V}_{\Gamma,k}$, we have $[[a]]_k = [[f(a)]]_k$.*

*Proof.* Since there is a unique 0-opetope and a unique 1-opetope, the result holds trivially if $k=0,1$. If $k \ge 2$, we proceed by induction on $sa$.

(1) If $sa = b \in \mathbb{V}_{k-1}$, then $[[a]]_k = \mathbb{Y}_{[[b]]_{k-1}} = \mathbb{Y}_{[[f(b)]]_{k-1}} = [[f(a)]]_k$.

(2) If $sa = \underline{b}$ for some $b \in \mathbb{V}_{k-2}$, then $[[a]]_k = \mathbb{I}_{[[b]]_{k-2}} = \mathbb{I}_{[[f(b)]]_{k-2}} = [[f(a)]]_{k-2}$.

(3) If $sa = b(\overrightarrow{c_i \leftarrow u_i})$, then by induction, $[[u_i]]_k = [[f(u_i)]]_k$, and

$$[[a]]_k = \mathbb{Y}_{[[b]]_{k-1}} \bigcirc_{[[s_b c_i]]} [[u_i]]_k = [[f(a)]]_k.$$

□

**Definition 3.98.** Let $\mathcal{C}\mathcal{t}^!$ for the category of derivable OCMTs and such morphisms. In a sense, it is the syntactic category of system $\mathcal{OPT}\mathcal{SET}^!$.

**Definition 3.99** (Named stratification functor). The named stratification functor $S^! : \mathcal{C}\mathcal{t}^! \to \tilde{\mathbb{O}}_{\text{fin}}$ is defined as follows:

$$ \begin{gathered} S^! : \mathcal{C}\mathcal{t}^! \to \tilde{\mathbb{O}}_{\text{fin}} \\ (E \triangleright \Gamma) \mapsto \Gamma/E \\ \left( (E \triangleright \Gamma) \xrightarrow{f} (F \triangleright \Upsilon) \right) \mapsto \left( \Gamma/E \xrightarrow{S^!f} \Upsilon/F \right). \end{gathered} $$

**Proposition 3.100.** Let $f: (E \triangleright \Gamma) \rightarrow (F \triangleright \Upsilon)$ be a morphism of OCMTs. Then the map $S^!f$ of definition 3.99 is indeed a morphism of opetopic sets.

*Proof.* By definition, the cells of $\Gamma/E$ are exactly the variables of $\mathbb{V}_{\Gamma}$, and likewise for $\Upsilon/F$. By lemma 3.97, $S^!f$ preserves the shapes of the cells. By definition, if $x$ is an $n$-variable, and $x: X$ a typing in $\Gamma$, then $f(x): f(X)$ is a typing in $\Upsilon$. So, for $\omega := [[x]]_n$ and $[p] \in \omega^\bullet$, the following naturality square commutes:

$$ \begin{tikzcd} (\Gamma/E)_{\omega} \arrow[r, "S^!f_\omega"] \arrow[d, "s_{[p]}"] & (\Upsilon/F)_\omega \arrow[d, "s_{[p]}"] \\ (\Gamma/E)_{s_{[p]}\omega} \arrow[r, "S^!f_{s_{[p]}\omega}"] & (\Upsilon/F)_{s_{[p]}\omega}. \end{tikzcd} $$

By definition again, if $n \ge 1$, then $f(t \cdot x) = t f(x)$, so the analogous naturality square for target embeddings also commutes. Finally, $S^!f$ is a natural transformation. □

**Theorem 3.101.** *The stratification functor $S^! : \mathcal{C}\mathcal{t}^! \to \tilde{\mathbb{O}}_{\text{fin}}$ is an equivalence of categories.*
**Proof.** The full subcategory of $\tilde{\mathbb{O}}_{\text{fin}}$ spanned by the essential image of $S^!$ contains all the representables opetopic sets (proposition 3.91), the initial object (since $S^!(\triangleright)$ is the opetopic set with no cell), and is closed under finite sums and quotients (definition 3.92). Thus it is finitely cocomplete, and equal to the whole category $\tilde{\mathbb{O}}_{\text{fin}}$, so $S^!$ is essentially surjective. By definition, $S^!$ is also faithful, and it remains to show that it is full.

Let $f : \Gamma/E \to \Upsilon/F$ be a morphism of opetopic sets. Then, in particular, it is a map between the set of cells of $\Gamma/E$ and $\Upsilon/F$. To prove that it is a morphism of OCMT, we show that $\Gamma[f(x)/x \mid x \in \mathbb{V}_\Gamma]$ (see notation 3.95) is a subcontext of $\Upsilon$ modulo $F$, i.e. that for every typing $x : X$ in $\Gamma$, for some $x \in \mathbb{V}_k$, the type of $f(x)$ in $\Upsilon$ is $f(X)$ modulo $F$. If $(E \triangleright \Gamma)$ is the empty OCMT, the result is trivial. Let $x : X$ be a typing in $\Gamma$, with $x \in \mathbb{V}_k$. Since $f$ is a morphism of opetopic sets, we have $f(x) \in \mathbb{V}_{\Upsilon,k}$, and

$$ \begin{align*} [[x]]_k &= x^\flat \\ &= f(x)^\flat \\ &= [[f(x)]]_k. \end{align*} \text{ in the opetopic set } \Gamma/E $$

We show that the type of $f(x)$ in $\Upsilon$ is $f(X)$ by induction on $k$.

(1) If $k=0$, then $X = \emptyset$. Since $f(x) \in \mathbb{V}_{\Upsilon,0}$, its type is necessarily $\emptyset = f(X)$, thus $f(x) : f(X)$ is a typing in $\Upsilon$.

(2) If $k=1$, then $X = (a \mapsto \emptyset)$, where $a = v_{[]} x$ in $\Gamma/E$, and since $f$ is a morphism of opetopic sets, $f(v_{[]} x) =_F v_{[]} f(x)$. Thus

$$ f(X) = (f(v_{[]} x) \mapsto \emptyset) =_F (v_{[]} f(x) \mapsto \emptyset), $$

the latter being the type of $f(x)$ in $\Upsilon$.

(3) Assume now that $k \ge 2$. The type of $x$ is $X = (sx \mapsto ssx \mapsto \dots \mapsto \emptyset)$, and by definition, the type of $tx$ is $Y := (ssx \mapsto \dots \mapsto \emptyset)$ (see equation (3.72)). By induction, the type of $f(tx)$ in $\Upsilon$ is $f(Y)$, and since $f(tx) =_F tf(x)$, and the type of the latter is $(sxf(x) \mapsto \dots \mapsto \emptyset)$, we have

$$ (f(ssx) \mapsto \dots \mapsto \emptyset) = f(Y) =_F (sxf(x) \mapsto \dots \mapsto \emptyset), $$

or in other words, $s^i f(x) =_F f(s^i x)$, for $2 \le i \le k$. It remains to show that the latter formula holds in the case $i=1$. Towards a contradiction, assume $s f(x) \neq_F f(sx)$. Then there exists $[p] \in [[x]]_k^\bullet = [[f(x)]]_k^\bullet$ such that $v_{[p]} f(x) \neq_F f(v_{[p]} x)$, which contradicts the fact that $f$ is a morphism of opetopic sets. Consequently, $s f(x) =_F f(sx)$, and $f(X)$ is the type of $f(x)$ in $\Upsilon$ modulo $F$.

Finally, the underlying map of $f : \Gamma/E \to \Upsilon/F$ is a morphism of OCMT, and $S^!$ is full. $\square$

If $\mathcal{C}$ and $\mathcal{D}$ are small categories with finite limits, let $\mathcal{L}_{\text{EX}}(\mathcal{C}, \mathcal{D})$ be the category of left exact (i.e. finite limit preserving) functors from $\mathcal{C}$ to $\mathcal{D}$ and natural transformations. We now formally state the fact that system $\text{OPTSET}^?$ describe opetopic sets.

**Theorem 3.102.** We have an equivalence $\tilde{\mathbb{O}} \simeq \mathcal{L}_{\text{EX}}((\mathcal{C}\text{tx}^!)^{\text{op}}, \text{Set})$.

**Proof.** This follows directly from theorem 3.101 and from the Gabriel–Ulmer duality [6] [17, theorem 8]. $\square$
**3.7 Examples** In this section, we give example derivations in system OPTSET'. For clarity, we do not repeat the type of previously typed variables in proof trees.

**Example 3.103.** The opetopic set

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

is derived as follows. First, we derive the cells $\alpha$, $g$, and $h$ as opetopes (i.e. in OPTSET') to obtain the following sequents:

$$ \vdash a : \emptyset, f : a \mapsto \emptyset, \alpha : f \mapsto a \mapsto \emptyset \vdash_2 \alpha : f \mapsto a \mapsto \emptyset $$

$$ \vdash c : \emptyset, g : c \mapsto \emptyset \vdash_1 g : c \mapsto \emptyset $$

$$ \vdash b : \emptyset, h : b \mapsto \emptyset \vdash_1 h : b \mapsto \emptyset $$

and applying the **repr** rule yields respectively:

$$ \vdash a : \emptyset, f : a \mapsto \emptyset, \alpha : f \mapsto a \mapsto \emptyset, tf : \emptyset, t\alpha : a \mapsto \emptyset, tt\alpha : \emptyset $$

$$ \vdash c : \emptyset, g : c \mapsto \emptyset, tg : \emptyset $$

$$ \vdash b : \emptyset, h : b \mapsto \emptyset, th : \emptyset $$

The proof tree then reads:

<figure><img src="image_62.png" /></figure>
**Example 3.104.** The opetopic set

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

is derived as follows. First, we derive the cells $\alpha$ and $\beta$ as opetopes to obtain the following sequents:

$$ \left( \begin{array}{l} a:\emptyset, b:\emptyset \\ \vdash \quad f:a\dashv\emptyset, g:a\dashv\emptyset \quad \vdash_2 \alpha:g(b\leftarrow f)\dashv a\dashv\emptyset, \\ \alpha:g(b\leftarrow f)\dashv a\dashv\emptyset \\ \\ a':\emptyset \\ \vdash \quad h:a'\dashv\emptyset \quad \vdash_2 \beta:h\dashv a'\dashv\emptyset, \\ \beta:h\dashv a'\dashv\emptyset \end{array} \right). $$

Applying the repr rule yields respectively:

$$ \left( \begin{array}{l} a:\emptyset, b:\emptyset, tf:\emptyset, tg:\emptyset, tt\alpha:\emptyset \\ b = tf, tg = tt\alpha \quad \vdash \quad f:a\dashv\emptyset, g:a\dashv\emptyset, t\alpha:a\dashv\emptyset, \\ \qquad \alpha:g(b\leftarrow f)\dashv a\dashv\emptyset \\ \\ a':\emptyset, th:\emptyset, tt\beta:\emptyset \\ th = tt\beta \quad \vdash \quad h:a'\dashv\emptyset, t\beta:a'\dashv\emptyset, \\ \qquad \beta:h\dashv a'\dashv\emptyset \end{array} \right). $$

The proof tree then reads:

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

Write $(E \vdash \Gamma)$ for the final OCMT of this proof tree. At the beginning of section 3.5, we gave a seemingly different OCMT for the same opetopic set:

$$ \left( \begin{array}{l} a:\emptyset, b:\emptyset, tf:\emptyset, tg:\emptyset, tt\alpha:\emptyset, \\ \phantom{a:\} th:\emptyset, tt\beta:\emptyset \\ b = tf, a = tg = tt\alpha = th = tt\beta \\ \phantom{b =} h = t\beta = t\alpha \\ \\ \vdash \quad f:a\dashv\emptyset, g:a\dashv\emptyset, t\alpha:a\dashv\emptyset, \\ \phantom{f:a\dashv\} h:a\dashv\emptyset, t\beta:a\dashv\emptyset, \\ \alpha:g(b\leftarrow f)\dashv a\dashv\emptyset, \beta:h\dashv a\dashv\emptyset \end{array} \right). $$
But this is $\alpha$-equivalent to $(E \triangleright \Gamma)$, as instances of $a'$ have been replaced by $a$, which are both equal according to the equational theory $E$.

**3.8 Python implementation** The system $OPTSET^1$ is implemented in the Python module `opetopy.NamedOpetopicSet` of [13]. The rules are represented by functions `repres` (since `repr` a Python standard function), `sum`, `glue`, and `zero`, and are further encapsulated in rule instance classes `Repr`, `Sum`, `Glue`, and `Zero`. We do not discuss the implementation, but we give an example derivation in figure 3.5.

<caption>Figure 3.5: Derivation of example 3.103 using `opetopy.NamedOpetopicSet`</caption>

```python
from opetopy.NamedOpetopicSet import *
# We first define all relevant variables using system OPT^1.
f = Shift(Point("a"), "f")
g = Shift(Point("c"), "g")
h = Shift(Point("b"), "h")
alpha = Shift(f, "alpha")
# We then take the sum of all the representables we need. Note that the new
#   → target variables added by the repr rule have "t" prepended to their name
#   → e.g. the target variable of f is "tf", while that of α is "talpha".
example_unglued = Sum(Sum(Repr(alpha), Repr(g)), Repr(h))
example = Glue(
    Glue(
        Glue(
            Glue(
                example_unglued, "a", "c"
            ), "b", "tf"
        ), "b", "tg"
    ), "a", "th"
), "g", "talpha")
```

**3.9 The mixed system for opetopic sets** The $OPTSET^1$ system, presented in section 3.5, suffers from the following drawback: derivations of opetopic sets start with instances of rules `zero` or `repr`, the latter requiring a full opetopic derivation in system $OPT^1$ (presented in section 3.1). This makes derivations somewhat unintuitive, since for an opetopic set $X \in \mathbb{O}$ written as

$$X = \frac{\sum_i O[\omega_i]}{\sim}$$

where $\sim$ represents some quotient, the opetopes $\omega_i$ have to be derived in $OPT^1$ first, then the `repr` rule has to be used on each one to produce the corresponding representables $O[\omega_i]$, and
only then can the sums and gluing be performed:

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

In this section, we present system $OPTSET_M^!$ (the $M$ standing for “mixed”) for opetopic sets, which does not depend on $OPT^!$, and allows to perform introductions of new cells, sums, and gluings in any sound order. This is done by introducing new cells along with all their targets, effectively rendering $OPTSET^!’$’s **repr** rule superfluous, and removing the “barrier” between $OPT^!$ and $OPTSET^!$ in the schema above.

### 3.9.1 Syntax
The syntax of system $OPTSET_M^!$ uses sequents from $OPT^!$ (see section 3.1) and OCMTs from $OPTSET^!$. Specifically, we use two types of judgments.

(1) “$E \triangleright \Gamma$”, stating that $E \triangleright \Gamma$ is a well formed OCMT.

(2) “$E \triangleright \Gamma \vdash t : T$”, stating that in the OCMT $E \triangleright \Gamma$, the term $t$ is well formed, and has type $T$. We may also write “$E \triangleright \Gamma \vdash_T t : T$” to emphasize that $t \in T_n$.

### 3.9.2 Inference rules
We present the inference rules of system $OPTSET_M^!$ in definition 3.105. It uses rules **point**, and **graft** from system $OPT^!$, and rules **zero**, **sum**, and **glue** from system $OPTSET^!$. Two new rules, **degen** and **pd**, will go from the first type of judgment to the second, by introducing degenerate terms and single variable terms respectively. In the other direction, rule **shift** is a variant of that of system $OPT^!$, and from $(E \triangleright \Gamma \vdash t : T)$, introduces a new cell having $t$ as source, along with all the necessary targets. It can be viewed as a fusion of $OPT^!’$'s **shift** rule and $OPTSET^!’$'s **repr** rule.
**Definition 3.105** (The OPTSET<sub>M</sub><sup>1</sup> system). *Introduction of points.* This rule introduces 0-cells, also called points. If $x \in \mathbb{V}_0$, then

$$ \xrightarrow{\quad} \text{point} $$

*Introduction of degenerate pasting diagrams.* This rule creates a new degenerate pasting diagram. If $x \in \mathbb{V}_{\Gamma,k}$, then

$$ \frac{E \triangleright \Gamma, x : X}{E \triangleright \Gamma, x : X \vdash_{k+1} \underline{x} : x \mapsto X} \text{degen} $$

*Introduction of non-degenerate pasting diagrams.* This rule creates a new non-degenerate pasting diagram consisting of a single cell. It can then be extended using the *graft* rule. If $x \in \mathbb{V}_{\Gamma,k}$, then

$$ \frac{E \triangleright \Gamma, x : X}{E \triangleright \Gamma, x : X \vdash_k x : X} \text{pd} $$

*Grafting.* This rule extends a previously derived non-degenerate pasting diagram by grafting a cell. With the same conditions as rule *graft* of system OPT<sup>1</sup> (see section 3.1), if $x \in \mathbb{V}_n$, $t \in \mathbb{T}_n$ is not degenerate, $a \in (st)^*$ is such that $sa = ssx$, then

$$ \frac{E \triangleright \Gamma \vdash_n t : s_1 \mapsto s_2 \mapsto \dots \quad F \triangleright \Upsilon, x : X}{G \triangleright \Gamma \cup \Upsilon \vdash_n t(a \leftarrow x) : s_1[\mathfrak{s}x/a] \mapsto s_2 \mapsto \dots} \text{graft} $$

where $G$ is the union of $E$, $F$, and potentially a set of additional equalities incurred by the substitution $s_1[\mathfrak{s}x/a]$ (definition 3.21). We also write *graft-a* to make explicit the fact that we grafted onto $a$.

*Shifting of pasting diagrams.* This rule takes a previously derived pasting diagram (degenerate or not), and introduces a new cell having this pasting diagram as source. It also introduces the targets of all its iterated sources, and extends the ambient equational theory with the required identities, in the same fashion as rule *repr* of definition 3.23. If $x \in \mathbb{V}_{n+1}$ is such that $x \notin \mathbb{V}_{\Gamma}$, then

$$ \frac{E \triangleright \Gamma \vdash_n t : T}{F \triangleright \Upsilon} \text{shift} $$

with

$$ \Upsilon := \Gamma \cup \{x : t \mapsto T\} \cup \{\mathfrak{t}^i x : \mathfrak{s}^{i+1} x \mapsto \mathfrak{s}^{i+2} x \mapsto \dots \mid 0 < i \le n\}, $$

where by convention, we let $\mathfrak{t}^0 x = x$, and $F$ is defined as follows:

(1) if $t$ is a degenerate term, say $t = \underline{a}$, then

$$ F := E \cup \{\mathfrak{t}^{i+2} x = \mathfrak{t}^i a \mid 0 \le i \le n-1\} \quad (3.106) $$

(2) if $t$ is not degenerate, say $t = y(\overline{z_i} \leftarrow \overline{u_i})$, for some $y \in \mathbb{V}_n$, $\overline{z_i} \in \mathbb{V}_{n-1}$, and $\overline{u_i} \in \mathbb{T}_n$, then

$$ \begin{align*} F &:= E \\ & \cup \{\mathfrak{t}^2 x = ty \mid \text{if } n \ge 1\} \\ & \cup \{ta = b \mid \text{for all } b \leftarrow a(\dots) \text{ occurring in } t\}. \end{align*} $$
**Zero.** This rules introduces the empty OCMT.

$$ \bar{\triangleright} \text{zero} $$

**Binary sums.** This rule takes two disjoint OCMTs (i.e. whose cells have different names), and produces their sum. If $\Gamma \cap \Upsilon = \emptyset$, then

$$ \frac{E \triangleright \Gamma \quad F \triangleright \Upsilon}{E, F \triangleright \Gamma, \Upsilon} \text{sum} $$

**Quotients.** This rule identifies two parallel cells in an opetopic set by extending the underlying equational theory. If $a, b \in \mathbb{V}_{\Gamma}$ are such that $sa =_E sb$ and $ta =_E tb$, then

$$ \frac{E \triangleright \Gamma}{E, a =_b b \triangleright \Gamma} \text{glue} $$

We also write $\text{glue}-(a=b)$ to make explicit that we added $a=b$ to the theory.

*Remark 3.107.* The **sum** and **zero** rules may be replaced by the following **usum** rule (unbiased sum) without changing the set of derivable OCMTs. For $k \ge 0$, and for $(E_1 \triangleright \Gamma_1), \dots, (E_k \triangleright \Gamma_k)$ OCMTs such that $\Gamma_i \cap \Gamma_j = \emptyset$ for all $i \ne j$, then

$$ \frac{E_1 \triangleright \Gamma_1 \quad \dots \quad E_k \triangleright \Gamma_k}{E_1, \dots, E_k \triangleright \Gamma_1, \dots, \Gamma_k} \text{ usum} $$

*Remark 3.108.* Akin to **OPT**¹ and **OPTSET**¹, in **OPTSET**¹ a sequent or an OCMT that is equivalent to a derivable one is itself derivable.

**3.10 Equivalence with opetopic sets** The aim of this section is to prove theorem 3.113, stating that system $\text{OPTSET}_M^!$ precisely derives opetopic sets, in the sense of theorems 3.101 and 3.102. In other words, we prove that the set of derivable OCMTs of systems $\text{OPTSET}_M^!$ and $\text{OPTSET}^!$ are the same. This is done by rewriting proof trees in $\text{OPTSET}^!$ to proof trees in $\text{OPTSET}_M^!$ (see proposition 3.110) and conversely (see proposition 3.112).

*Convention 3.109.* Throughout this section, the rules of systems $\text{OPT}^!$ and $\text{OPTSET}^!$ will be decorated by a prime, e.g. **shift**, in order to differentiate them from the rules of system $\text{OPTSET}_M^!$. Further, to make notations lighter and the demonstrations more graphical, we write proof trees as actual trees, whose nodes are decorated by rules, and edges by sequents or OCMTs. For instance, derivation of the arrow ■ (see example 3.65) in system $\text{OPT}^!$ is represented as on the left, or more concisely as on the right:

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

If no uncertainty arises, we leave the decoration of the edges implicit, as on the right.

**Proposition 3.110.** Every OCMT derivable in system $\text{OPTSET}^!$ is also derivable in system $\text{OPTSET}_M^!$.
*Proof.* Recall that a proof tree in system $OPTSET^!$ has the following structure:

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

meaning that it begins with derivations in system $OPT^!$, followed by instances of the *repr* rule, followed by a derivation in system $OPTSET^!$. Remark that rule *glue* is exactly *glue*, and likewise for *sum*, so that the bottom part of the proof tree is already a derivation in system $OPTSET_M^!$.

We now show that we can rewrite the top part to a proof in system $OPTSET_M^!$ by “moving up” the instances of rule *repr*, and replacing the other rule instances by those of $OPTSET_M^!$. This rewriting procedure is defined by the following cases.

(1) If we have a proof tree as on the left, we rewrite it as on the right:

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

(2) If we have a derivation as on the left, where $Π$ is a proof tree in system $OPT^!$ or $OPTSET^!$, then we rewrite it as on the right:

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

(3) If $k \ge 0$ and if we have a derivation as on the top, where $Π, Π_1, \dots, Π_k$ are proof trees in system $OPT^!$ or $OPTSET^!$, then we rewrite it as below:

<figure><img src="image_70.png" /></figure>
<figure><img src="image_71.png" /></figure>

Here, the new instances of **pd** pick the adequate variables from each sequent, so that they can be used by the instances of **graft**. Once the grafting process is complete, rule **shift** adds all necessary targets, which was previously done by **repr**'.

It is routine verification to check that the conclusion OCMT on the left and the right of any of those cases are the same. This rewriting procedure is terminating, and a normal form of a proof tree in system $OPTSET_M^!$ is a proof tree in system $OPTSET_M^!$ that derives the same OCMT. $\square$

**Lemma 3.111.** Let $(E \triangleright \Gamma)$ be a derivable OCMT in system $OPTSET_M^!$. Then it admits a proof tree of the following form

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

meaning a proof tree starting with a derivation in the fragment of system $OPTSET_M^!$ containing only rules **point**, **degen**, **pd**, **graft**, and **shift**, followed by a derivation in the complementary fragment.

*Proof.* If we have a proof tree consisting only of an instance of rule **zero**, then the result trivially holds. Otherwise, we proceed by stating rewriting steps of proof trees in system $OPTSET_M^!$, as in the proof of proposition 3.110.

(1) If we have a proof tree as on the left, and assuming the instance of **degen** degenerates a variable in $\Gamma_2$, we rewrite it as on the right:

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

(2) A proof tree as on the left is rewritten as on the right:

<figure><img src="image_74.png" /></figure>
(3) Consider a proof tree as on the top. Then, by assumption on rule **sum**, either $a_{i-1} \in \mathbb{V}_{\Gamma_1}$ or $a_{i-1} \in \mathbb{V}_{\Gamma_2}$. Without loss of generality, assume the latter holds. Then we rewrite the proof tree as below:

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

(4) Consider a proof tree as on the top, and rewrite it as below, $x$.

<figure><img src="image_76.png" /></figure>
<figure><img src="image_77.png" /></figure>

where in the dashed zone, for $i-1 \le j \le k-1$,

$$a'_{j} = \begin{cases} x & \text{if } a_j = y \\ a_j & \text{otherwise.} \end{cases}$$

In other words, the uses of $y$ in the dashed zone have been replaced by uses of $x$. $\square$

**Proposition 3.112.** Every OCMT derivable in system $OPTSET_M^!$ is also derivable in system $OPTSET^!$.

*Proof.* Consider a proof tree in system $OPTSET_M^!$. Then it can be rewritten so as to have the shape described in lemma 3.111. Applying the rewriting steps of proposition 3.110 in reverse order yields a proof tree in systems $OPT^!$ and $OPTSET^!$ that derives the same OCMT. $\square$

**Theorem 3.113.** The system $OPTSET_M^!$ derives opetopic sets in the sense of theorems 3.101 and 3.102.

*Proof.* By propositions 3.110 and 3.112, the OCMTs derived by system $OPTSET_M^!$ and $OPTSET^!$ are the same. $\square$

**3.11 Examples** In this section, we give example derivations in system $OPTSET_M^!$. For clarity, we do not repeat the type of previously typed variables in proof trees.

**Example 3.114.** The opetopic set

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

of example 3.103 can be derived as follows:
<figure><img src="image_79.png" /></figure>

where rules of the form $(x = y)$ are shorthands for $\text{glue-}(x = y)$.

**Example 3.115.** The opetopic set

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

of example 3.104 can be derived as follows.
<figure><img src="image_81.png" /></figure>

**3.12 Python implementation** The system OPTSET<sub>m</sub> is implemented in the Python module `opetopy.NamedOpetopicSet` of [13]. Its usage is very similar to `opetopy.NamedOpetope` and `opetopy.NamedOpetopicSet`, presented in sections 3.4 and 3.8 respectively.
<figure><img src="image_82.png" /><figcaption>Figure 3.6: Derivation of example example 3.103 using opetopy .NamedOpetopicSetM</figcaption></figure>

4. Unnamed approach

4.1 The system for opetopes The unnamed approach for opetopes relies on the calculus of higher addresses presented in section 2.2.3 to identify cells, rather than on names as in the named approach. For example, recall the opetope 3 ∈ O 2 from example 2.36, drawn on the left, with its underlying 3 $^{0}$-tree represented on the right:

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

In the unnamed approach for opetopes presented in this section, **3** will be encoded as a mapping
from its set of node addresses $\mathbf{3}^* = [[],[*],[**]]$ to the set of 1-opetopes $\mathcal{O}_1$ as follows:

<figure><img src="image_84.png" /></figure>
The 1-opetope $\bullet$ can recursively be encoded by $\{ * \leftarrow \diamond \}$, which gives a complete expression of 3:

$$ \left\{ \begin{array}{l} [[\quad] \leftarrow \{ * \leftarrow \diamond \} \\ [[*] \leftarrow \{ * \leftarrow \diamond \} \\ [[**] \leftarrow \{ * \leftarrow \diamond \} \end{array} \right. $$

This example will be treated in depth in example 4.36. In a similar manner, the opetope $\omega$ on the left, whose tree is given in the middle, can be encoded as on the right:

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

Similarly to 3, the opetope 2 can be expressed by $\{ [[\quad] \leftarrow \bullet \quad \}$, and recall that $\bullet$ can be expressed by $\{ * \leftarrow \diamond \}$. We thus have a complete encoding of $\omega$ as:

$$ \omega \quad \rightsquigarrow \quad \left\{ \begin{array}{l} [[\quad] \leftarrow \{ [[\quad] \leftarrow \{ * \leftarrow \diamond \} \quad \} \quad \} \quad \} \\ [[*] \leftarrow \{ * \leftarrow \diamond \} \\ [[**] \leftarrow \{ * \leftarrow \diamond \} \quad \} \quad \} \end{array} \right. $$

This example is fully treated in example 4.37.

### 4.1.1 Preopetopes

**Definition 4.1 (Preopetope).** The sets $\mathbb{P}_n$ of $n$-preopetopes are defined by the following grammar:

$$ \mathbb{P}_0 := \{ \diamond \} $$

$$ \mathbb{P}_n := \left\{ \begin{array}{l} \mathbb{A}_{n-1} \leftarrow \mathbb{P}_{n-1} \\ \vdots \\ \mathbb{A}_{n-1} \leftarrow \mathbb{P}_{n-1} \end{array} \right. \qquad n \ge 1 \qquad (4.2) $$

$$ \mid \{ \mathbb{P}_{n-2} \qquad n \ge 2 \qquad (4.3) $$

where the set $\mathbb{A}_n$ of $n$-addresses is defined in definition 2.38. In line (4.2), we require further that there is at least one $(n-1)$-address, and that all addresses are distinct.

An $n$-preopetope $\mathbf{p}$ is degenerate if it is of the form of line (4.3), it is non-degenerate otherwise. We write $\dim \mathbf{p} := n$ for its dimension.

**Convention 4.4.** An $n$-preopetope as in equation (4.2) is considered as a set of expressions $\mathbb{A}_{n-1} \leftarrow \mathbb{P}_{n-1}$ rather than a list. For instance, the following two $n$-preopetopes are equal

$$ \left\{ \begin{array}{l} [[p_1] \leftarrow \mathbf{p}_1 \\ [[p_2] \leftarrow \mathbf{p}_2 \end{array} \right. = \left\{ \begin{array}{l} [[p_2] \leftarrow \mathbf{p}_2 \\ [[p_1] \leftarrow \mathbf{p}_1 \end{array} \right. $$

for any distinct $(n-1)$-addresses $[p_1], [p_2] \in \mathbb{A}_{n-1}$, and any $\mathbf{p}_1, \mathbf{p}_2 \in \mathbb{P}_{n-1}$.
**Example 4.5.** (1) There is a unique 1-preopetope {$* \leftarrow \diamond$}, which we simply write ■.
(2) The following are examples of a 2 and 3-preopetope, respectively:

$$ \left\{ \begin{array}{l} [[\cdot] \leftarrow \{ * \leftarrow \diamond \\ [[**]] \leftarrow \{ * \leftarrow \diamond \} \end{array} \right. \qquad \left\{ \begin{array}{l} [[\cdot]] \leftarrow \{ \diamond \\ [[**][\cdot][\cdot]] \leftarrow \{ \cdot \leftarrow \diamond \} \end{array} \right. $$

We will see that the first does not correspond to an actual opetope, as it is impossible for a 2-opetope to only contain addresses $[]$ and $[* * * *]$ (it would at least need addresses $[*]$, $[**]$, $[* * ]$, and $[* * *]$). The second does not correspond to an opetope either, as it does not have a root node (corresponding to address $[]$).

(3) The following is a 4-preopetope $\{\{\{\diamond\} . \text{ We will see that it corresponds to } l_i, \in \mathbb{O}_4.\}$

(4) The following is not a valid preopetope:

$$ \left\{ \begin{array}{l} [[*]] \leftarrow \diamond \\ [[*][\cdot]] \leftarrow \{ * \leftarrow \diamond \} \end{array} \right. $$

as $\diamond$ and $\{ * \leftarrow \diamond$ do not have the same dimension.

**Definition 4.6.** If we have a non-degenerate $n$-preopetope of the form

$$ \mathbf{p} = \left\{ \begin{array}{l} [[p_1]] \leftarrow \mathbf{q}_1 \\ \vdots \\ [[p_k]] \leftarrow \mathbf{q}_k \end{array} \right. \qquad (4.7) $$

we call $[p_1], \dots, [p_k] \in \mathbb{A}_{n-1}$ the source addresses of $\mathbf{p}$ (or just sources), write $\mathbf{p}^\bullet$ for the set of source addresses of $\mathbf{p}$, and $\mathbf{s}_{[p_i]} \mathbf{p} := \mathbf{q}_i$ for the $[p_i]$-source of $\mathbf{p}$.

Assume $n \ge 2$. A leaf address (or just leaf) of $\mathbf{p}$ is an $(n-1)$-address of the form $[p[q]]$ such that $[p] \in \mathbf{p}^\bullet$, $[q] \in (\mathbf{s}_{[p]} \mathbf{p})^\bullet$, and such that for all $[r] \in \mathbf{p}^\bullet$, $[p[q]] \notin [r]$. In other words, $[p[q]]$ is not a prefix of any node address of $\mathbf{p}$, and in particular $[p[q]] \notin \mathbf{p}^\bullet$. We write $\mathbf{p}^\prime \subseteq \mathbb{A}_{n-1}$ for the set of leaf addresses of $\mathbf{p}$. By convention, if $\mathbf{p}$ is degenerate, then $\mathbf{p}^\bullet := \emptyset$ and $\mathbf{p}^\prime := \{[]\}$. Further, $\mathbf{p}^\bullet = \mathbf{p}^\prime := \emptyset$.

**Example 4.8.** Consider the following preopetopes

$$ \mathbf{p} := \left\{ \begin{array}{l} [[\cdot] \leftarrow \{ \cdot \leftarrow \diamond \\ [[\cdot]] \leftarrow \{ * \leftarrow \diamond \\ [[*]] \leftarrow \{ \cdot \leftarrow \diamond \} \end{array} \right. \qquad \mathbf{q} := \left\{ \begin{array}{l} [[\cdot] \leftarrow \{ \cdot \leftarrow \diamond \\ [[\cdot]] \leftarrow \{ \diamond \} \end{array} \right. $$

Then $\mathbf{p}^\bullet = \{[]$, $[[*]]\}$, $\mathbf{p}^\prime = \{[[\cdot]], [[*][\cdot]], [[*][\cdot][\cdot]]\}$, $\mathbf{q}^\bullet = \{[]$, $[[\cdot]]\}$, and $\mathbf{q}^\prime = \emptyset$.

**Definition 4.9** (Corolla grafting). Let $n \ge 1$, $\mathbf{p} \in \mathbb{P}_n$ be as in equation (4.7), and $\mathbf{q} \in \mathbb{P}_{n-1}$. For $[l] \in \mathbf{p}^\prime$ a leaf address of $\mathbf{p}$ (so in particular $[l] \notin \mathbf{p}^\bullet$), write

$$ \mathbf{p}_{[l]} \tilde{\mathbf{q}} := \left\{ \begin{array}{l} [[p_1]] \leftarrow \mathbf{q}_1 \\ \vdots \\ [[p_k]] \leftarrow \mathbf{q}_k \\ [l] \leftarrow \mathbf{q} \end{array} \right. $$

and call $\mathbf{p}_{[l]} \tilde{\mathbf{q}}$ the corolla grafting of $\mathbf{q}$ on $\mathbf{p}$ at address $[l]$. By convention, this operation is associative on the right.
**Example 4.15.** The following is a sequent:

$$ \frac{[[]], [[*]][] , [[*][*]] [**]}{[]}, \quad \left\{ \begin{array}{l} [] \leftarrow \begin{cases} [] \leftarrow \{* \leftarrow \bullet \\ [*] \leftarrow \{* \leftarrow \bullet \end{cases} \\ [[*]] \leftarrow \begin{cases} [] \leftarrow \{* \leftarrow \bullet \\ [*] \leftarrow \{* \leftarrow \bullet \end{cases} \end{array} \right. \rightarrow \begin{array}{l} [] \leftarrow \{* \leftarrow \bullet \\ [*] \leftarrow \{* \leftarrow \bullet \\ [**] \leftarrow \{* \leftarrow \bullet \end{array} $$

As we will see in example 4.37, it describes the following 3-opetope:

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

The operation of *substitution* (definitions 2.19 and 3.21), which consists in replacing a node by a pasting diagram in an opetope, can be defined as follows in our formalism.

**Definition 4.16 (Substitution).** Let $\mathbf{t}, \mathbf{q} \in \mathbb{P}_n$, $\Upsilon \vdash \mathbf{q} \rightarrow \mathbf{u}$ be a sequent. Write $\mathbf{t}$ as

$$ \mathbf{t} = \begin{cases} [t_1] \leftarrow \mathbf{w}_1 \\ \vdots \\ [t_l] \leftarrow \mathbf{w}_l \end{cases} $$

For $[t_i] \in \mathbf{t}^*$, we define $\mathbf{t} \sqcap_{[t_i]} \mathbf{q}$, the *substitution* by $\mathbf{q}$ in $\mathbf{t}$ at $[t_i]$, as follows:

(1) if $l=1$ and $\mathbf{q}$ is degenerate, then $\mathbf{t} \sqcap_{[t_1]} \mathbf{q} := \mathbf{q}$;

(2) if $l \ge 2$ and $\mathbf{q}$ is degenerate, then

$$ \mathbf{t} \sqcap_{[t_i]} \mathbf{q} := \left\{ \begin{array}{ll} \rho[t_1] \leftarrow \mathbf{w}_1 & \\ \vdots & \\ \rho[t_{i-1}] \leftarrow \mathbf{w}_{i-1} & \text{where } \rho[t_j] := \begin{cases} [t_i r] & \text{if } [t_j] = [t_i [] r], \\ [t_j] & \text{otherwise.} \end{cases} \\ \\ \rho[t_{i+1}] \leftarrow \mathbf{w}_{i+1} & \\ \vdots & \\ \rho[t_l] \leftarrow \mathbf{w}_l & \end{array} \right. $$

(3) if $l \ge 2$, and $\mathbf{q}$ is not degenerate, write it as

$$ \mathbf{q} = \begin{cases} [q_1] \leftarrow \mathbf{v}_1 \\ \vdots \\ [q_k] \leftarrow \mathbf{v}_k \end{cases} $$

and define

$$ \mathbf{t} \sqcap_{[t_i]} \mathbf{q} := \left\{ \begin{array}{ll} \rho[t_1] \leftarrow \mathbf{w}_1 & \\ \vdots & \\ \rho[t_{i-1}] \leftarrow \mathbf{w}_{i-1} & \\ [t_i q_1] \leftarrow \mathbf{v}_1 & \\ \vdots & \\ [t_i q_k] \leftarrow \mathbf{v}_k & \text{where } \rho[t_j] := \begin{cases} [t_i a r] & \text{if } [t_j] = [t_i [] r] \\ [t_j] & \text{for some } \frac{[a]}{[b]} \in \Upsilon, \\ \end{cases} \\ \\ \rho[t_{i+1}] \leftarrow \mathbf{w}_{i+1} & \\ \vdots & \\ \rho[t_l] \leftarrow \mathbf{w}_l & \end{array} \right. $$

This operation relies on the context $\Upsilon$, which we leave implicit. By convention, $\sqcap$ is associative on the left.

We refer to section 4.3 for examples of applications of this construction. We now state the inference rules of our unnamed system OPT$^?$ in definition 4.17.
**Definition 4.17** (The OPT? system).

*Introduction of points.*

$$ \vdash \diamond \to \emptyset \text{ point} $$

*Introduction of degeneracies.*

$$ \frac{\Gamma \vdash \mathbf{p} \to \mathbf{t}}{\begin{bmatrix} \end{bmatrix} \vdash \{\{\mathbf{p} \to \{\begin{bmatrix} \end{bmatrix} \leftarrow \mathbf{p}\}\} \} \text{degen}} $$

Note that $\dim(\{\{\mathbf{p}\} = 2 + \dim \mathbf{p}\}, \text{and that } \dim(\{\begin{bmatrix} \end{bmatrix} \leftarrow \mathbf{p}) = 1 + \dim \mathbf{p}.$
*Shift to the next dimension.* Write $\mathbf{p}^{\bullet} = \{[p_1], \dots, [p_k]\}$.

$$ \frac{\Gamma \vdash \mathbf{p} \to \mathbf{t}}{\begin{bmatrix} \end{bmatrix} \vdash \{\{\begin{bmatrix} \end{bmatrix} \vdash \mathbf{p} \to \mathbf{p}\}\} \text{shift}} $$

As in the previous rule, $\dim(\{\begin{bmatrix} \end{bmatrix} \leftarrow \mathbf{p}) = 1 + \dim \mathbf{p}.$
*Grafting.* Assume $\dim \mathbf{p} = n \ge 2$, $[p[q]] \in \mathbf{p}^{\bullet}$, $\dim \mathbf{q} = n - 1$, write $\mathbf{u} := \mathbf{s}_{[q]} \mathbf{s}_{[p]} \mathbf{p}$ and $\mathbf{q}^{\bullet} = \{[s_1], \dots, [s_l]\}$.

$$ \frac{\Gamma, \frac{[p[q]]}{[r]} \vdash \mathbf{p} \to \mathbf{t} \quad \Upsilon \vdash \mathbf{q} \to \mathbf{u}}{\Gamma', \frac{[p[q][s_1]]}{[rs_1]}, \dots, \frac{[p[q][s_l]]}{[rs_l]} \vdash \mathbf{p} \xrightarrow{\tilde{\omega}} \mathbf{q} \to \mathbf{t} \quad \begin{array}{c} \square \\ [r] \end{array} \mathbf{q}} \text{graft} $$

where $\Gamma'$ is given by pairs of the form

(1) $\frac{[a]}{[rxr']}$, where $\frac{[a]}{[r[y]r']}$ $\in \Gamma$ and $\frac{[x]}{[y]} \in \Upsilon$,

(2) $\frac{[a]}{[b]}$, where $\frac{[a]}{[b]} \in \Gamma$ is not as above (i.e. $[b]$ not of the form $[r[y]r']$ for some $\frac{[x]}{[y]} \in \Upsilon$).

In large derivation trees, we will sometimes refer to this rule as *graft-* `[p[q]]` for clarity, or simply as `[p[q]]` in order to make notations lighter.

**Remark 4.18.** Let us explain the transformation of context defined in rule *graft* in definition 4.17. Take a derivable sequent in OPT?, say

$$ \Gamma \vdash \mathbf{p} \to \mathbf{t}, $$

with $\mathbf{p} \in \mathbb{P}_n$. It will be proved in lemma 4.20 that $\Gamma$ exhibits a bijection between $\mathbf{p}^{\bullet}$ and $\mathbf{t}^{\bullet}$. Further, in theorem 4.34, we will see that $\mathbf{p}$ corresponds uniquely to an $n$-opetope $\omega = [[\mathbf{p}]]$, that $\mathbf{t}\omega = [[\mathbf{t}]]$, and that $\Gamma$ corresponds to the readdressing function $\wp_{\omega} : \omega^{\bullet} \to (\mathbf{t}\omega)^{\bullet}$ or definition 2.27.

But where is the readdressing map $\wp_{\omega}$ implemented in OPT? Applying theorem 3.64, we know that $\omega$ corresponds to a unique sequent (modulo $\alpha$-equivalence), say

$$ E \triangleright \Upsilon \vdash x : s_1 \dashv s_2 \dashv \dots \dashv \emptyset $$

where $x \in \mathbb{V}_n$. More precisely, considered as a tree, $\omega$ is encoded by the term $s_1$, and by proposition 3.53, $\mathbf{t}\omega$ is encoded by $s_2$. In lemma 3.51, we show that $\wp_{\omega}$ exhibits a bijection

$$ \{\&_{s_1} b \mid b \in s_2^{\bullet}\} \xrightarrow{\wp_{\omega}} \{\&_{s_2} b \mid b \in s_2^{\bullet}\}. $$
Say that a *node* of the term $s_2$ is a $(n-2)$-variable $b \in s_2^\bullet$, while a *leaf* of $s_1$ is a variable that can be used for grafting (see rule *graft* in definition 3.23), i.e. also a $(n-2)$-variable $b \in s_2^\bullet$. Then the left hand side can be considered as the set of leaf addresses of $s_1$, while the right hand side is its set of node addresses of $s_2$, and $\wp_\omega$ maps the address of $b \in \mathbb{V}_{n-2}$ as a leaf of $s_1$ to the address of $b$ as a node of $s_2$. But in $\text{OPT}^1$, the function $\wp_\omega$ is unnecessary, as this correspondence is already established by the name of the variables.

In $\text{OPT}^2$ however, such bookkeeping is necessary since there are no names, and $\Gamma$ is designed to precisely be the desired correspondence.

We now prove basic properties of derivable sequents in $\text{OPT}^2$. In proof trees, we may sometimes omit irrelevant information. For instance, if contexts and targets are not important, the *shift* rule may be written as

$$ \frac{\mathbf{p}}{\{ \emptyset \leftarrow \mathbf{p} } \text{shift} $$

**Lemma 4.19.** If $\Gamma \vdash \mathbf{p} \rightarrow \mathbf{t}$ is a derivable sequent, then $\dim \mathbf{p} = 1 + \dim \mathbf{t}$.

*Proof.* Easy induction on proof trees. $\square$

**Lemma 4.20.** Let $\Gamma \vdash \mathbf{p} \rightarrow \mathbf{t}$ be a derivable sequent with $\dim \mathbf{p} \ge 2$. Then $\Gamma$ establishes a bijection between $\mathbf{p}^1$ and $\mathbf{t}^\bullet$ (i.e. as a set of pairs, $\Gamma$ is the graph of a bijective function).

*Proof.* The fact that $\Gamma$ is a relation from $\mathbf{p}^1$ to $\mathbf{t}^\bullet$ (i.e. that whenever $\frac{[a]}{[b]} \in \Gamma$ we have $[a] \in \mathbf{p}^1$ and $[b] \in \mathbf{t}^\bullet$) is clear from the inference rules. It is also clear that $\Gamma$ is a function (i.e. that whenever $\frac{[a]}{[b]}$, $\frac{[a']}{[b']} \in \Gamma$ if $[b] \neq [b']$, then $[a] \neq [a']$). Finally, the fact that it is a bijection is clear in the case of *degen* and *shift*, and follows from lemma 4.13 in the case of *graft*. $\square$

**Lemma 4.21.** Let $\Gamma \vdash \mathbf{p} \rightarrow \mathbf{t}$ be a derivable sequent with $\dim \mathbf{p} \ge 2$ non-degenerate. For $\frac{[p[q]]}{[r]} \in \Gamma$, we have $s_{[q]} s_{[p]} \mathbf{p} = s_{[r]} \mathbf{t}$.

*Proof.* The sequent necessarily follows from an instance of *shift* or *graft*. The result is clear for the former, and follows from inspection for the latter. $\square$

**Proposition 4.22.** If $\Gamma \vdash \mathbf{p} \rightarrow \mathbf{t}$ is derivable, then so is $\mathbf{t}$, i.e. there exists a derivable sequent of the form $\Upsilon \vdash \mathbf{t} \rightarrow \mathbf{u}$.

*Proof.* The only non obvious case is (as always) *graft*, where we have to show that $\mathbf{t} \sqcap_{[r]} \mathbf{q}$ is derivable. Since the sequent $\Gamma, \frac{[p[q]]}{[r]} \vdash \mathbf{p} \rightarrow \mathbf{t}$ has a nonempty context, $\mathbf{p}$ and $\mathbf{t}$ are non-degenerate. Write $\mathbf{t}$ and $\mathbf{q}$ as in definition 4.16. Up to reindexing, we may assume that $\rho[t_j] = [t_j]$ if and only if $j < i$. Assume moreover that the sequences $[t_1], \dots, [t_{i-1}]$ and $[t_{i+1}], \dots, [t_l]$ are both lexicographically sorted. In particular, $[t_1] = []$. For $j > i$ write $[t_j] = [t_i[b_j]x_j]$ and $\wp[t_j] = [t_i a_j x_j]$, so that $\Upsilon = \{\frac{[a_j]}{[b_j]} | i < j \le l\}$. Then the proof tree of $\mathbf{t} \sqcap_{[t_i]} \mathbf{q}$ is sketched as follows.

(1) If $[t_i] = []$, then necessarily $i = 1$, and $\mathbf{t} \sqcap_{[t_i]} \mathbf{q}$ can be derived as
Assume $n \ge 2$, that $C^?$ is defined for all $k < n$, and take $\omega \in \mathbb{O}_n$.

(1) If $\omega$ is degenerate, say $\omega = I_\phi$ for some $\phi \in \mathbb{O}_{n-2}$, then

$$C^? (I_\phi) := \{\{C^? (\phi)\}.$$

(2) If $\omega$ is an endotope, say $\omega = Y_\psi$ for some $\psi \in \mathbb{O}_{n-1}$, then

$$C^? (Y_\psi) := \{[] \leftarrow C^? (\psi)\}.$$

(3) Otherwise, decompose $\omega$ as $\omega = \nu \circ_{[l]} Y_\psi$, for $\nu \in \mathbb{O}_n$, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu^1$, and let

$$C^? (\omega) := C^? (\nu) \tilde{\circ}_{[l]} C^? (\psi).$$

This grafting is well-defined by lemma 4.28 applied inductively to $\nu$.

**Proposition 4.27.** Let $n \ge 2$ and $\omega \in \mathbb{O}_n$ have at least three nodes. Then the preopetope $C^? (\omega)$ does not depend on the decomposition of $\omega$ in corollas.

*Proof.* Akin to proposition 3.62, it is enough to check that for $\nu \in \mathbb{O}_n$ non-degenerate, two different leaf addresses $[l]$, $[l'] \in \nu^1$ (which are necessarily $\sqsubseteq$-incomparable), and $\psi, \psi' \in \mathbb{O}_{n-1}$ such that $t\psi = e_{[l]}\nu$ and $t\psi' = e_{[l']}\nu$, we have

$$C^? \left( (\nu \circ_{[l]} Y_\psi) \circ_{[l']} Y_{\psi'} \right) = C^? \left( (\nu \circ_{[l']} Y_{\psi'}) \circ_{[l]} Y_\psi \right).$$

To unclutter notations, write $C^? (\nu) = \{\cdot\}$. We have

$$
\begin{align*}
C^? \left( (\nu \circ_{[l]} Y_\psi) \circ_{[l']} Y_{\psi'} \right) \\
&= C^? \left( \nu \circ_{[l]} Y_\psi \right) \tilde{\circ}_{[l']} C^? (\psi') && \text{by definition} \\
&= \left( C^? (\nu) \tilde{\circ}_{[l]} C^? (\psi) \right) \tilde{\circ}_{[l']} C^? (\psi') && \text{by definition} \\
&= \left( \begin{array}{c} \vdots \\ [l] \leftarrow C^? (\psi) \end{array} \right) \tilde{\circ}_{[l']} C^? (\psi') && \text{see definition 4.9} \\
&= \left\{ \begin{array}{c} \vdots \\ [l] \leftarrow C^? (\psi) \\ [l'] \leftarrow C^? (\psi') \end{array} \right. && \text{see definition 4.9} \\
&= \left\{ \begin{array}{c} \vdots \\ [l'] \leftarrow C^? (\psi') \\ [l] \leftarrow C^? (\psi) \end{array} \right. && \text{see convention 4.4} \\
&= \left( \begin{array}{c} \vdots \\ [l'] \leftarrow C^? (\psi') \end{array} \right) \tilde{\circ}_{[l]} C^? (\psi) && \text{since } [l] \notin [l'] \\
&= \left( C^? (\nu) \tilde{\circ}_{[l']} C^? (\psi') \right) \tilde{\circ}_{[l]} C^? (\psi) \\
&= C^? \left( (\nu \circ_{[l']} Y_{\psi'}) \circ_{[l]} Y_\psi \right).
\end{align*}
$$

□
We now establish a series of results to prove proposition 4.31 stating that $C^?(\omega)$ is always a derivable preopetope.

**Lemma 4.28.** For $\omega \in \mathbb{O}_n$, we have $\omega^\bullet = C^?(\omega)^\bullet$, and $\omega^1 = C^?(\omega)^1$.

*Proof.* We proceed by induction.

(1) If $n \le 1$, then the claims trivially hold.

(2) Assume $\omega = \mathbf{l}_\phi$, for some $\phi \in \mathbb{O}_{n-2}$. Then $\omega^\bullet = \emptyset = (\{C^?(\phi)\}^\bullet)$. For leaves, $\omega^1 = \{[]\} = (\{C^?(\phi)\}^1) = C^?(\omega)^1$ (see definition 4.6).

(3) Assume $\omega = \mathbf{Y}_\psi$, for some $\psi \in \mathbb{O}_{n-1}$, so that we have $C^?(\omega) = \{[] \leftarrow C^?(\psi)\}$. Then $\omega^\bullet = \{[]\} = (\{[] \leftarrow C^?(\psi)\}^\bullet = C^?(\omega)^\bullet$. By induction, $\psi^\bullet = C^?(\psi)^\bullet$, so the leaf addresses of $\omega$ and $\{[] \leftarrow C^?(\psi)$ are both of the form $[[q]]$, where $[q]$ ranges over $\psi^\bullet$, hence $\omega^1 = C^?(\omega)^1$.

(4) Assume $\omega = \nu \circ_{[l]} \mathbf{Y}_\psi$, for some $\nu \in \mathbb{O}_n$, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu^1$. Then, by induction,

$$ 
\begin{align*}
\omega^{\bullet} &= \nu^{\bullet} + \{[l]\} & \text{by definition} \\
&= C^{?}(\nu)^{\bullet} + \{[l]\} & \text{by induction} \\
&= \left( C^{?}(\nu) \tilde{\circ}_{[l]} C^{?}(\psi) \right)^{\bullet} & \text{see definition 4.9} \\
&= C^{?}(\omega)^{\bullet} & \text{see definition 4.26,}
\end{align*}
$$

and

$$ 
\begin{align*}
\omega^1 &= \nu^1 - \{[l]\} + \{[l[q]] \mid [q] \in \psi^\bullet\} & \text{by definition} \\
&= C^?(\nu)^1 - \{[l]\} + \{[l[q]] \mid [q] \in C^?(\psi)^\bullet\} & \text{by induction} \\
&= \left( C^?(\nu) \tilde{\circ}_{[l]} C^?(\psi) \right)^1 & \text{see definition 4.9} \\
&= C^?(\omega)^1 & \text{see definition 4.26.}
\end{align*}
$$

□

**Lemma 4.29.** For $\omega \in \mathbb{O}_n$ non-degenerate and $[p] \in \omega^\bullet$, we have $C^?(\mathbf{s}_{[p]})\omega = \mathbf{s}_{[p]} C^?(\omega)$.

*Proof.* We proceed by induction. Since $\omega^\bullet \neq \emptyset$, $\omega$ is either ■, an endotope, or a grafting.

(1) If $\omega = \blacksquare$, then $[p] = \blacksquare$, and trivially, $C^?(\mathbf{s}_\blacksquare) = C^?(\blacksquare) = \blacksquare = \mathbf{s}_\blacksquare \{\blacksquare \leftarrow \blacksquare = \mathbf{s}_\blacksquare C^?(\blacksquare)\}$.

(2) Assume that $\omega$ is an endotope, say $\omega = \mathbf{Y}_\psi$, for some $\psi \in \mathbb{O}_{n-1}$. Necessarily, $[p] = []$, and $C^?(\mathbf{s}_{[l]}\omega) = C^?(\psi) = \mathbf{s}_{[l]}\{[] \leftarrow C^?(\psi) = \mathbf{s}_{[l]} C^?(\omega)\}$.

(3) Assume $\omega = \nu \circ_{[l]} \mathbf{Y}_\psi$, for some $\nu \in \mathbb{O}_n$, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu^1$. Let $[p] \in \omega^\bullet$. If $[p] = [l]$, then

$$ 
\begin{align*}
C^?(\mathbf{s}_{[l]}\omega) &= C^?(\psi) \\
&= \mathbf{s}_{[l]}\left( C^?(\nu) \tilde{\circ}_{[l]} C^?(\psi) \right) & \text{see definition 4.9} \\
&= \mathbf{s}_{[l]} C^?(\omega) & \text{see definition 4.26.}
\end{align*}
$$
Otherwise, we have

$$
\begin{align*}
C^? (\mathfrak{s}_{[p]} \omega) &= C^? (\mathfrak{s}_{[p]} \nu) \\
&= \mathfrak{s}_{[p]} C^? (\nu) && \text{by induction} \\
&= \mathfrak{s}_{[p]} \left( C^? (\nu) \tilde{\circ}_{[l]} C^? (\psi) \right) && \text{see definition 4.9} \\
&= \mathfrak{s}_{[p]} C^? (\omega) && \text{see definition 4.26.}
\end{align*}
$$

□

**Lemma 4.30.** Let $\omega \in \mathbb{O}_n$, and assume that $C^? (\omega)$ is derivable. Then $C^? (t\omega) = tC^? (\omega)$, and $\wp_\omega = \wp_{C^? (\omega)}$ (see notation 4.24).

*Proof.* We proceed by induction.

(1) Assume $\omega = I_\phi$, for some $\phi \in \mathbb{O}_{n-2}$. Then

$$
\begin{align*}
C^? (t\omega) &= C^? (Y_\phi) \\
&= \{[] \leftarrow C^? (\phi) \} && \text{see definition 4.26} \\
&= t \{\{C^? (\phi)\} \} && \text{see degen rule} \\
&= t C^? (\omega) && \text{see definition 4.26.}
\end{align*}
$$

Since $\omega$ and $C^? (\omega)$ are both degenerate (as opetope and preopetope, respectively), $\wp_\omega$ and $\wp_{C^? (\omega)}$ both map $[] \in \omega^1 = C^? (\omega)^1$ to $[] \in (t\omega)^\bullet = tC^? (\omega)^\bullet$ (see the **degen** rule).

(2) Assume $\omega = Y_\psi$, for some $\psi \in \mathbb{O}_{n-1}$, so that we have $C^? (\omega) = \{[] \leftarrow C^? (\psi)$. Then

$$
\begin{align*}
C^? (t\omega) &= C^? (\psi) \\
&= t \{[] \leftarrow C^? (\psi)\} && \text{see shift rule} \\
&= t C^? (\omega) && \text{see definition 4.26.}
\end{align*}
$$

Moreover, we have $\omega^1 = C^? (\omega)^1 = \{ [[p]] | [p] \in \psi^\bullet \}$, and by definition, $\wp_\omega [[p]] = [p] = \wp_{C^? (\omega)} [p]$ (see the **shift rule**).

(3) Assume $\omega = \nu \circ_{[l]} Y_\psi$, for some $\nu \in \mathbb{O}_n$, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu^1$. Then,

$$
\begin{align*}
C^? (t\omega) &= C^? \left( (t\nu) \underset{\wp_\nu [l]}{\sqcap} \psi \right) && \text{by proposition 2.37} \\
&= C^? (t\nu) \underset{\wp_{C^? (\nu)} [l]}{\sqcap} C^? (\psi) && \text{by induction, } \wp_\nu = \wp_{C^? (\nu)} \\
&= t C^? (\nu) \underset{\wp_{C^? (\nu)} [l]}{\sqcap} C^? (\psi) && \text{by induction} \\
&= t \left( C^? (\nu) \tilde{\circ}_{[l]} C^? (\psi) \right) && \text{see graft rule} \\
&= t C^? (\omega)
\end{align*}
$$

The equality $\wp_\omega = \wp_{C^? (\omega)}$ follows by inspection of rule **graft**.

□

**Proposition 4.31.** If $\omega \in \mathbb{O}_n$, then $C^? (\omega)$ is a derivable $n$-preopetope.

*Proof.* If $n \le 1$, then the result is trivial, so assume that $n \ge 2$.
(1) If $\omega = l_{\phi}$ for some $\phi \in \mathbb{O}_{n-2}$, then $C^?(\omega)$ is simply obtained by an instance of **degen**:

$$ \frac{C^?(\phi)}{C^?(\omega)} \text{degen} $$

(2) Likewise, if $\omega = Y_{\psi}$ for some $\psi \in \mathbb{O}_{n-1}$, then $C^?(\omega)$ can be obtained using an instance of **shift**.

(3) Assume that $\omega = \nu \circ_{[l]} Y_{\psi}$, for $\nu \mathbb{O}_n$ non-degenerate, $\psi \in \mathbb{O}_{n-1}$, and $[l] \in \nu^1$. By lemma 4.28, $\nu^1 = C^?(\nu)^1$, thus $[l] \in C^?(\nu)^1$. Since $\nu$ is not degenerate, the leaf address $[l]$ can be decomposed as $[l] = [p[q]]$, where $[p] \in \nu^\bullet$ and $[q] \in (s_{[p]}\nu)^\bullet$. We have

$$ \begin{align*} s_{[q]} s_{[p]} C^?(\nu) &= s_{[q]} C^?(s_{[p]} \nu) & \text{by lemma 4.28} \\ &= C^?(s_{[q]} s_{[p]} \nu) & \text{by lemma 4.28} \\ &= C^?(t\psi) & \text{by assumption} \\ &= tC^?(\psi) & \text{by lemma 4.30} \end{align*} $$

Finally, rule **graft** can be used to derive $C^?(\omega)$:

$$ \frac{\begin{array}{c} \vdots \\ C^?(\nu) \end{array}}{C^?(\omega)} \text{graft-}[l] $$

□

We finally prove that $C^?$ is a bijection by constructing its inverse.

**Definition 4.32.** Define the polynomial coding function $\llbracket - \rrbracket : \mathbb{P}_n^? \to \mathbb{O}_n$ by induction on $n \in \mathbb{N}$. If $n = 0, 1$, then both sets are singletons, and $\llbracket - \rrbracket$ is trivially defined. Assume $n \ge 2$, and that $\llbracket - \rrbracket$ is defined for all $k < n$. We distinguish three cases.

(1) If $\mathbf{q} \in \mathbb{P}_{n-2}^?$, then $\llbracket \{\mathbf{q}\} \rrbracket := l_{[\mathbf{q}]}$.

(2) If $\mathbf{q} \in \mathbb{P}_{n-1}^?$, then $\llbracket \{\emptyset \leftarrow \mathbf{q}\} \rrbracket := Y_{[\mathbf{q}]}$.

(3) If $\mathbf{p} \in \mathbb{P}_n^?$, $\mathbf{q} \in \mathbb{P}_{n-1}^?$, and $[l] \in \mathbf{p}^1$ are such that the corresponding instance of rule **graft** is well-defined, then let

$$ \llbracket \mathbf{p} \tilde{\circ} \mathbf{q} \rrbracket := \llbracket \mathbf{p} \rrbracket \circ Y_{[\mathbf{q}]}, $$

which is well-defined by lemmas 4.28 to 4.30, and inductively applying theorem 4.34.

**Lemma 4.33.** Let $n \ge 1$ and $\mathbf{p} \in \mathbb{P}_n^?$ have at least three node addresses. Then $\llbracket \mathbf{p} \rrbracket$ does not depend on the decomposition of $\mathbf{p}$ into corolla graftings.

*Proof.* Akin to propositions 3.62 and 4.27, it is enough to check that for $\mathbf{p} \in \mathbb{P}_n^?$ non-degenerate, $[l], [l'] \in \mathbf{p}^1$ distinct leaf addresses (in particular, they are $\sqsubseteq$-incomparable), $\mathbf{q}, \mathbf{q}' \in \mathbb{P}_{n-1}^?$ such that $t\mathbf{q} = e_{[l]}\mathbf{p}$ and $t\mathbf{q}' = e_{[l']}\mathbf{p}$, we have

$$ \llbracket (\mathbf{p} \tilde{\circ} [l]) \mathbf{q} \rrbracket \tilde{\circ} \mathbf{q}' \rrbracket = \llbracket (\mathbf{p} \tilde{\circ} [[l']]) \mathbf{q}' \rrbracket \tilde{\circ} [l] \rrbracket. $$
This is straightforward:

$$ \begin{aligned} \left[ \left( \mathbf{p}_{[[l]]} \tilde{\mathbf{q}}_{[[l']}] \right) \tilde{\mathbf{q}}'_{[[l']]} \right] &= \left( \left[ \mathbf{p} \right]_{[[l]]} \circ \mathbf{Y}_{[[\mathbf{q}]]} \right) \circ \mathbf{Y}_{[[\mathbf{q}']]} && \text{by definition} \\ &= \left( \left[ \mathbf{p} \right]_{[[l']]} \circ \mathbf{Y}_{[[\mathbf{q}']]} \right) \circ \mathbf{Y}_{[[\mathbf{q}]]} && \text{since } [[l]] \neq [[l']]] \\ &= \left[ \left( \mathbf{p}_{[[l']]} \tilde{\mathbf{q}}'_{[[l]]} \right) \tilde{\mathbf{q}}_{[[l]]} \right] && \text{by definition.} \end{aligned} $$

□

**Theorem 4.34.** The functions $C^?$ and $[[–]]$ are mutually inverse.

*Proof.* It is straightforward to check that $[[C^? (\omega)]] = \omega$ by induction on the dimension and the number of nodes of $\omega$, and that $C^? ([[\mathbf{p}]]) = \mathbf{p}$ by induction on the prooftree of $\mathbf{p}$. □

This concludes the inductive process started at definition 4.26.

**4.3 Examples** In this section, we give example derivations in system OPT$^?$.

**Example 4.35 (The arrow).** The unique 1-opetope $\blacksquare = \{ * \leftarrow \diamond \text{ is derived by}$

$$ \begin{array}{ccc} \vdash \diamond \rightarrow \emptyset & \text{point} \\ \vdash \{ * \leftarrow \diamond \rightarrow \diamond \} & \text{shift} \end{array} $$

**Example 4.36 (Opetopic integers).** The opetopic integer $\mathbf{n}$ (example 2.36) is represented on the left in the case $n = 0$, and on the right if $n \ge 1$:

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

The derivation of $\mathbf{0}$ is simply

$$ \frac{\text{\textbf{point}}}{\{ \mathbf{0} \} \vdash \{ \diamond \rightarrow \blacksquare \}} \text{degen} $$

whereas for $n \ge 1$, the opetope $\mathbf{n}$ is derived as
**4.4 Deciding opetopes** We now present in algorithm 4.1 the ISOPETOPE function that, given a preopetope $\omega \in \mathbb{P}$, decides if $\omega \in \mathbb{P}^{\surd}$, as proved in proposition 4.41. This algorithm tries to deconstruct $\omega$ by finding the last rule instance of its potential proof tree, and recursively checking the validity of the premises. We emphasize that this algorithm is extremely inefficient.

<caption>**Algorithm 4.1 Well formation algorithm**</caption>

1: **procedure** ISOPETOPE($\omega \in \mathbb{P}$) ▷ Returns a boolean
2:     **if** $\omega = \diamond$ **then**
3:         **return** true
4:     **else if** $\omega = \{\phi \}$ **then**
5:         **return** ISOPETOPE($\phi$)
6:     **else**
7:         **while** $\omega$ has an address of the form $[p[q]]$ **do**
8:             **if** $[p] \notin \omega^{\bullet}$ **or not** ISOPETOPE($s_{[p]}$ $\omega$) **then**
9:                 **return** false
10:             **else if** $[q] \notin (s_{[p]}$ $\omega)^{\bullet}$ **or not** ISOPETOPE($s_{[p[q]]}$ $\omega$) **then**
11:                 **return** false
12:             **else if** $t s_{[p]}$ $\omega \neq s_{[p[q]]}$ $\omega$ **then**
13:                 **return** false
14:             **else**
15:                 Remove address $[p[q]]$ from $\omega$
16:             **end if**
17:         **end while**
18:     **if** $\omega$ is of the form $\{[\psi] \}$ **then**
19:         **return** ISOPETOPE($\psi$)
20:     **else**
21:         **return** false
22:     **end if**
23: **end if**
24: **end procedure**

**Proposition 4.41.** For $\omega \in \mathbb{P}$, the execution `ISOPETOPE(\omega)` returns **true** if and only if $\omega \in \mathbb{P}^{\surd}$.

*Proof.* This algorithm tries to deconstruct the potential proof tree of $\omega$ in system `OPT^?`:

(1) condition at line (2) removes an instance of the **point** rule;

(2) condition at line (4) removes an instance of **degen**;

(3) each iteration of the **while** loop at line (7) removes an instance of **graft**;

(4) finally the condition at line (18) removes an instance of **shift**.

If the algorithm encounters an expression that is not the conclusion of any instance of any rule of `OPT^?`, it returns **false**. Otherwise, if all branches of the proof tree lead to $\diamond$, it returns **true**.

□

This algorithm is implemented in method `UnnamedOpetope.ProofTree` of package `opetopy` [13]. It is worth noting that deciding opetopes can also be achieved by enumerating the proof trees of `OPT^?`. In fact, this enumeration scheme applies to all derivation systems presented in this work.
**4.5 Python implementation** The derivation system OPT? and its syntax are implemented in opetopy.UnnamedOpetope of [13]. In particular, the four derivation rules are represented by functions of the same name: `point`, `degen`, `shift`, and `graft`. As an example, we review the implementation of `shift` in figure 4.1.

<figure><img src="image_88.png" /><figcaption>Figure 4.1: Implementation of OPT?’s shift rule in opetopy.UnnamedOpetope.shift</figcaption></figure>

To construct proof trees, those rules are further abstracted in classes Point, Degen, Shift, as well as Graft. We review the implementation of some examples in figures 4.2 to 4.4.
<figure><img src="image_89.png" /><figcaption>Figure 4.3: Derivation of some opetopic integers (see example 4.36) using opetopy.UnnamedOpetope</figcaption></figure>

<figure><img src="image_90.png" /></figure>
<caption>Figure 4.4: Derivation of example 4.37 using opetopy .UnnamedOpetope</caption>

1

2

3

4

5

6

7

from opetopy .UnnamedOpetope import *

# Recall that in this example, the final opetope ω is defined by
→ ω := ( { [ ] ← 2 } ˜ o$_{[}$$_{∗}$$_{]}$ 2 .

example_classic =Graft(
Shift(opedtopic_integer_2),
opedtopic_integer_2,
address(["*"]))

4.6 The system for opetopic sets

**Definition 4.42** (Pasting diagram). Let $\mathbf{p} \in \mathbb{P}^\S$. We define the notion of * pasting diagram* of shape $\mathbf{p}$:

(1) if **p** = ♦, then the expression “♦” is the only pasting diagram of shape ♦;

(2) if **p** is degenerate, then a pasting diagram of shape **p** is an expression of the form $\{\!\{x,$ where *x* is a variable;

(3) otherwise, if {[p₁], ..., [pₖ]} = **p**•, then a pasting diagram of shape **p** is an expression of the form

$$
\begin{cases}
[p_1] \leftarrow x_1 \\
\vdots \\
[p_k] \leftarrow x_k
\end{cases}
$$

where $x_1, \dots, x_k$ are variables.

If $\mathbf{P}$ is a pasting diagram of shape $\mathbf{p}$, then we write $\mathbf{P}^{\mathfrak{h}} = \mathbf{p}$. In the third case, we also write $\mathbf{s}_{[p_i]} \mathbf{P} = x_i$.

**Definition 4.43** (Typing). A *typing* is an expression of the form $x : \mathbf{P} \to y$, where $\mathbf{P}$ is a pasting diagram, and where $x$ and $y$ are variables not occurring in $\mathbf{P}$. The *shape* of $x$ is then simply the shape of $\mathbf{P}$, and we write $x^{\mathfrak{h}} = \mathbf{P}^{\mathfrak{h}}$. Let $t x := y$, and if $[p] \in (x^{\mathfrak{h}})^{\bullet}$, let $\mathbf{s}_{[p]} x := \mathbf{s}_{[p]} \mathbf{P}$.

**Definition 4.44** (Context). A context $\Gamma$ is an ordered list of typings of distinct variables.

In the OPTSET? system, we rely on two types of judgment that can be understood as follows:

(1) “Γ”, meaning that Γ is a context,

(2) “Γ ⊢ P”, meaning that P is a pasting diagram in context Γ.

We now state the inference rules in definition 4.45.

**Definition 4.45** (The OPTSET? system). *Introduction of points.*

$$
\frac{\Gamma}{\Gamma, x : \diamond} \text{ point}
$$