Pierre-Louis Curien
email: curien@irif.fr

Cédric Ho

Samuel Mimram
email: samuel.mimram@lix.polytechnique.fr

Samuel Mimram Syntactical

Syntactical approaches to opetopes

Keywords: Mathematics Subject Classification. Primary 18D50; Secondary 03B15 Opetope, Opetopic set, Sequent calculus, Polynomial functor

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.

Opetopes were originally introduced by Baez and Dolan in order to formulate a definition of weak ωcategories [START_REF] Baez | Higher-dimensional algebra. III. n-categories and the algebra of opetopes[END_REF]]. 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 investigations in order to provide good working definitions of opetopes allowing to explore their combinatorics [Cheng, 2003, Hermida et al., 2000, Leinster, 2004]. One of the most commonly used nowadays is the formulation based on polynomial functors and the corresponding graphical representation using "zoom complexes" [START_REF] Kock | Polynomial functors and opetopes[END_REF].

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

a b c d e f g h i
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 ○ f with i ○ h. Or we can compose f , g and h together all at once, and then the result with i. These two schemes for composing can respectively be pictured (1.1.1)

From there, the general idea of getting "higher-dimensional" is that we should take these compositions as "2operations", which can be composed in various ways. For instance, in the first case, we can compose α with γ, and then β 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 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 [Finster, 2016], which is based on opetopes. Recently, Mimram and Finster have used sequent calculus as a convenient tool to describe globular weak ω-categories [START_REF] Finster | A Type-Theoretical Definition of Weak ω-Categories[END_REF]. Our goal is to achieve a similar type-theoretic presentation for opetopic weak ω-categories [Baez andDolan, 1998, Hermida et al., 2002], and we begin here by defining a representation of opetopes and opetopic sets of type-theoretic flavor.

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, opetopes 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,

⇓

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 α, whose target consists of one cell β whose source and target are the same as the ones of the source of α. It follows recursively that the opetope is entirely determined by the source of α, which we call the associated pasting scheme, which is of dimension n -1. The opetope associated to a pasting scheme of dimension n can be obtained by adding a single cell β of dimension n parallel to the pasting scheme, and an (n + 1)-cell α from the pasting scheme to β.

This article aims to provide syntactic tools making opetopes easier to manipulate than their classical definitions. The unnamed (or anonymous) approaches of chapter 4 on page 47 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 ? presented in figure 4.1.1 on page 50, while opetopic sets are derivable contexts in system OptSet ? . The named approaches of chapter 3 on page 15, 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 ! for describing opetopes, and OptSet ! for opetopic sets, introduced in figures 3.1.1 and 3.5.1 on page 17 and on page 30 respectively. The Python implementation of [START_REF] Ho | [END_REF]] is also discussed.

Generating opetopes

Our two opetope derivation systems Opt ! (figure 3.1.1 on page 17) and Opt ? (figure 4.1.1 on page 50) 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 ω, we can form the (n + 1)-globe whose source and target are ω, as illustrated below. It can geometrically be thought of as the "extrusion" of ω. Ill-formed graftings may occur with n-pasting diagrams, for n ≥ 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 indicated 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

⇓

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

(1) Filling of pasting schemes. Given an n-pasting scheme, 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: (2) Substitution, which consists in replacing a cell in a pasting scheme by another "parallel" pasting scheme.

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: Rules point and degen can also be reformulated in term of pasting schemes, but representing them graphically is not as insightful.

Plan

In chapter 2 on the facing page, 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 chapters 3 and 4 on page 15 and on page 47 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 ! (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 [START_REF] Kock | Polynomial functors and opetopes[END_REF] (which we shall refer to as polynomial opetopes) in sections 3.2 and 4.2;

(3) we showcase the Opt ! and Opt ? systems in examples in sections 3.3 and 4.3; (4) we discuss the Python implementation of Opt ! and Opt ? of [START_REF] Ho | [END_REF] 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 ! (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 [Ho Thanh, 2018a] in sections 3.6 and 4.7; (7) we showcase the OptSet ! and OptSet ? systems in examples in sections 3.7 and 4.8; (8) we discuss the Python implementation of OptSet ! and OptSet ? sections 3.8 and 4.9; (9) for the named approach of chapter 3, we present the additional "mixed" system OptSet ! m in section 3.9 on page 39, with the same plan as previously presented. The equivalence proofs with polynomial opetopes of sections 3.2 and 4.2 on page 20 and on page 52 rely on a precise definition of the Baez-Dolan (-) + construction [Kock et al., 2010, Baez andDolan, 1998], which is presented in appendix A on page 71.

Related works

Our syntactic opetopes are shown in sections 3.2 and 4.2 on page 20 and on page 52 to be equivalent to the polynomial opetopes (or "zoom complexes") of [START_REF] Kock | Polynomial functors and opetopes[END_REF], which are themselves equivalent to Leinster's opetopes [Leinster, 2004]. It is known that the latter are incompatible with Cheng's opetopes [Cheng, 2003], which should be thought of as being symmetric. There is a closely related notion of multitope [START_REF] Hermida | On weak higher-dimensional categories. I. 3[END_REF], Harnik et al., 2008] which is defined in terms of multicategories (whence the multi) instead of operads (ope); the two notions can be shown to be equivalent [Ho Thanh, 2018a]. A syntax for multitopes was proposed in [START_REF] Hermida | On weak higher-dimensional categories. I. 3[END_REF], where however not all the desired computations have been given algorithmic formulations.

The Opetopic proof assistant [Finster, 2016] for weak higher categories relies on the notion of higherdimensional 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 [START_REF] Finster | A Type-Theoretical Definition of Weak ω-Categories[END_REF], starts from the same idea of generating well-formed pasting schemes 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 [START_REF] Bar | Globular: an online proof assistant for higher-dimensional rewriting[END_REF], also based on globular shapes, which is quite popular, notably thanks to its nice graphical interface. CHAPTER 2

Preliminaries

Polynomial functors and trees

We recall basic knowledge on the theory of polynomial functors from e.g. [Kock, 2011, Kock et

I F E F B F I F I F ′ E F ′ B F ′ I F ′ f ⌟ f f f
where all three squares commute, and the middle one is cartesian. This latter condition means that for b ∈ B F , the map f ∶ E F → E F ′ exhibits a bijection between the set E F (b) of inputs of b, and

E F ′ (f (b)) of inputs of f (b).
We note PolyEnd the category of polynomial endofunctors and morphisms, and PolyEnd(I) the category of polynomial endofunctors over the set I, where morphisms as above are required to satisfy f = id I .

A polynomial tree is a polynomial endofunctor T such that (1) I T (also called the set of edges in this case), B T (also called the set of nodes), and E T are finite, and moreover I T ≠ ∅, (2) s and t are injective, and the complement of the image of s has a unique element r ∈ I T which we call the root edge, (3) for every edge i ∈ I T , there exists k ∈ N such that σ k (i) = r, where the walk-to-root function σ ∶ I T → I T is inductively defined by σ(r) = r, and, for i ≠ r ∈ I T , σ(i) = tp(s -1 (i)). An edge that is not in the image of σ is called a leaf. Let Tree be the full subcategory of PolyEnd spanned by trees. We emphasize that morphisms in Tree are not required to be identities on edges, unlike what would happen if Tree was a subcategory of PolyEnd(I).

For F ∈ PolyEnd, let tr F , the category of F -trees, be a chosen skeleton of Tree/F . Depending on the context, it may also refer to the set of isomorphism classes of F -trees. An F -tree is thus a tree ⟨T ⟩ and a morphism of polynomial functors T ∶ ⟨T ⟩ → F . For x an edge of T (or more precisely of ⟨T ⟩), the morphism T associates a color i = T (x) ∈ I F , and we say that x is decorated with i, and likewise for nodes.

Let T ∈ tr F , and σ the walk-to-root function of ⟨T ⟩. Write ⟨T ⟩ as

I T E T B T I T . s p t
For an edge x ∈ I T we define inductively the address of x, noted &x, which is a bracket-enclosed list of elements of E T , indicating the path from the root to that edge. If x is the root edge, then &x = [], the empty list. Otherwise,

let &x = (&σ(x)) ⋅ [x],
where ⋅ is the concatenation of lists. If y ∈ B T is a node of T , let its address be given by &y = &t(y), that is, it is the address of its output edge. Write T • the set of node addresses of T , and for [p] ∈ T and the obvious morphism to F . This corresponds uniquely to the F -tree with no node and a unique edge, decorated by i. Equivalently, it corresponds uniquely to the edge address of an edge decorated in i. Let now b ∈ B, and define Y b ∈ tr F , the corolla at b, as having underlying tree

E(b) + {t(b)} E(b) {b} E(b) + {t(b)}, b (2.1.3)
where the left map is increasing with codomain {1, . . . , n}, and the right one maps b to n + 1. This corresponds to a F -tree with a unique node, decorated by b, or equivalently, to the node address of such a node. Let S, T ∈ tr F be two F -trees, where the root edge (that at address []) of T is decorated by i ∈ I F , and let [l] ∈ S | be the address of a leaf of S decorated by i. We define the grafting S ○ [l] T of S and T on l by the following pushout (in tr F ): Kock, 2011]). Every F -tree is either of the form I i , for some i ∈ I, or obtained by graftings a corollas on an F -tree.

I i T S S ○ [l] T. ⌜ r l (2.1.4) Proposition 2.1.5 ([
Take T, U 1 , . . . , U k ∈ tr F , where the leaves of T have addresses [l 1 ], . . . , [l k ], and assume the grafting T ○ [li] U i is defined for all i. Then the total grafting will be denoted concisely by

T ◯ [li] U i = (⋯(T ○ [l1] U 1 ) ○ [l2] U 2 ⋯) ○ [l k ] U k . (2.1.6)
It is easy to see that the result does not depend on the order in which the graftings are performed. From such a monad M , we may define a new polynomial monad M + whose underlying functor is given by

B M tr • M tr M B M s u t
where tr • M is the set of M -trees with one marked node (or equivalently, equipped with one of their node addresses), s gives the marked node (or more precisely its decoration), u forgets the marking, and t is induced from the monad law of M . The monad structure of M + is given by substitution of trees, see appendix A.2 on page 73.

Opetopes

2.2.1. Definition. Let Z 0 be the identity polynomial monad on Set, on the left, and define

Z n+1 ∶=(Z n ) + . { * } { * } { * } { * }, O n E Z n+1 O n+1 O n . s t
If we write the polynomial functor Z n as on the right, an n-opetope ω is by definition an element of O n , and we say that ω has dimension n, written dim ω = n. The map s is called the source map, and t the target map. The unique 0-opetope is written ⧫ and called the point, whereas the unique 1-opetope is written ◾ and called the arrow. For n ≥ 2, we have O n = tr Z n-2 , hence an n-opetope is a tree whose nodes and edges are decorated with (n -1)-opetopes and (n -2)-opetopes, respectively. For ω ∈ O n , the set E Z n (ω) is precisely ω • , i.e. is the set of node addresses of ω. The readdressing of ω is then of the form

℘ ω ∶ ω | → (t ω) • .
2.2.2. Opetopes vs. pasting schemes. Opetopes are closely related to the notion of "pasting scheme" commonly used in higher category theory to describe composition of higher cells. Informally, a pasting scheme 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 represents a 2-pasting scheme, and the corresponding tree is drawn on the right:

. . . . . ⇓ ⇓ ⇓ • • •
If we consider the k-cells as k-opetopes for all k, then an n-pasting scheme P induces a Z n-1 -tree, thus an (n + 1)opetope, say ω. We say that P is the source pasting scheme of ω. Further, by definition of Z n , the opetope ω has a target t ω ∈ O n-1 . In the sequel, graphical representations of opetopes include both the source pasting scheme and the target: for instance, if P is the pasting scheme above, then ω is represented by

⇓

represents a 2-opetope (whose underlying 1-pasting scheme has three 1-cells), but also a 2-pasting scheme having a unique 2-cell. In this work, such ambiguities shall be lifted by the surrounding context.

2.2.3. Higher addresses. We now introduce the concept of higher dimensional address, a refinement if that of addresses presented in section 2.1 on page 9, which will serve as a more convenient way to designate nodes and edges of opetopes. Start by defining the set A n of n-addresses as follows:

A 0 = { * } , A n+1 = lists A n ,
where lists X is the set of finite lists (or words) on the alphabet X. Explicitly, the unique 0-address is * (also written [] by convention), while an (n + 1)-address is a sequence of n-addresses. Such sequences are enclosed by brackets. Note that the address [], associated to the empty word, is in A n for all n ≥ 0. However, the surrounding context will almost always make the notation unambiguous 1 . Here are examples of the words we shall use:

[] ∈ A 1 , [ * * * * ] ∈ A 1 , [[][ * ][]] ∈ A 2 , [[[[ * ]]]] ∈ A 4 . . . For ω ∈ O
an opetope, nodes of ω can be uniquely specified using higher addresses as we now show. In Z 0 , set

E Z 1 (◾) = { * }, so that the unique node address of ◾ is * ∈ A 0 . For n ≥ 2, recall that an opetope ω ∈ O n is a Z n-2 -tree: ω ∶ ⟨ω⟩ → Z n-2 . A node b ∈ B ⟨ω⟩ has an address &b ∈ lists E ⟨ω⟩ , which by ω ∶ E ⟨ω⟩ → E Z n-1 is mapped to an element of lists E Z n-1 . By induction, elements of E Z n-1 are (n-2)-addresses, whence E ⟨ω⟩ (&b) ∈ list A n-2 = A n-1 .
For the induction step, elements of E Z n (ω) are nodes of ⟨ω⟩, which we identify by their aforementioned (n -1)-addresses. Consequently, for all n ≥ 1 and ω ∈ O n , elements of E Z n (ω) = ω • can be seen as the set of (n -1)-addresses of the nodes of ω, and similarily, ω | can be seen as the set of (n -1)-addresses of edges of ω.

We denote the concatenation of higher addresses by

⋅, i.e. if [p 1 ], [p 2 ] are n-addresses, then [p 1 ]⋅[p 2 ] ∶=[p 1 p 2 ].
Let ⊑ be the prefix order on the set of n-addresses: [p 1 ] ⊑ [p 2 ] if and only if as sequences, p 1 is a prefix of p 2 . Let 1 Ambiguity with addresses could be lifted altogether by hinting the dimension as e.g.

[] 1 ∈ A 1 , [ * * * * ] 1 ∈ A 1 , [[] 1 [ * ] 1 [] 1 ] 2 ∈ A 2 , [[[[ * ] 1 ] 2 ] 3 ] 4 ∈ A 4
. This however makes notations significantly heavier, so we avoid using this convention.

⪯ be the lexicographical order on the set of n-addresses. Explicitly, it is trivial on A 0 , given by the prefix order ⊑ on A 1 , and on A n , seen as the set of finite sequences of elements of A n-1 , it is induced from the lexicographical order on A n-1 . Remark that ⊑ is always a suborder of ⪯.

Example 2.2.1. Consider the following 2-opetope, called 3: . . . .

⇓

Its underlying pasting diagram consists of 3 arrows ◾ grafted linearly. Since the only node address of ◾ is * ∈ A 0 , the underlying tree of 3 can be depicted as follows:

◾ ◾ ◾ ⧫ ⧫ ⧫ ⧫ * * * [] [ * ] [ * * ]
On the left are the decorations: nodes are decorated with ◾ ∈ O 1 , while the edges are decorated with ⧫ ∈ O 0 . For each node int the tree, the set of input edges of that node is in bijective correspondence with the node addresses of the decorating opetope, and that address is written on the right of each edges. In this low dimensional example, those addresses can only be * . Finally, on the right of each node 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:

3 ◾ ◾ ◾ ◾ [ ] [ * ] [ * * ] []
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, with its annotated underlying tree on the right (the 2-opetopes 1 and 2 are analogous to 3):

. . . . . ⇓ ⇓ ⇓ ⇛ . . . . . ⇓ 3 1 2 ◾ ◾ ◾ ◾ ◾ ◾ ◾ [] [[ * * ]] [[ * ]] [ * * ] [ * ] [ ] [] [ ] [ * ] Let [l] = [p[q]] ∈ A n-1 be an address such that [p] ∈ ω • and [q] ∈ (s [p] ω)
• . Then as a shorthand, we write

e [l] ω ∶= s [q] s [p] ω. (2.2.2)
The source map s give the decoration of a node in a tree, and likewise, e gives the decoration of edges.

Remark 2.2.3 (Opetopic induction). The proposition 2.1.5 on page 10 allows a fundamental type of induction on opetopes that we use frequently throughout this paper. Let Φ(-) be a logical proposition about opetopes such that (1) Φ holds for ⧫, written Φ(⧫),

(2) Φ(ψ) ⇒ Φ(I ψ ) ∧ Φ(Y ψ ), for all ψ ∈ O, (3) Φ(ν) ∧ Φ(ψ) ⇒ Φ(ν ○ [l] Y ψ ), for ν, ψ ∈ O with at least one node, [l] ∈ ν | ,
and assuming the grafting is well-defined. Then Φ holds for all opetope.

2.2.4. The category of opetopes. In this subsection, we define the category O of opetopes. We first begin by a result whose geometrical meaning is explained later in this section. Lemma 2.2.4 (Opetopic identities, [Ho Thanh, 2018a]). Let ω ∈ O n with n ≥ 2.

(1) (Inner edge) For [p[q]] ∈ ω • (forcing ω to be non degenerate), we have t s

[p[q]] ω = s [q] s [p] ω. (2) (Globularity 1) If ω is non degenerate, we have t s [] ω = t t ω. (3) (Globularity 2) If ω is non degenerate, and [p[q]] ∈ ω | , we have s [q] s [p] ω = s ℘ω[p[q]] t ω. (4) (Degeneracy) If ω is degenerate, we have s [] t ω = t t ω.
With those identities in mind, we define the category O of opetopes by generators and relations as follows.

( p[q]] ∈ ω • (forcing ω to be non degenerate), the following square must commute:

s [q] s [p] ω s [p] ω s [p[q]] ω ω s [q] t s [p] s [p[q]]
(b) (Glob1) if ω is non degenerate, the following square must commute: and for [p[q]] ∈ ω | , the following square must commute:

t t ω t ω s [] ω ω. t t t s [] (c) (Glob2) if ω is non degenerate,
s ℘ω[p[q]] t ω t ω s [p] ω ω. s ℘ω[p[q]] s [q] t s [p]
(d) (Degen) if ω is degenerate, the following square must commute:

t t ω t ω t ω ω. t s [] t t
An opetopic set is a Set-valued presheaf over O. We write Ô for the category of opetopic sets and natural transformations, O[-] ∶ O → Ô for the Yoneda embedding, and Fin Ô for the full subcategory of Ô spanned by finite opetopic sets, i.e. those X ∈ Ô such that ∑ ω∈O X ω is a finite set. Equivalently, Fin Ô is the completion of O under finite colimits.

Let us explain this definition a little more. As previously mentioned, 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.

(1) (Inner) The inner edge at [p[q]] ∈ ω • is decorated by the target of the decoration of the node "above" it (here s [p[q]] ω), and in the [q]-source of the node "below" it (here s [p] ω). By construction, those two decorations match, and this relation makes the two corresponding embeddings s [q] s [p] ω → ω match as well. On the left is an informal diagram about ω 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.

t s [ p [ q ] ] ω s [ q ] s [ p ] ω s [p] ω s [p[q]] ω ω . . . . ⇓ ⇓ ⇛ .
. . .

⇓

(2) (Glob1-2) If we consider the underlying tree of ω (which really is ω itself) as its "geometrical source", and the corolla Y t ω as its "geometrical target", then they should be parallel. The relation (Glob1) expresses this idea by "gluing" the root edges of ω and Y t ω together, while (Glob2) glues the leaves according to the readdressing function ℘ ω .

t s [] ω ⋯ ω s [] ω t t ω ⋯ t ω . . . . ⇓ ⇓ ⇛ . . . . ⇓ ⋯ s[q] s[p ] ω ω s [p] ω ⋯ s℘ω [p [q ]] t ω t ω . . . . ⇓ ⇓ ⇛ .
. . .

⇓

(3) (Degen) If ω is a degenerate opetope, depicted as on the right, then its target should be a "loop", i.e. its only source and target should be glued together.

s [] t ω ω s [] t ω t t ω t ω • ⇓ CHAPTER 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 scheme is pictured below:

a b c d e f g h i j k ⇓α ⇓β ⇓γ
We shall use the names of the cells of this picture as variables, and encode the pasting scheme as the following expression: γ(j ← α, k ← β). Here, j, k, α, β, and γ are now variables, equipped with a dimension (1 for j and k, and 2 for α , β, and γ), and the notation is meant to be read as "the variable γ in which α (resp. β) has been formally grafted on the input labeled j (resp. k)". Such a term will be given a type:

i(t ← h(z ← g(y ← f ))) ⊷ a ⊷ ∅,
which expresses the fact that the source is the "composite" i ○ h ○ g ○ f , and that the source of the source is x. Since the pasting scheme is 2-dimensional, there is no further iterated source, and we conclude the sequence by a ∅ symbol (which can be read as the only (-1)-dimensional pasting scheme). Similarly, the degenerate pasting scheme on the left below will be denoted by the typed term figured on the right:

.

⇓ • x f α α ∶ x ⊷ x ⊷ ∅
where the term x denotes a degenerate 1-dimensional pasting scheme with x as source.

3.1.1.1. Terms. We have a N-graded set V of variables. Elements of V n represent n-dimensional cells. An n-term is constructed according to the following grammar:

T -1 ::= {∅} by convention

T 0 ::= V 0 T n+1 ::= V n | T ′ n+1 T ′ n+1 ::= V n+1 (V n ← T ′ n+1 , . . .)
where the expression (V n ← T ′ n+1 , . . .) signifies that there is 0 or more instances of the "V n ← T ′ n+1 " part between the parentheses. For example, if f, g ∈ V 1 , and a ∈ V 0 , then the following is an element of T 1 :

g(a ← f ())
To make notations lighter, we do not write empty parentheses "()", so the previous 1-term can be more concisely written as g(a ← f ). The terms of the form u are called degenerate terms, or empty syntactic pasting schemes.

A term of the form g(a 1 ← f 1 , . . . , a k ← f k ) will oftentimes be abbreviated as g( → a i ← f i ), leaving k implicit. By convention, the sequence a 1 ← f 1 , . . . , a k ← f k above is always considered up to permutation: for σ a bijection of the set {1, . . . , k}, the terms g(a 1 ← f 1 , . . . , a k ← f k ) and g(a σ(1) ← f σ(1) , . . . , a σ(k) ← f σ(k) ) are considered equal. Note that the above definition entails that T 0 = V 0 (in particular, there are no degenerate 0-terms).

For t ∈ T n , write t • for the set of n-variables occurring in t. In the previous example, (g(a ← f ))

• = {f, g}. Note that x ∈ x • for all x ∈ V n . We consider terms of the form y, with y ∈ V k , as empty, or degenerate, (n+1)-terms, i.e. with no (n + 1)-variables.

3.1.1.2. Types. An n-type T is a sequence of terms of the form

s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅,
where s i ∈ T n-i . As we will see (rule shift in figure 3.1.1 on the next page, and theorem 3.1.8 on page 19), this sequence of terms essentially describes a zoom complex in the sense of [START_REF] Kock | Polynomial functors and opetopes[END_REF], which justifies the use of the ⊷ symbol. A typing of a term t ∈ T n is an expression of the form t ∶ T , for T an n-type. If T is as above, then s i is thought of as the i-th (iterated) source of t. We then write s t ∶= s 1 , and more generally s i t ∶= s i . By convention, s 0 t ∶= t.

3.1.1.3. Contexts. A context Γ is a set of typings, more commonly written as a list. Write V Γ,k for the set of k-variables typed in Γ, let V Γ ∶= ∑ k∈N V Γ,k , write T Γ,k for the set of k-terms whose variables (in any dimension) are in V Γ , and T Γ ∶= ∑ k∈N T Γ,k . As we will see (inference rules in figure 3.1.1 on the next page), for a derivable context Γ, if x occurs in the typing of a variable of Γ, then x ∈ V Γ . Note that in any context Γ, if a variable x ∈ V Γ,k occurs in the type of y ∈ V Γ,l , then k < l, and thus there is no cyclic dependency among variables.

3.1.1.4. Sequents. Let Γ be a context. An equational theory E on V Γ is a set of formal equalities between variables of Γ. We write = E for the equivalence relation on V Γ generated by E. A sequent is an expression of the form E ▹ Γ ⊢ t ∶ T where Γ is a context, E is an equational theory on V Γ , and the right hand side is a typing. We may write ⊢ n to signify that t ∈ T n . The equivalence relation = E on V Γ extends to T Γ in an obvious way. If x = E y ∈ t • , then, by convention x ∈ t • , so that x and y really are interchangeable.

If

(F ▹ Υ ⊢ u ∶ U ) is a sequent such that there exists a bijection σ ∶ V Υ → V Γ with (E ▹ Γ ⊢ t ∶ T ) = (F σ ▹ Υ σ ⊢ u σ ∶ U σ )
, where (-) σ is the substitution according to σ, then we say that both sequents are equivalent (or α-equivalent), denoted

(E ▹ Γ ⊢ t ∶ T ) ≃ (F ▹ Υ ⊢ u ∶ U ) .
In the following, sequents are implicitly considered up to equivalence.

3.1.2. Inference rules. We present the inference rules of the Opt ! system in figure 3.1.1 on the facing page. Rule graft requires the so-called graft notation and substitution operation, respectively introduced in definitions 3.1.1 and 3.1.3 on the next page.

E ▹ Γ ⊢ n x ∶ T degen E ▹ Γ ⊢ n+1 x ∶ x ⊷ T
Shift to the next dimension: This rule takes a term t and introduces a new cell x having t as source. If

x ∈ V n+1 is such that x ∉ V Γ , then E ▹ Γ ⊢ n t ∶ T shift E ▹ Γ, x ∶ t ⊷ T ⊢ n+1 x ∶ t ⊷ T Grafting:
This rule glues an n-cell x onto an n-term t along a variable a ∈ s • 1 ∶=(s t) • . We assume that Γ and Υ are compatible, in that for all y ∈ V, if y ∈ V Γ ∩ V Υ , then the typing of y in both contexts match modulo the equational theory E ∪ F . Further, the only variables typed in both Γ and Υ are a and the variables occurring in the sources of a (i.e. s i a, for

1 ≤ i ≤ n -1). If x ∈ V n , t ∈ T n is not degenerate, a ∈ (s t) • is such that s a = s s x, then E ▹ Γ ⊢ n t ∶ s 1 ⊷ s 2 ⊷ ⋯ F ▹ Υ ⊢ n x ∶ U graft G ▹ Γ ∪ Υ ⊢ n t(a ← x) ∶ s 1 [s x/a] ⊷ s 2 ⊷ ⋯
where the notations t(a ← x) and s 1 [s x/a] are presented below, where G is the union of E, F , and potentially a set of additional equalities incurred by the substitution s 1 [s x/a]. We also write graft-a to make explicit that we grafted onto a.

The condition a ∈ (s t) • ensures that a hasn't been used for grafting beforehand, while the condition s a = E s s x shows that x may indeed be glued onto a. Definition 3.1.1 (Graft notation). For a sequent (E ▹ Γ ⊢ n t ∶ T ), a ∈ V n-1 , and x ∈ V Υ,n , the graft notation t(a ← x) of the graft rule can be simplified depending on the structure of t, according to the following rewriting rule: for y ∈ V Γ,n :

y( → z i ← v i )(a ← x) ⟿ { y( → z i ← v i (a ← x)) if a ∉ (s y) • , y( → z i ← v i , a ← x) if a ∈ (s y) • , (3.1.2)
In particular, note that if a ∉ (s y) • , then y()(a ← x) ⟿ y(), and with the "empty parentheses convention", this gives y(a ← x) ⟿ y.

Definition 3.1.3 (Substitution). We now explain how to evaluate u[w/a] for any term u ∈ T n-1 . We let

u[w/a] ∶= { y( → z i ← v i [w/a]) if a ≠ E∪F y, w( → z i ← v i ) if a = E∪F y.
and then, in the case w = b, we perform the following actions:

(1) for subterms of the form x(. . . , z ← b, . . .), we remove the grafting z ← b, and add the equation b = z to the ambient equational theory, (2) for subterms of the form x(. . . (1) If w is not an empty pasting diagram (i.e. not of the form b), then writing u = y( (e) otherwise, if u is of the form y( → z i ← v i ), and if the previous cases do not apply (i.e. a is not the front variable of u or v i for all i), then

→ z i ← v i ): u[w/a] ∶= { y( → z i ← v i [w/a]) if a ≠ E∪F y, w( → z i ← v i ) if a = E∪F y. ( 3
u[b/a] ∶= y( → z i ← v i [b/a]),
as in equation (3.1.4) on the preceding page.

From the formulation of system Opt ! , 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.

Example 3.1.5. Consider the term t = α(g ← β) in a suitable context Γ:

x y . z f g h i ⇓α ⇓β Then the graftings t(f ← γ) = α(f ← γ, g ← β) and t(i ← γ ′ ) = α(g ← β(i ← γ))
, for some appropriate γ and γ ′ , can respectively be represented as:

α ∶ g(y ← f ) ⊷ x ⊷ ∅, β x ∶ x ⊷ x ⊷ ∅, β y ∶ y ⊷ y ⊷ ∅.
Then α, α(f ← β x ), and α(g ← β y ) can respectively be represented as: Then the sources α(f ← β x ) and α(g ← β y ) are respectively

g(y ← f )[x/f ] = g(y ← x) = g, g(y ← f )[y/g] = y(y ← f ) = f,
and, in the first case, the equation x = y is added to the ambient equational theory.

Remark 3.1.7. The degen rule may be replaced by the following degen-shift rule without changing the set of derivable sequents of the form

(E ▹ Γ ⊢ y ∶ T ) with y ∈ V: if x ∈ V n and d ∈ V n+2 such that d ∉ V Γ,n+2 , then E ▹ Γ ⊢ n x ∶ T degen-shift E ▹ Γ, d ∶ x ⊷ x ⊷ T ⊢ n+2 d ∶ x ⊷ x ⊷ T However, note that sequents of the form (E ▹ Γ ⊢ y ∶ T ) are no longer derivable. 1 The case in which u is of the form y(. . . , z ← a(b 1 ← r 1 , . . . , b k ← r k ), . . .) with k > 1 does not happen in valid derivations.
3.1.3. Uniqueness of typing. Let (E ▹ Γ ⊢ x ∶ X) be a derivable sequent. We prove in theorem 3.1.8 that the type X = (s x ⊷ s s x ⊷ ⋯) is completely determined by s x and Γ.

A consequence of this result is that at any stage, a context Γ may be replaced by its "meager form" Γ, obtained by replacing "full typings" y ∶ Y by y ∶ s y, i.e. by removing all but the top term of Y . Using meager context comes with a cost however: checking the hypothesis of rule graft requires to compute the second source s s x of x, which is not contained in Γ. For clarity, we do not make use of meager forms throughout the rest of this work.

Define the function s as follows:

s ∶ T Γ → T Γ x → s x x ∈ V Γ , x → x x ∈ V Γ , x( → y i ← u i ) → (s x)[ → su i /y i ] x, → y i ∈ V Γ , → u i ∈ T Γ . Theorem 3.1.8. Let (E ▹ Γ ⊢ t ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅) be a derivable sequent. Then for 1 ≤ k ≤ n we have s k = s k t, or equivalently, for 0 ≤ i ≤ n, we have ss i = s i+1 , with 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:

point x ∶ ∅ then sx = s x = ∅, since x ∈ V.
(2) If the sequent is obtained by the following proof tree:

s 1 ∶ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ degen t ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ then s 1 ∈ V and t = s 1 . Thus, st = s 1 , while for 1 ≤ i ≤ n, the equality ss i = s i+1 holds by induction.
(3) If the sequent is obtained by the following proof tree:

s 1 ∶ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ shift t ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ then t ∈ V,
so st = s t = s 1 , while for 1 ≤ i ≤ n, the equality ss i = s i+1 holds by induction. (4) Assume now that the sequent is obtained by the following proof tree:

u ∶ r 1 ⊷ r 2 ⊷ s 3 ⊷ ⋯ ⊷ s n ⊷ ∅ x ∶ X graft-a t ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ with a ∈ r • 1 and x ∈ V such that s s x = s a. Then t = u(a ← x), s 1 = r 1 [s x/a],
and s i = r i for 2 ≤ i ≤ n. On the one hand, we have

st = s (u(a ← x)) = su[sx/a] = su[s x/a] since x ∈ V = s 1 .
On the other hand, write

r 1 = v(y ← a( → z i ← w i )), for some v, → w i ∈ T n-1 and y ∈ V n-2 .
Then

ss 1 = s (r 1 [s x/a]) = s (v(y ← (s x)( → z i ← w i ))) = (sv)[(s s x)[ → sw i /z i ]/y] = (sv)[(s s x)[ → sw i /z i ]/y] by ind. = (sv)[(s a)[ → sw i /z i ]/y] hyp. of graft-a = sr 1 = r 2 = s 2 .
Finally, for 1 ≤ i ≤ n, the equality ss i = s i+1 holds by induction. □ Corollary 3.1.9. Let (E ▹ Γ ⊢ t ∶ T ) be a derivable sequent, and

x ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ be a typing in Γ. Then for 1 ≤ k ≤ n we have s k = s k t, or equivalently, for 0 ≤ i ≤ n, we have ss i = s i+1 , with s 0 ∶= x. Proof. If x ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅ is a typing in Γ, then somewhere in the proof tree of (E ▹Γ ⊢ t ∶ T ) appears a sequent of the form (F ▹ Υ ⊢ x ∶ s 1 ⊷ s 2 ⊷ ⋯ ⊷ s n ⊷ ∅)
, which is necessarily derivable. We conclude by applying theorem 3.1.8 on the preceding page □ By definition, s extends s to a function T Γ → T Γ , and for convenience, we just write it as s in the sequel, and call it the source of a term.

Example 3.1.10. Consider the following term:

α(f ← γ, g ← β) = x y . z f g h i ⇓α ⇓β j γ ⇒
Then its source is computed as follows:

s (α(f ← γ, g ← β)) = (s α) [(s γ)/f, (s β)/g] = (g(y ← f )) [(s γ)/f, (s β)/g] since s α = g(y ← f ) = (g(y ← f )) [j/f, (s β)/g] since s γ = j = (g(y ← f )) [j/f, i(z ← h)/g] since s β = i(z ← h) = (g(y ← j)) [i(z ← h)/g] = (i(z ← h)) (y ← j) = i(z ← h(y ← j)) since y ∈ (s h) • .
The latter term indeed corresponds to the source of the pasting diagram, i.e. the arrow composition on the top.

Equivalence with polynomial opetopes

In this section, all sequents are assumed derivable in Opt ! . We show that sequents typing a variable (up to ≃) are in bijective correspondence with polynomial opetopes (see section 2.2 on page 10). To this end, we define the polynomial coding operation ⟦-⟧ poly n+1 that maps a sequent 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):

(E ▹ Γ ⊢ n t ∶ T ), with t ∈ T n , to an (n + 1)-opetope ⟦E ▹ Γ ⊢ n t ∶ T ⟧ poly n+1 ∈ O n+1 ,
⟦α(g ← β)⟧ = ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ • α f g • β h i ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ ∶= • ⟦α⟧ ⟦f ⟧ ⟦g⟧ • ⟦β⟧ ⟦h⟧ ⟦i⟧ where ⟦-⟧ is a shorthand for ⟦-⟧ poly . For t = x( → y i ← u i ) ∈ T n and z ∈ t • , the address & t z ∈ A n of z in t is an n-address (see section 2.2.3 on page 11) that indicates "where z is located in t". Definition 3.2.1 (Address). Take t ∈ T Γ , t = x( → y i ← u i ). (1) For z ∈ t • , the address & t z ∈ A n of z in t is given by & t z ∶= { [] if z = x in the current eq. th., [& s x y i ] ⋅ & ui z if z ∈ u • i , If [p] = & t z, then we write s [p] t ∶= z. In particular, s [] t = x. (2) For a ∈ (s t) • , the address & t a ∈ A n of a in t is given by & t a ∶= { [& s x a] if a ∈ (s x) • , [& s x y i ] ⋅ & ui a if a ∉ (s x) • , but a ∈ (s u i ) • .
Example 3.2.2. The context describing the following pasting scheme:

x y . z f g h i ⇓α ⇓β contains the following typings: x, y, z ∶ ∅, f ∶ x ⊷ ∅, g ∶ y ⊷ ∅, h ∶ y ⊷ ∅, i ∶ z ⊷ ∅, α ∶ g(y ← f ) ⊷ a ⊷ ∅, and β ∶ i(z ← h) ⊷ b ⊷ ∅. Then for t ∶= α(g ← β), we have & t α = [], & t β = [& s α g] ⋅ & β β = [[]] ⋅ [] = [[]], & t i = [& s α g] ⋅ & β i = [[]] ⋅ [& s β i] = [[]] ⋅ [[]] = [[][]], & t h = [& s α g] ⋅ & β h = [[]] ⋅ [& s β h] = [[]] ⋅ [[& s i z] ⋅ & h h] = [[][[]]] = [[][ * ]], & t f = [& s α f ] = [[& s g y] ⋅ & f f ] = [[ * ]].
Those addresses indeed match with that of the corresponding opetope:

2 2 ◾ ◾ ◾ ◾ ◾ [] [[]] [ ] [ * ] [ ] [ * ] Definition 3.2.3 (Polynomial coding). The polynomial coding operation ⟦-⟧ poly n
is defined inductively by:

⟦x ∶ ∅⟧ poly 0 ∶= ⧫ x ∈ V 0 , (3.2.4) ⟦x ∶ x ⊷ ⋯⟧ poly n+2 ∶= I ⟦x⟧ poly n x ∈ V n , (3.2.5) ⟦x( → y i ← u i ) ∶ ⋯⟧ poly n+1 ∶= Y ⟦x⟧ poly n ◯ [&s x yi] ⟦u i ⟧ poly n+1 x( → y i ← u i ) ∈ T n .
(3.2.6)

We recall that (see equation (2.1.6) on page 10)

Y ⟦x⟧ poly n ◯ [&s xyi] ⟦u i ⟧ poly n+1 ∶= (⋯ (Y ⟦x⟧ poly n ○ [&s x y1] ⟦u 1 ⟧ poly n+1 ) ○ [&s x y2] ⟦u 2 ⟧ poly n+1 ⋯) ○ [&s xyk ] ⟦u k ⟧ poly n+1 .
It is clear that the coding function is well defined in equations (3.2.4) and (3.2.5). We now establish a series of results to prove proposition 3.2.12 on page 23 stating that equation (3.2.6) is well defined too.

Proposition 3.2.7. For t ∈ T Γ,n , t = x( → y i ← u i ), z ∈ t • , and [p] ∶= & t z, we have s [p] ⟦t⟧ poly n+1 = ⟦z⟧ poly n . Proof. By definition we have ⟦t⟧ poly n+1 = Y ⟦x⟧ poly n ◯ [&s x yi] ⟦u i ⟧ poly n+1 ,
and we distinguish two cases.

If z = x, then [p] = [],
and the result clearly holds. Otherwise,

[p] = [& s x y j ] ⋅ & uj z, for j such that z ∈ u • j . Then, s [p] ⟦t⟧ poly n+1 = s [&s x yj ]⋅&u i z ⎛ ⎝ Y ⟦x⟧ poly n ◯ [&s xyi] ⟦u i ⟧ poly n+1 ⎞ ⎠ = s &u j z ⟦u j ⟧ poly n+1
= ⟦z⟧ poly n by induction □ Corollary 3.2.8. For x as in case (3.2.6) above, and

[q i ] ∶= & s x y i we have s [qi] ⟦x⟧ poly n = ⟦y i ⟧ poly n-1 . Proof. We have s [qi] ⟦x⟧ poly n = s [qi] ⟦s x⟧ poly n = ⟦y i ⟧ poly n-1 . □
Lemma 3.2.9. Consider the following derivation tree:

⋯ ⊢ n t ∶ T ⋯ ⊢ n x ∶ X graft-a ⋯ ⊢ n t(a ← x) ∶ R Writing r ∶= t(a ← x),
r = z( → y i ← u i )(a ← x) = { z( → y i ← u i , a ← x) if a ∈ (s z) • , z( → y i ← u i (a ← x)) if a ∉ (s z) • .
There are two cases:

(

1) if a ∈ (s z) • , then [l] = [& s z a] = & t a; (2) if a ∉ (s z) • , then ⟦r⟧ poly n+1 = Y ⟦z⟧ poly n ◯ [&s z yi] ⟦u i (a ← x)⟧ poly n+1 .
Let j be the index such that a ∈ (s u j ) • . Then, by induction,

⟦u j (a ← x)⟧ poly n+1 = ⟦u j ⟧ poly n+1 ○ &u j a Y ⟦x⟧ poly n , thus [l] = [& s z y j ] ⋅ & uj a = & t a. □ Lemma 3.2.10 (Named readdressing lemma). Let r ∈ T Γ,n . Then for b ∈ (s r) • , we have & s r b = ℘ ⟦r⟧ poly n+1
& r b, where ℘ is the readdressing function introduced in section 2.1.1 on page 10.

Proof. Recall the definition of the readdressing map from appendix A on page 71. If r is a variable, then

& s r b = ℘ Y ⟦r⟧ poly n [& s r b] = ℘ ⟦r⟧ poly n+1 & r b.
Otherwise, write the derivation tree of r:

⋯ ⊢ n t ∶ T ⋯ ⊢ n x ∶ X graft-a ⋯ ⊢ n r ∶ R assume that & s t a = ℘ ⟦t⟧ poly n+1 & t a holds by induction. Since s r = s t[s x/a], we have & s r b = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ & s t a ⋅ & s x b if b ∈ (s x) • , & s t a ⋅ & s x c ⋅ [p] if b ∈ (s t) • , & s t a ⊑ & s t b, say & s t b = & s t a ⋅ [& s a c] ⋅ [p], & s t b if b ∈ (s t) • , & s t a / ⊑ & s t b. = ℘ (⟦t⟧ poly n+1 ○ & t a Y ⟦x⟧ poly n ) & r b = ℘ ⟦r⟧ poly n+1 & r b. □ Proposition 3.2.11. Let α ∈ V n be a typed n-variable, for n ≥ 2. Then t ⟦α⟧ poly n = ⟦s s α⟧ poly n-1 . Proof. We proceed by induction on s α. (1) If s α = x ∈ V n-1 , then ⟦α⟧ poly n = Y ⟦x⟧ poly n-1
, and t ⟦α⟧

poly n = ⟦x⟧ poly n-1 = ⟦s x⟧ poly n-1 = ⟦s s α⟧ poly n-1 . (2) If s α = a for some a ∈ V n-2 , then ⟦α⟧ poly n = I ⟦a⟧ poly n-2
, and t ⟦α⟧

poly n = Y ⟦a⟧ poly n-2 = ⟦a⟧ poly n-1 = ⟦s s α⟧ poly n .
(3) Otherwise, s α is given by the following proof tree:

⋯ ⊢ n t ∶ T ⋯ ⊢ n x ∶ X graft-a ⋯ ⊢ n s α ∶ s s α ⊷ ⋯
and write r ∶= s α = t(a ← x) for shorter notations. By lemma 3.2.9 on the facing page we have , and the graftings are well defined. = ω, for any opetopes ω ∈ O n . We proceed by opetopic induction (see remark 2.2.3 on page 12).

Proof. Write u i ∶= a( → b j ← v j ). Then t s [] ⟦u i ⟧ poly n+1 = t ⟦a⟧
(1) Trivially, ⟦⧫⟧ ! is obtained by the following proof tree:

point ⟦⧫⟧ ! (3.2.14)
with an arbitrary choice of variable (different choices lead to equivalent sequents).

(2) For ϕ ∈ O n-2 the sequent ⟦I ϕ ⟧ ! is obtained by the following proof tree:

⟦ϕ⟧ ! degen ⟦I ϕ ⟧ ! (3.2.15) (3) For ψ ∈ O n-1 , the sequent ⟦Y ψ ⟧
! is obtained by the following proof tree:

⟦ψ⟧ ! shift ⟦Y ψ ⟧ ! (3.2.16)
with an arbitrary choice of fresh variable (different choices lead to equivalent sequents). (4) Let ν ∈ O n having at least one node, [l] ∈ ν | , and ψ ∈ O n-1 be such that the grafting ν ○

[l] Y ψ is well-defined. Then the sequent ⟦ν ○ [l] Y ψ ⟧
! is obtained by the following proof tree:

⟦ν⟧ ! ⟦ψ⟧ ! graft-a ⟦ν ○ [l] Y ψ ⟧ ! (3.2.17) where ⟦ν⟧ ! = (E ▹ Γ ⊢ n u ∶ U ), where the variable a ∈ (s s u) • is such that & s s u a = [l]
(see corollary 3.2.13 on the preceding page), and where the adequate α-conversion have been performed to fulfill the side conditions of graft. We check in propositions 3.2.19 and 3.2.20 that this definition is well-founded.

Lemma 3.2.18. Let (E ▹ Γ ⊢ n w ∶ W ) ∶= ⟦ω⟧ ! , with ω ∈ O n non degenerate, n ≥ 2.
Then, by corollary 3.2.13 on the preceding page, for

[l] ∈ ω | , there is a variable a ∈ (s s w) • such that & s s w a = [l]. Proof. By assumption, ω is either of the form Y ψ , or ν ○ [k] Y ψ , for some ν ∈ O n and ψ ∈ O n-1 . From
ω = (⋯ (Y s [p 1 ] ω ○ [p2] Y s [p 2 ] ω ) ○ [p3] Y s [p 3 ] ω ⋯) ○ [p k ] Y s [p k ] ω = (⋯ (Y s [q 1 ] ω ○ [q2] Y s [q 2 ] ω ) ○ [q3] Y s [q 3 ] ω ⋯) ○ [q k ] Y s [q k ] ω . Then ⟦(Y s [p 1 ] ω ○ [p2] Y s [p 2 ] ω ) ⋯ ○ [p k ] Y s [p k ] ω ⟧ ! = ⟦(Y s [q 1 ] ω ○ [q2] Y s [q 2 ] ω ) ⋯ ○ [q k ] Y s [q k ] ω ⟧ !
In other words, ⟦ω⟧ ! does not depend on the decomposition of ω in corollas.

Proof. By assumption, the sequence [p 1 ], . . . , [p k ] (and likewise for [q 1 ], . . . , [q k ]) has the following property: for

1 ≤ i ≤ j ≤ k, either [p i ] ⪯ [p j ] or [p i ] and [p j ] are ⪯-incomparable (recall that ⪯ is the lexicographical order on A n-1 , see section 2.2.3 on page 11). Further, {[p 1 ], . . . , [p k ]} = ω • = {[q 1 ], . . . , [q k ]}. Consequently, the sequence of addresses [q 1 ], . . . , [q k ] can be obtained from [p 1 ], . . . , [p k ] via a sequence of transpositions of consecutive ⪯-incomparable addresses.
It is thus enough to check the following:

for ν ∈ O n , [l], [l ′ ] ∈ ν | (necessarily,
neither is a prefix of the other), and ψ, ψ ′ ∈ O n-1 such that the following graftings are well defined, we have

⟦(ν ○ [l] Y ψ ) ○ [l ′ ] Y ψ ′ ⟧ ! = ⟦(ν ○ [l ′ ] Y ψ ′ ) ○ [l] Y ψ ⟧ ! . Let ⟦ν⟧ ! = (E ν ▹ Γ ν ⊢ x ν ∶ s ν ⊷ X ν )
, and likewise for ψ and ψ ′ , and a, a ′ ∈ (s s ν) • be such that & s s ν a = [l] and & s s ν a ′ = [l ′ ] (see corollary 3.2.13 on page 23). The sequents above are respectively obtained by the following proof trees:

E ν ▹ Γ ν ⊢ x ν ∶ s ν ⊷ X ν E ψ ▹ Γ ψ ⊢ x ψ ∶ s ψ ⊷ X ψ graft-a F ▹ Γ ν ∪ Γ ψ ⊢ x ν (a ← x ψ ) ∶ s ν [s ψ /a] ⊷ X ν E ψ ′ ▹ Γ ψ ′ ⊢ x ψ ′ ∶ s ψ ′ ⊷ X ψ ′ graft-a ′ G ▹ Γ ν ∪ Γ ψ ∪ Γ ψ ′ ⊢ x ν (a ← x ψ )(a ′ ← x ψ ′ ) ∶ s ν [s ψ /a][s ψ ′ /a ′ ] ⊷ X ν E ν ▹ Γ ν ⊢ x ν ∶ s ν ⊷ X ν E ψ ′ ▹ Γ ψ ′ ⊢ x ψ ′ ∶ s ψ ′ ⊷ X ψ ′ graft-a ′ F ′ ▹ Γ ν ∪ Γ ψ ′ ⊢ x ν (a ′ ← x ψ ′ ) ∶ s ν [s ψ ′ /a ′ ] ⊷ X ν E ψ ▹ Γ ψ ⊢ x ψ ∶ s ψ ⊷ X ψ graft-a G ′ ▹ Γ ν ∪ Γ ψ ′ ∪ Γ ψ ⊢ x ν (a ′ ← x ψ ′ )(a ← x ψ ) ∶ s ν [s ψ ′ /a ′ ][s ψ /a] ⊷ X ν
It remains to prove that both those conclusion sequents are equal.

(1) Since by assumptions

[l], [l ′ ] ∈ ν | , we have a ∉ s • ψ ′ and a ′ ∉ s • ψ . Thus x ν (a ← x ψ )(a ′ ← x ψ ′ ) = x ν (a ← x ψ , a ′ ← x ψ ′ ) = x ν (a ′ ← x ψ ′ )(a ← x ψ ). (2) Again, since a ∉ s • ψ ′ and a ′ ∉ s • ψ , we have s ν [s ψ /a][s ψ ′ /a ′ ] = s ν [s ψ ′ /a ′ ][s ψ /a]. (
⟦⟦I ϕ ⟧ ! ⟧ poly n = I ⟦⟦ϕ⟧ ! ⟧ poly n-2 = I ϕ .
(3) With the same notations as in (3.2.16), and by induction, we have,

⟦⟦Y ψ ⟧ ! ⟧ poly n = Y ⟦⟦ψ⟧ ! ⟧ poly n-1 = Y ψ .
(4) With the same notations as in (3.2.17), and by induction, we have

⟦⟦ν ○ [l] Y ψ ⟧ ! ⟧ poly n = ⟦⟦ν⟧ ! ⟧ poly n ○ [&s s ua] ⟦⟦Y ψ ⟧ ! ⟧ poly n = ⟦⟦ν⟧ ! ⟧ poly n ○ [l] ⟦⟦Y ψ ⟧ ! ⟧ poly n = ν ○ [l] Y ψ .
Conversely, we now show that for all sequents (E ▹ Γ ⊢ α ∶ T ) (abbreviated (α ∶ T ) if no ambiguity arise) we have

(E ▹ Γ ⊢ α ∶ T ) = ⟦⟦E ▹ Γ ⊢ α ∶ T ⟧ poly n ⟧ ! up to ≃.
(1) We have that ⟦⟦x ∶ ∅⟧

poly 0 ⟧ ! = ⟦⧫⟧ ! ≃ (x ∶ ∅).
(2) With the same notations as in equation (3.2.5) on page 21, ⟦⟦δ

∶ x ⊷ x ⊷ X⟧ poly n ⟧ ! = ⟦I ⟦x∶X⟧ poly n ⟧ ! ,
and both sequents ⟦I ⟦x∶X⟧ poly n ⟧ ! and (δ ∶ x ⊷ x ⊷ X) are obtained by applying degen to (x ∶ X). Thus

⟦⟦δ ∶ x ⊷ x ⊷ X⟧ poly n ⟧ ! ≃ (δ ∶ x ⊷ x ⊷ X).
(3) Lastly, consider the sequent

(α ∶ x( → y i ← u i ) ⊷ T ) as in equation (3.2.6) on page 21. Then ⟦⟦α ∶ x( → y i ← u i ) ⊷ T ⟧ poly n+1 ⟧ ! = ⟦Y ⟦x⟧ poly n ◯ [&s xyi] ⟦u i ⟧ poly n+1 ⟧ ! ≃ (α ∶ x( → y i ← u i ) ⊷ T ′ ) .
Since T and T ′ are completely determined by x( → y i ← u i ) (see theorem 3.1.8 on page 19), we have that

T = T ′ , whence ⟦⟦α ∶ x( → y i ← u i ) ⊷ T ⟧ poly n+1 ⟧ ! ≃ (α ∶ x( → y i ← u i ) ⊷ T ) . □ 3.3. Examples
In this section, we showcase the derivation of some low dimensional opetopes. On a scale of a proof tree, specifying the context at every step is redundant. Hence we allow omitting it, only having the equational theory on the left of ⊢.

Example 3.3.1 (The arrow). The unique 1-opetope, the arrow, is given by the following simple derivation:

point ⊢ 0 a ∶ ∅ shift ⊢ 1 f ∶ a ⊷ ∅ Example 3.3.2 (Opetopic integers). The set of O 2 of 2-
(n -1) (n)

⇓

The derivation of the opetope 0 is point

⊢ 0 a ∶ ∅ degen ⊢ 1 a ∶ a ⊷ ∅ shift ⊢ 1 0 ∶ a ⊷ a ⊷ ∅
alternatively, we could have used the degen-shift rule. For n ≥ 1, the opetope n is derived as

⋮ ⊢ 1 f 1 ∶ a 1 ⊷ ∅ ⋮ ⊢ 1 f 2 ∶ a 2 ⊷ ∅ graft-a 1 ⊢ 1 f 1 (a 1 ← f 2 ) ∶ a 2 ⊷ ∅ ⋮ ⊢ 1 f 3 ∶ a 3 ⊷ ∅ graft-a 2 ⊢ 1 f 1 (a 1 ← f 2 (a 2 ← f 3 )) ∶ a 3 ⊷ ∅ ⋮ ⊢ 1 f 1 (a 1 ← f 2 (⋯a n-2 ← f n-1 )) ∶ a n-1 ⊷ ∅ ⋮ ⊢ 1 f n ∶ a n ⊷ ∅ graft-a n-1 ⊢ 1 f 1 (a 1 ← f 2 (⋯a n-1 ← f n )) ∶ a n ⊷ ∅ shift ⊢ 1 n ∶ f 1 (a 1 ← f 2 (⋯a n-1 ← f n )) ⊷ a n ⊷ ∅ Example 3.3.3 (A classic). The 3-opetope . . . . ⇓ ⇓ ⇛ . . . . ⇓ is derived as follows. point ⊢ 0 c ∶ ∅ shift ⊢ 1 h ∶ c ⊷ ∅ point ⊢ 0 a ∶ ∅ shift ⊢ 1 i ∶ a ⊷ ∅ graft-c ⊢ 1 h(c ← i) ∶ c[a/c] ⊷ ∅ and c[a/c] = a. Then, ⋮ ⊢ 1 h(c ← i) ∶ a ⊷ ∅ shift ⊢ 2 β ∶ h(c ← i) ⊷ a ⊷ ∅ On the other hand we have point ⊢ 0 b ∶ ∅ shift ⊢ 1 g ∶ b ⊷ ∅ point ⊢ 0 a ∶ ∅ shift ⊢ 1 f ∶ a ⊷ ∅ graft-b ⊢ 1 g(b ← f ) ∶ b[a/b] ⊷ ∅ and b[a/b] = a. Then, ⋮ ⊢ 2 β ∶ h(c ← i) ⊷ a ⊷ ∅ ⋮ ⊢ 1 g(b ← f ) ∶⊷ ∅ shift ⊢ 2 α ∶ g(b ← f ) ⊷ a ⊷ ∅ graft-i ⊢ 2 β(i ← α) ∶ h(c ← i)[g(b ← f )/i] ⊷ a ⊷ ∅
The last grafting is well defined as s i = a = s s α, and h(c

← i)[g(b ← f )/i] = h(c ← g(b ← f )). Finally ⋮ ⊢ 2 β(i ← α) ∶ h(c ← g(b ← f )) ⊷ a ⊷ ∅ shift ⊢ 3 A ∶ β(i ← α) ⊷ h(c ← g(b ← f )) ⊷ a ⊷ ∅ Finally, the complete proof tree is: point ⊢ c ∶ ∅ shift ⊢ h ∶ c ⊷ ∅ point ⊢ a ∶ ∅ shift ⊢ i ∶ a ⊷ ∅ graft-c ⊢ h(c ← i) ∶ a ⊷ ∅ shift ⊢ β ∶ h(c ← i) ⊷ a ⊷ ∅ point ⊢ b ∶ ∅ shift ⊢ g ∶ b ⊷ ∅ point ⊢ a ∶ ∅ shift ⊢ f ∶ a ⊷ ∅ graft-b ⊢ g(b ← f ) ∶ a ⊷ ∅ shift ⊢ α ∶ g(b ← f ) ⊷ a ⊷ ∅ graft-i ⊢ β(i ← α) ∶ h(c ← g(b ← f )) ⊷ a ⊷ ∅ shift ⊢ A ∶ β(i ← α) ⊷ h(c ← g(b ← f )) ⊷ a ⊷ ∅
Example 3.3.4 (A degenerate case). The 3-opetope on the left is derived as on the right:

. ⇓ ⇓ ⇛ . ⇓ point ⊢ a ∶ ∅ shift ⊢ f ∶ a ⊷ ∅ shift ⊢ α ∶ f ⊷ a ⊷ ∅ point ⊢ a ∶ ∅ degen ⊢ δ ∶ a ⊷ a ⊷ ∅ graft-f ⊢ α(f ← δ) ∶ a ⊷ a ⊷ ∅ shift ⊢ A ∶ α(f ← δ) ⊷ a ⊷ a ⊷ ∅ Example 3.3.5 (Another degenerate case). The 3-opetope . . ⇓ ⇓ ⇛ . . ⇓ is derived as follows: point ⊢ b ∶ ∅ shift ⊢ g ∶ b ⊷ ∅ point ⊢ a ∶ ∅ shift ⊢ f ∶ a ⊷ ∅ graft-b ⊢ g(b ← f ) ∶ a ⊷ ∅ shift ⊢ β ∶ g(b ← f ) ⊷ a ⊷ ∅ point ⊢ a ∶ ∅ degen ⊢ a ∶ a ⊷ ∅ shift ⊢ α ∶ a ⊷ a ⊷ ∅ graft-f a = b ⊢ β(f ← α) ∶ g(b ← f )[a/f ] ⊷ a ⊷ ∅ and g(b ← f )[a/f ] = g, with the added equality a = b. ⋮ a = b ⊢ β(f ← α) ∶ g ⊷ a ⊷ ∅ shift a = b ⊢ A ∶ β(f ← α) ⊷ g ⊷ a ⊷ ∅

Python implementation

In this section, we briefly discuss the Python implementation [START_REF] Ho | [END_REF] of the present work. System Opt ! and all required syntactic constructs are implemented in module opetopy.NamedOpetope. The rules are represented by functions point, degen, shift, graft, as well as degenshift for the alternative rule presented in remark 3.1.7 on page 18. 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. # 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 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 on page 15, and present the inference rules in figure 3.5.1 on the next page.

3.5.1. Syntax. The main distinguishing feature of the named approach above is that only source faces of whichever cell is currently being derived are specified:

⋯ ⊢ n x ∶ s x ⊷ s s x ⊷ ⋯
Nonetheless, as proven in proposition 3.2.11 on page 22, all the information about targets remain. To adapt our previous derivation system to opetopic sets, all faces, including targets, need to be explicitly specified. This will be part of the role of rule repr of system OptSet ! . Further, recall that a sequent in system Opt ! :

E ▹ Γ ⊢ t ∶ T.
An opetopic set is a set of opetopic cells, and in a sequent, the context and the equational theory suffice to describe this. Thus, system OptSet ! will only deal with expressions of the form (E ▹ Γ), called opetopic contexts modulo theory (or OCMTs for short).

For example, the OCMT describing the following opetopic set (note that the graphical representation is not unique):

a a a b ⇓α ⇓β h f g h h is given by ⎛ ⎜ ⎝ b = t f, a = t g = t t α = t h = t t β h = t β = t α ▹ a ∶ ∅, b ∶ ∅, t f ∶ ∅, t g ∶ ∅, t t α ∶ ∅, t h ∶ ∅, t t β ∶ ∅ f ∶ a ⊷ ∅, g ∶ a ⊷ ∅, t α ∶ a ⊷ ∅, h ∶ a ⊷ ∅, t β ∶ a ⊷ ∅ α ∶ g(b ← f ) ⊷ a ⊷ ∅, β ∶ h ⊷ a ⊷ ∅ ⎞ ⎟ ⎠
3.5.2. Inference rules. Our derivation system for opetopic sets, presented in figure 3.5.1, has four rules:

(1) repr that takes an opetope in our previous system and makes it into the representable opetopic set of that opetope;

(2) zero that constructs the empty OCMT;

(3) sum that takes the disjoint union of two opetopic sets; (4) glue that identifies cells of an opetopic set. In virtue of the fact that every finite opetopic set is a quotient of a finite sum of representables, those rules should be enough to derive all finite opetopic sets. This is proved in theorem 3.6.15 on page 35.

Introduction of all targets:

This rule takes an opetope (E ▹ Γ ⊢ n x ∶ X), and completes it by adding all the missing cells, i.e. targets, and making it into an OCMT. If x ∈ V n , then

E ▹ Γ ⊢ n x ∶ X repr E ′ ▹ Γ ′ where Γ ′ ∶= Γ ∪ {t k a ∶ s k+1 a ⊷ s k+2 a ⊷ ⋯ | a ∈ V Γ,l , 1 ≤ k ≤ l ≤ n}
, and

E ′ ∶= E ∪ {t a = b | for all b ← a(⋯) occurring in a type in Γ} (3.5.1) ∪ {t t a = t s [] s a | a ∈ V Γ ′ ,k non degen., 2 ≤ k ≤ n} (3.5.2) ∪ {t k+2 a = b | if t k a ∶ b ⊷ b ⊷ ⋯, 0 ≤ k ≤ n -2} . (3.5.3)
Here, t k a = t ⋯ t a is a tagging on the variable a ∈ V l , but for simplicity, we consider it as a variable of its own: t k a ∈ V l-k . By convention, t 0 a ∶= a, and if a = b, then t a = t b, for all a, b ∈ Γ ′ . In line (3.5.2), the source of a is assumed non degenerate, thus s a is a term of the form x(

→ y i ← u i ),
E ▹ Γ glue E ∪ {a = b} ▹ Γ
We also write glue-(a=b) to make explicit that we added {a = b} to the theory. Remark 3.5.4. Akin to Opt ! , in OptSet ! , an OCMT that is equivalent to a derivable one is itself derivable.

Remark 3.5.5. The sum and zero rules may be replaced by the following usum rule (unbiased sum) without changing the set of derivable OCMTs:

for k ≥ 0, (E 1 ▹ Γ 1 ) , . . . , (E k ▹ Γ k ) OCMTs such that Γ i ∩ Γ j = ∅ for all i ≠ j, then E 1 ▹ Γ 1 ⋯ E k ▹ Γ k usum ∑ k i=1 E i ▹ ∑ k i=1 Γ i
3.6. Equivalence with opetopic sets 3.6.1. Opetopic sets from OCTM. Let E ▹ Γ and F ▹ Υ be two OCMTs. Then we write Γ/E for the set V Γ quotiented by the equivalence relation generated by the equational theory E, and likewise for Υ/F . For (E ▹ Γ ⊢ n x ∶ X) a derivable sequent on Opt ! , where x ∈ V n , let (T x ▹ C x ), the OCMT of x, be given by

E ▹ Γ ⊢ n x ∶ X repr T x ▹ C x
We wish to prove that C x /T x carries a natural structure of representable opetopic set. We proceed in 4 steps:

(1) we show that C x /T x is fibered over O via ⟦-⟧ poly (proposition 3.6.1);

(2) we construct the source and target maps, i.e. the structure maps of an opetopic set (proposition 3.6.2);

(3) we show that the opetopic identities of section 2.2.4 on page 13 are satisfied (theorem 3.6.3), and that consequently, C x /T x has the structure of an opetopic set; (4) finally, we show in proposition 3.6.10 on page 33 that C x /T x is in fact a representable opetopic set. From there, we define a structure of opetopic set on an arbitrary OCMT by induction on its proof tree in equations (3.6.11) and (3.6.12) on page 34.

Let a ∈ V Cx,k . If a is not a target, then the sequent (E| a ▹ Γ| a ⊢ k a ∶ A) is also derivable (where (-)| a denotes restriction of contexts and theories to variables occurring in type A, the type of a in Γ), and its proof tree is a subtree of that of x. Thus we have a well-defined opetope ⟦a⟧

poly k ∈ O k . Otherwise, if a = t n-k x, then s a = s n-k+1
x, and define ⟦a⟧

poly k = ⟦s n-k+1 x⟧ poly k . We thus have a map ⟦-⟧ poly ∶ V Cx → O. Proposition 3.6.1. The map ⟦-⟧ poly ∶ V Cx → O factors through C x /T x .
Proof. By construction, the theory

T x identifies variables a, b ∈ V Cx,k only if s a = s b, thus ⟦a⟧ poly k = ⟦s a⟧ poly k = ⟦s b⟧ poly k = ⟦b⟧ poly k . □ For ψ ∈ O k , write (C x /T x ) ψ = {a ∈ V Cx,k | ⟦a⟧ poly k
= ψ} . We now construct source and target maps between those subsets.

(1) (Sources) If (2) (Target) For a ∈ V Cx,k , k > 0, we of course set t(a) = t a, the latter being a variable introduced by the repr rule.

Proposition 3.6.2. Let a ∈ V Cx,k .

(1) For [p] ∈ ⟦a⟧ poly k

• we have ⟦s

[p] a⟧ poly k-1 = s [p] ⟦a⟧ poly k .
(2) We have ⟦t a⟧ Proof. We check the opetopic identities of section 2.2.4 on page 13. Take a ∈ V Cx,k ,

(1) (Inner) Take [p[q]] ∈ ⟦a⟧ poly k

• , and write d = s [p[q]] a. In s a, the variable d occurs as

s a = ⋯, b(c ← d), ⋯ for some b ∈ • and c ∈ (s b) • . Then, [p[q]] = & s a d = & s a b ⋅ [[& s b c]], and thus & s a b = [p] and & s b c = [q]. Finally, s [q] s [p] a = s [q] b = c = t d = t s [p[q]] a.
(2) (Glob1) Assume that a is not degenerate. Then, by definition of T x , we have t t a = t s [] a.

(3) (Glob2) Assume that a is not degenerate, and take [p[q]] ∈ ⟦a⟧ ] → C x /T x having cell x in its image, and since x is a maximum, the map is surjective.

□ ]. We now aim to show that the two are actually isomorphic (proposition 3.6.10 on the next page) by showing that they have the same number of cells: for ω ∈ O, let

Let (E ▹ Γ ⊢ n x ∶ X)
# ω ∶= ∑ ψ∈O # O[ω] ψ = ∑ ψ∈O # O(ψ, ω),
which is a finite number since the slice category O/ω is finite (see the definition of O in section 2.2.4 on page 13). The strategy of the proof of proposition 3.6.10 on the next page is to show that the number of cells in C x /T x is precisely # ⟦x⟧ poly n . We need some preliminary results first.

Proposition 3.6.5.

(1) We have # ⧫ = 1, and # ◾ = 3.

(2) For a non degenerate opetope ω ∈ O n , with n ≥ 2, we have

# ω = 2 + ⎛ ⎝ ∑ [p]∈ω • # s [p] ω ⎞ ⎠ - ⎛ ⎝ ∑ [p[q]]∈ω • # s [q] s [p] ω ⎞ ⎠ (3.6.6) (3) If ω is a degenerate opetope, say ω = I ϕ , then # ω = 2 + # ϕ.
Proof. This is a straightforward enumeration exercise from the definition of O by generators and relations (see section 2.2.4 on page 13), and using opetopic induction (see remark 2.2.3 on page 12). □ Corollary 3.6.7.

Let ω ∈ O n , for n ≥ 1. (1) If ω = Y ψ for some ψ ∈ O n-1 then # ω = 2 + # ψ. (2) If ω = ν ○ [l] Y ψ , for some ν ∈ O n , [l] ∈ ν | , and ψ ∈ O n-1 , then # ω = # ν + # ψ -# e [l] ν. (3.6.8)
Proof.

(1) Using proposition 3.6.5, we have

# ω = 2 + ⎛ ⎝ ∑ [p]∈ω • # s [p] ω ⎞ ⎠ - ⎛ ⎝ ∑ [p[q]]∈ω • # s [q] s [p] ω ⎞ ⎠ = 2 + # ψ.
(2) Using proposition 3.6.5 on the preceding page, we have

# ω = 2 + ⎛ ⎝ ∑ [p]∈ω • # s [p] ω ⎞ ⎠ - ⎛ ⎝ ∑ [p[q]]∈ω • # s [q] s [p] ω ⎞ ⎠ = 2 + ⎛ ⎝ # ψ + ∑ [p]∈ν • # s [p] ν ⎞ ⎠ - ⎛ ⎝ # e [l] ν + ∑ [p[q]]∈ν • # s [q] s [p] ν ⎞ ⎠ = # ν + # ψ -# e [l] ν. □
Examples 3.6.9. Consider the opetopic integer n ∈ O 2 from example 3.3.2 on page 26. We show that # n = 2n+3.

If n = 0, then by definition, # 0

= # I ⧫ = 2 + # ⧫ = 3. If n = 1, then # 1 = # Y ◾ = 2 + # ◾ =
5 by corollary 3.6.7 on the preceding page. Otherwise,

# n = # ((n -1) ○ [ * n-1 ] Y ◾ ) by def. of n = #(n -1) + # ◾ -# e [ * n-1 ] (n -1)
by eq. (3.6.8)

= (2n + 1) + 3 -# ⧫ by ind. = (2n + 1) + 3 -1 = 2n + 3.
As an other example, consider the 3-opetope ω = Y 2 ○ [[ * ]] Y 0 of example 3.3.5 on page 27: . . ] of opetopic sets.

⇓ ⇓ ⇛ . . ⇓ Then, # ω = # (Y 2 ○ [[ * ]] Y 0 ) = # Y 2 + # 0 -# e [[ *
Proof. If x = ⧫, then V Cx = ⧫, while T x = ∅. Thus # C x /T x = 1 = # ⧫ by proposition 3.6.5 on the preceding page. We know by lemma 3.6.4 on the facing page that

C x /T x is a quotient of O[⟦x⟧ poly n
], and we just showed that the two have the same number of cells, namely ]. Assume now that x ∈ V n for n ≥ 2. We proceed by cases on the form of s x.

# ⧫ = 1. Consequently, C x /T x ≅ O[⟦x⟧ poly 0 ]. Likewise, if x = ◾, then V Cx = {⧫, ◾, t ◾}, while T x = ∅. Thus # C x /T x = 3 = # ◾
(1

) If s x = y ∈ V n-1 , then ⟦x⟧ poly n = Y ⟦y⟧ poly n-1 so that # ⟦x⟧ poly n = 2 + # ⟦y⟧
C x /T x = C a /T a + {x, t x} . Consequently, # C x /T x = 2 + # C a /T a = 2 + # ⟦a⟧ poly n-2 = # ⟦x⟧ poly n .
(3) Assume s x = t(a ← y), for some t ∈ T n-1 , a ∈ V n-2 , and y ∈ V n-1 . Let z ∶ t ⊷ ⋯ be a fresh n-variable.

Since all cells of z except z and its targets are also cells of x, we have

C x = C y ∪ (C z -{t k z | 0 ≤ k ≤ n}) + {t k x | 0 ≤ k ≤ n} , while T x is equivalent to T y ∪ T z + {t y = a, t t x = t s [] x}. Since s [] x = s [] z,
C x /T x = C y /T y ∪ C z /T z + {x, t x} -{z, t z}. By hypothesis of the graft rule, C z /T z ∩ C y /T y = C a /T a , thus # C x /T x = # C y /T y + # C z /T z -# C a /T a = # ⟦y⟧ poly n-1 + # ⟦z⟧ poly n -# ⟦a⟧ poly n-2 = # (⟦t⟧ poly n ○ &ta Y ⟦y⟧ poly n-1 ) = # ⟦x⟧ poly n . □ Let (E ▹ Γ) be a derivable OCMT in OptSet ! , a ∈ V Γ,k ,
O[⟦a⟧ poly k ] ≅ → C a /T a → Γ| a /E| a i → Γ/E,
where the middle map comes from the fact that C a = Γ| a up to renaming, and that T a ⊆ E| a . Let now (E ▹ Γ) and (F ▹ Υ) be two OCMTs, and assume by induction that Γ/E and Υ/F have a structure of opetopic set. Then, by definition of rule sum, and for (G ▹ Ξ) given by

E ▹ Γ F ▹ Υ sum G ▹ Ξ
we have Ξ = Γ + Υ, and G = E + F . We endow the quotient Ξ/G with a structure of opetopic set as follows:

Ξ/G ∶= Γ/E + Υ/F. (3.6.11) Let a, b ∈ V Γ,k be such that s a = E s b and t a = E t b. Remark that O[⟦a⟧ poly k ] = O[⟦b⟧ poly k
]. Then, by definition of rule glue, and for (F ▹ Γ) given by E ▹ Γ glue-(a=b) F ▹ Γ we have F = E + {a = b}. We endow the quotient Γ/F with a structure of opetopic set defined by the following coequalizer:

O[⟦a⟧ poly k ] Γ/E Γ/F, ã b
(3.6.12) Proposition 3.6.13. For (E ▹ Γ) a derivable OCMT in OptSet ! , the structure of opetopic set on Γ/E does not depend on the proof tree of (E ▹ Γ).

Proof. The opetopic set Γ/E is given by the following expression that does not depend on the proof tree of (E ▹ Γ):

Γ/E ≅ ∑ k∈N,a∈V Γ,k O[⟦a⟧ poly k ] a ∼ b, ∀a, b ∈ V Γ s.t. a = E b .
Indeed, it holds when (E ▹ Γ) is of the form (T a ▹ C a ), and since other non empty OCMTs are given by application of rules sum and glue, we can show by induction on the proof tree of (E ▹ Γ) that the opetopic set Γ/E doesn't depend on that proof tree! □ 3.6.2. Equivalence. Recall that Ô is the category of opetopic sets, and that Fin Ô is the full subcategory of Ô spanned by finite opetopic sets (see section 2.2.4 on page 13). In this subsection, we provide the last results needed to establish the equivalence between the category of derivable OCMTs and Fin Ô.

For (E ▹ Γ) an OCMT, and a, b ∈ V, the substitution Γ[a/b] is defined in the obvious manner, by applying said substitution to all typings in Γ.

A morphism f ∶ (E ▹ Γ) → (F ▹ Υ) is a (non necessarily bijective) map f ∶ V Γ → V Υ compatible with E and F , such that if x ∶ X is a typing in Γ, then f (x) ∶ f (X) is a typing in Υ,
where f (X) is the result of applying f to every variable in X. Note that this condition implies that f preserves the dimension of variables. Also, if f, g ∶ (E ▹ Γ) → (F ▹ Υ), and if for all x ∈ V Γ we have f (x) = F g(x), then f = g. We write Ctx ! for the category of derivable OCMTs and such morphisms. In a sense, it is the syntactic category of the OptSet ! system. Lemma 3.6.14. Let f ∶ (E ▹ Γ) → (F ▹ Υ) be a morphism of OCMT, and a ∈ V Γ,k . Then ⟦a⟧

poly k = ⟦f (a)⟧ poly k .
Informally, morphisms of OCMTs preserve the "shape" of variables.

Proof. Since there is a unique 0-opetope and a unique 1-opetope, the result holds trivially if k = 0, 1. Assume now k ≥ 2. We proceed by induction on s a.

(1) If s a = b ∈ V k-1 , then ⟦a⟧ poly k = Y ⟦b⟧ poly k-1 = Y ⟦f (b)⟧ poly k-1 = ⟦f (a)⟧ poly k . (2) If s a = b for some b ∈ V k-2 , then ⟦a⟧ poly k = I ⟦b⟧ poly k-2 = I ⟦f (b)⟧ poly k-2 = ⟦f (a)⟧ poly k-2 . (3) If s a = b( → c i ← u i ), we can show by a secondary induction that ⟦u i ⟧ poly k = ⟦f (u i )⟧ poly k
, and

⟦a⟧ poly k = Y ⟦b⟧ poly k-1 ◯ [& s b ci] ⟦u i ⟧ poly k = ⟦f (a)⟧ poly k □
The named stratification functor S ! ∶ Ctx ! → Fin Ô is defined as follows:

S ! ∶ Ctx ! → Fin Ô E ▹ Γ → Γ/E ((E ▹ Γ) f → (F ▹ Υ)) → (Γ/E f → Υ/F ) .
By lemma 3.6.14, f = S ! f ∶ S ! (E ▹ Γ) → S ! (F ▹ Υ) is indeed a morphism of opetopic sets.

Theorem 3.6.15. The stratification functor S ! ∶ Ctx ! → Fin Ô is an equivalence of categories.

Proof. The category im D, consisting of finite opetopic sets of the form Γ/E for some OCMT E ▹ Γ, contains all representables (proposition 3.6.10 on page 33), the initial object (since S ! (▹) is the opetopic set with no cell), and is closed under finite sums (equation (3.6.11) on the preceding page) and quotients (equation (3.6.12) on the facing page). Thus its closure under isomorphism is finitely cocomplete, and equal to the whole category Fin Ô, so S ! is essentially surjective. By definition, S ! is also faithful, and it remains to show that is it full. Let f ∶ S ! (E▹Γ) → S ! (F ▹Υ) be a morphism of opetopic sets. Then, in particular, it is a map f ∶ Γ/E → Υ/F between the set of cells of S ! (E ▹ Γ) and S ! (F ▹ Υ). To prove that it is a morphism of OCMT, we show that

Γ[f (x)/x | x ∈ V Γ ] is a subcontext of Υ modulo F , i.e. that for all typings x ∶ X in Γ, for some x ∈ V k , the type of f (x) in Υ is f (X) modulo F . If (E ▹ Γ)
is the empty OCMT, the result is trivial, so we assume now that this is not the case. Since f is a morphism of opetopic sets, we have f (x) ∈ V Υ,k , and by lemma 3.6.14, ⟦x⟧

poly k = ⟦f (x)⟧ poly k
. We proceed by induction on k.

(1

) If k = 0, then X = ∅. Since f (x) ∈ V Υ,0 , its type is necessarily ∅ = f (X), thus f (x) ∶ f (X) is a typing in Υ. (2) If k = 1, then X = (s [] x ⊷ ∅), and, since f is a morphism of opetopic sets, f (s [] x) = F s [] f (x). Thus f (X) = (f (s [] x) ⊷ ∅) = F (s [] f (x) ⊷ ∅) ,
the latter being the type of f (x) in Υ.

(3) Assume now that k ≥ 2. The type X of x in Γ is by definition X = (s x ⊷ s s x ⊷ ⋯ ⊷ ∅), and the type of t x in Γ is Y ∶= (s s x ⊷ ⋯ ⊷ ∅). By induction, the type of f (t x) in Υ is f (Y ), and since f (t x) = t f (x), and the type of the latter is by definition s s f (x) ⊷ ⋯ ⊷ ∅, we have

(f (s s x) ⊷ ⋯ ⊷ ∅) = f (Y ) = F (s s f (x) ⊷ ⋯ ⊷ ∅) , or in other words, s i f (x) = F f (s i x), for 2 ≤ i ≤ k.
It remains to show that the latter formula holds in the case i = 1 (the case i = 0 is tautological). Towards a contradiction, assume s f (x) ≠ F f (s x). Then there exists [p] ∈ ⟦x⟧

poly k • = ⟦f (x)⟧ poly k • such that s [p] f (x) ≠ F f (s [p]
x), which contradicts the fact that f is a morphism of opetopic sets. Consequently, s f (x) = F f (s x), and f (X) is the type of f (x) in Υ modulo F . Finally, the underlying map f ∶ Γ/E → Υ/F of the morphism of opetopic sets f ∶ S ! (E ▹ Γ) → S ! (F ▹ Υ) is a morphism of OCMT, and S ! is full. □ Proposition 3.6.16. The category Ctx ! has finite colimits, and S ! preserves them.

Proof. The empty OCMT is certainly an initial object of Ctx ! (it is in fact the only one), and the OCMT (E + F ▹ Γ + Υ) obtained by the rule sum is clearly a coproduct of (E ▹ Γ) and (F ▹ Υ). Let now f, g ∶ (E ▹ Γ) → (F ▹ Υ) be two parallel morphism in Ctx ! . Consider the following:

(F ▹ Υ) q∶x →x → (F ∪ {f (x) = g(x) | x ∈ V Γ } G ▹Υ).
Then, G ▹ Υ is derived from F ▹ Υ by repeated application of the glue rule, and by universal property, it is easy to see that it is a coequalizer of f and g in Ctx ! . So, to summarize, Ctx ! contains all finite sums and coequalizers, and it is thus finitely cocomplete. The fact that S ! preserves finite colimits is trivial in the case of initial objects, a consequence of equation (3.6.11) on page 34 for binary sums, and of equation (3.6.12) on page 34 for coequalizers. □ Theorem 3.6.17. We have an equivalence Ô ≃ Mod((Ctx ! ) op , Set), where the latter is the category of (Ctx ! ) opmodels in Set, i.e. finitely continuous functors (Ctx ! ) op → Set and natural transformations 2 .

Proof. We apply Gabriel-Ulmer duality [Adámek andRosický, 1994, Lack andPower, 2009]. The category Ô is finitely locally presentable as it is the presheaf category of a small category. Finite opetopic sets are the finitely presentable objects, thus

Mod ((Ctx ! ) op , Set) ≃ Mod (Fin Ôop , Set) ≃ Ô. □ 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. is derived as follows. First, we derive the cells α, g, and h as opetopes (i.e. in OptSet ! ) to obtain the following sequents:

▹a ∶ ∅, f ∶ a ⊷ ∅, α ∶ f ⊷ a ⊷ ∅ ⊢ 2 α ∶ f ⊷ a ⊷ ∅ ▹c ∶ ∅, g ∶ c ⊷ ∅ ⊢ 1 g ∶ c ⊷ ∅ ▹b ∶ ∅, h ∶ b ⊷ ∅ ⊢ 1 h ∶ b ⊷ ∅ 2
The category of models Mod is sometimes written Lex, for left exact functors.

and applying the repr rule yields respectively:

▹ a ∶ ∅, f ∶ a ⊷ ∅, α ∶ f ⊷ a ⊷ ∅, t f ∶ ∅, t α ∶ a ⊷ ∅, t t α ∶ ∅ ▹ c ∶ ∅, g ∶ c ⊷ ∅, t g ∶ ∅ ▹ b ∶ ∅, h ∶ b ⊷ ∅, t h ∶ ∅.
The proof tree then reads: is derived as follows. First, we derive the cells α and β as opetopes to obtain the following sequents:

⋮ ▹a, f, α ⊢ 2 α repr t t α = t f ▹ a, f, α, t f, t α, t t α ⋮ ▹c, g ⊢ 1 g repr ▹c, g, t g sum t t α = t f ▹ a, f, α, t f, t α, t t α, c, g, t g ⋮ ▹b, h ⊢ 1 h repr ▹b, h, t h sum t t α = t f ▹ a, b, c, t f, t g, t h, t t α f, g, h, t α α glue-(a = c) t t α = t f, a = c ▹ a, b, c, t f, t g, t h, t t α f, g, h, t α α glue-(b = t f ) t t α = t f, a = c, b = t f ▹ a, b, c, t f, t g, t h, t t α f, g, h, t α α glue-(b = t g) t t α = t f, a = c, b = t f, b = t g ▹ a, b, c, t f, t g, t h, t t α f, g, h, t α α glue-(a = t h) t t α = t f, a = c, b = t f, b = t g, a = t h ▹ a, b, c, t f, t g, t h, t t α f, g, h, t α α glue-(g = t α) t t α = t f, a = c, b = t f, b = t g, a = t h g = t α ▹ a,
▹ a ∶ ∅, b ∶ ∅ f ∶ a ⊷ ∅, g ∶ a ⊷ ∅ α ∶ g(b ← f ) ⊷ a ⊷ ∅ ⊢ 2 α ∶ g(b ← f ) ⊷ a ⊷ ∅ ▹ a ′ ∶ ∅ h ∶ a ′ ⊷ ∅ β ∶ h ⊷ a ′ ⊷ ∅ ⊢ 2 β ∶ h ⊷ a ′ ⊷ ∅
Applying the repr rule yields respectively:

b = t f, t g = t t α ▹ a ∶ ∅, b ∶ ∅, t f ∶ ∅, t g ∶ ∅, t t α ∶ ∅ f ∶ a ⊷ ∅, g ∶ a ⊷ ∅, t α ∶ a ⊷ ∅ α ∶ g(b ← f ) ⊷ a ⊷ ∅ t h = t t β ▹ a ′ ∶ ∅, t h ∶ ∅, t t β ∶ ∅ h ∶ a ′ ⊷ ∅, t β ∶ a ′ ⊷ ∅ β ∶ h ⊷ a ′ ⊷ ∅ The proof tree then reads: ⋮ ▹ a ∶ ∅, b ∶ ∅ f ∶ a ⊷ ∅, g ∶ a ⊷ ∅ α ∶ g(b ← f ) ⊷ a ⊷ ∅ ⊢2 α ∶ g(b ← f ) ⊷ a ⊷ ∅ repr b = t f, t g = t t α ▹ a, b, t f ∶ ∅, t g ∶ ∅, t t α ∶ ∅ f, g, t α ∶ a ⊷ ∅ α glue-(a = t g) b = t f, a = t g = t t α ▹ a, b, t f, t g, t t α f, g, t α α ⋮ ▹ a ′ ∶ ∅ h ∶ a ′ ⊷ ∅ β ∶ h ⊷ a ′ ⊷ ∅ ⊢2 β ∶ h ⊷ a ′ ⊷ ∅ repr t h = t t β ▹ a ′ , t h ∶ ∅, t t β ∶ ∅ h, t β ∶ a ′ ⊷ ∅ β glue-(h = t β) t h = t t β h = t β ▹ a ′ , t h, t t β h, t β β glue-(a ′ = t h) a ′ = t h = t t β h = t β ▹ a ′ , t h, t t β h, t β β sum b = t f, a = t g = t t α, a ′ = t h = t t β h = t β ▹ a, b, t f, t g, t t α, a ′ , t h, t t β f, g, t α, h, t β α, β glue-(a = a ′ ) b = t f, a = t g = t t α = a ′ = t h = t t β h = t β ▹ a, b, t f, t g, t t α, a ′ , t h, t t β f, g, t α, h, t β α, β glue-(t α = h) b = t f, a = t g = t t α = a ′ = t h = t t β h = t β = t α ▹ a, b, t f, t g, t t α, a ′ , t h, t t β f, g, t α, h, t β α, β
Write (E ▹ Γ) for the final OCMT of this proof tree. At the beginning of section 3.5.1 on page 29, we gave a slightly different OCMT for the same opetopic set:

(F ▹ Υ) ∶= ⎛ ⎜ ⎝ b = t f, a = t g = t t α = t h = t t β h = t β = t α ▹ a ∶ ∅, b ∶ ∅, t f ∶ ∅, t g ∶ ∅, t t α ∶ ∅, t h ∶ ∅, t t β ∶ ∅ f ∶ a ⊷ ∅, g ∶ a ⊷ ∅, t α ∶ a ⊷ ∅, h ∶ a ⊷ ∅, t β ∶ a ⊷ ∅ α ∶ g(b ← f ) ⊷ a ⊷ ∅, β ∶ h ⊷ a ⊷ ∅ ⎞ ⎟ ⎠ .
However, there exists an isomorphism f ∶ (E ▹ Γ) → (F ▹ Υ), defined by mapping a ′ to a, and variables in V Γ -{a ′ } to those in V Υ with the same name. Its inverse it given by mapping a to either a or a ′ , and similarly for the over variables of Υ.

Python implementation

The system OptSet ! is implemented in module opetopy.NamedOpetopicSet of [START_REF] Ho | [END_REF]]. 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.8.1 on the next page. # We first define all relevant variables using system Opt ! . 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(Glue(example_unglued, "a", "c"), "b", "tf"), "b", "tg"), "a", "th"), "g", "talpha")

3.9. The mixed system for opetopic sets

The OptSet ! system, presented in section 3.5 on page 29, suffers from the following drawback: derivations of opetopic sets start with instances of rules zero or repr, the latter requiring a full opetope derivation in system Opt ! (presented in section 3.1 on page 15). This makes derivations somewhat unintuitive, since for an opetopic set X ∈ Ô written as

X = ∑ i O[ω i ]
∼ where ∼ represents some quotient, the opetopes ω i have to be derived in Opt ! first, then the repr rule has to be used on each one to produce the corresponding representables O[ω i ], and only then can the sums and gluing be performed.

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 above schema.

3.9.1. Syntax. The syntax of system OptSet ! m uses sequents from Opt ! (see section 3.1.1 on page 15) and OCMTs from OptSet ! (see section 3.5.1 on page 29). Specifically, we use two types of judgments.

(1) E ▹ Γ, stating that E ▹ Γ is a well formed OCMT.

(2) E ▹ Γ ⊢ t ∶ T , stating that in OCMT E ▹ Γ, the term t is well formed, and has type T . We may also write

E ▹ Γ ⊢ n t ∶ T if t ∈ T n .
3.9.2. Inference rules. We present the inference rules of system OptSet ! m in figure 3.9.1 on the following page. It uses rules point, degen, and graft from system Opt ! , and rules zero, sum, and glue from system OptSet ! . Rule pd is a counterpart to degen, introducing a non degenerate pasting diagram from an OCMT. Lastly, rule shift is a variant of that of system Opt ! , and introduces a new cell from a pasting diagram, along with all its targets. It can be viewed as a fusion of Opt ! 's shift rule and OptSet ! 's repr rule.

x ∈ V Γ,k , then E ▹ Γ, x ∶ X degen E ▹ Γ, x ∶ X ⊢ k+1 x ∶ x ⊷ X Introduction of
. If x ∈ V Γ,k , then E ▹ Γ, x ∶ X pd E ▹ Γ, x ∶ X ⊢ k x ∶ X 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 ! (see section 3.1 on page 15):

for x ∈ V n , t ∈ T n is not degenerate, a ∈ (s t) • such that s a = s s x, then E ▹ Γ ⊢ n t ∶ s 1 ⊷ s 2 ⊷ ⋯ F ▹ Υ ⊢ n x ∶ X graft G ▹ Γ ∪ Υ ⊢ n t(a ← x) ∶ s 1 [s x/a] ⊷ s 2 ⊷ ⋯
where G is the union of E, F , and potentially a set of additional equalities incurred by the substitution s 1 [s x/a]. We also write graft-a to make explicit 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.

If x ∈ V n+1 is such that x ∉ V Γ , then E ▹ Γ ⊢ n t ∶ T shift F ▹ Υ where Υ ∶= Γ ∪ {x ∶ t ⊷ T } ∪ {t i x ∶ s i+1 x ⊷ s i+2 x ⊷ ⋯ | 0 < i ≤
n} by convention, we let t 0 x = x, and where F is defined as follows:

(1) if t is a degenerate term, say t = a, then

F ∶= E ∪ {t i+2 x = t i a | 0 ≤ i ≤ n -1} (3.9.1) (2) if t is not degenerate, say t = y( → z i ← u i ), for some y ∈ V n , → z i ∈ V n-1 , and → u i ∈ T n , then F ∶= E ∪ {t 2 x = t y | if n ≥ 1} ∪ {t a = b | for all b ← a(⋯)
E ▹ Γ glue E ∪ {a = b} ▹ Γ
We also write glue-(a=b) to make explicit that we added {a = b} to the theory. Remark 3.9.2. The sum and zero rules may be replaced by the following usum rule (unbiased sum) without changing the set of derivable OCMTs: for k ≥ 0,

(E 1 ▹ Γ 1 ) , . . . , (E k ▹ Γ k ) OCMTs such that Γ i ∩ Γ j = ∅ for all i ≠ j, then E 1 ▹ Γ 1 ⋯ E k ▹ Γ k usum ∑ k i=1 E i ▹ ∑ k i=1
Γ i Remark 3.9.3. Akin to Opt ! and OptSet ! , in OptSet ! m a sequent or an OCMT that is equivalent to a derivable one is itself derivable.

Equivalence with opetopic sets

The aim of this section is to prove theorem 3.10.4 on page 44, stating that system OptSet ! m precisely derives opetopic sets, in the sense of theorems 3.6.15 and 3.6.17 on page 35 and on page 36. In other words, we prove that the set of derivable OCMTs of systems OptSet ! m and OptSet ! are the same. This is done by rewriting proof trees in OptSet ! to proof trees in OptSet ! m (see proposition 3.10.1) and conversely (see proposition 3.10.3 on page 44).

Throughout this section, the rules of systems Opt ! and OptSet ! will be decorated by a prime, e.g. shift', in order to differentiate them from the rules of system 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.3.1 on page 26) in system Opt ! is represented as on the left, and more concisely as on the right:

point' shift' ▹x ∶ ∅ ⊢ 0 x ∶ ∅ ▹x ∶ ∅, f ∶ x ⊷ ∅ ⊢ 1 f ∶ x ⊷ ∅ point' shift'
If no uncertainty arise, we leave the decoration of the edges implicit, as on the right. Proposition 3.10.1. Every OCMT derivable in system OptSet ! is also derivable in system OptSet ! m . Proof. Recall that a proof tree in system OptSet ! has the following structure:

glue' sum' Opt ! repr'
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 "lifting" the instances of 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:

point' repr' ⟿ point
(2) Likewise, if we have a derivation as on the left, where Π is a proof tree in system Opt ! or OptSet ! , we rewrite it as on the right:

' graft'-a k-1 graft'-a 2 graft'-a 1 Π1 Π2 Π3 Π k ⟿ shift-α graft-a k-1 graft-a 2 graft-a 1 pd pd pd pd repr' repr' repr' repr' Π1 Π2 Π3 Π k
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 convergent (i.e. confluent and terminating), and the normal form of a proof tree in system OptSet ! is a proof tree in system OptSet ! m that derives the same OCMT. □ Lemma 3.10.2. Let (E ▹ Γ) be a derivable OCMT in system OptSet ! m . Then it admits a proof tree of the following form zero, glue sum point, degen, pd graft, shift meaning a proof tree starting with 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.10.1 on the previous page.

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

sum degen-x shift-δ Π1 Π2 E 1 ▹ Γ 1 E 2 ▹ Γ 2 ⟿ degen-x shift-δ sum Π1 Π2 E 1 ▹ Γ 1 E 2 ▹ Γ 2
(2) Likewise, consider a proof tree as on the left. Then, by assumption on rule sum, either x ∈ V Γi,1 or x ∈ V Γi,2 . Without loss of generality, assume the latter holds. Then we rewrite the proof tree as on the right:

glue-(a=b) degen-x shift-δ Π ⟿ degen-x shift-δ glue-(a=b) Π
(3) Likewise, consider a proof tree as on the left of figure 3.10.2. Then, by assumption on rule sum, either

a i-1 ∈ V Γ1 or a i-1 ∈ V Γ2 .
Without loss of generality, assume the latter holds. Then we rewrite the proof tree as on the right of the figure.

shift-α graft-a k-1 graft-a i-1 graft-a 1 sum Π1 Π2 Πi,1 Πi,2 Π k E i,2 ▹ Γ i,2 E i,1 ▹ Γ i,1 ⟿ shift-α graft-a k-1 graft-a i-1 graft-a 1 sum Π1 Π2 Πi,1 Πi,2 Π k E i,2 ▹ Γ i,2 E i,1 ▹ Γ i,1
(4) Likewise, consider a proof tree as on the left of figure 3.10.3 on the next page. Then for 1 ≤ j ≤ k, we have x ∈ V Γj if and only if y ∈ V Γj . Assume x, y ∈ V Γj , and by induction, assume that the last rule instance of Π j is glue-(x=y). Then we rewrite the proof tree as on the right of the figure, where Π ′ j is Π j with the instance of glue-(x=y) removed, if x, y ∈ V Γj , or otherwise Π j .

-α graft-a k-1 graft-a i-1 graft-a 1 glue-(x=y) Π1 Π2 Πi Π k E k ▹ Γ k E i ▹ Γ i E 2 ▹ Γ 2 E 1 ▹ Γ 1 ⟿ shift-α graft-a k-1 graft-a i-1 graft-a 1 glue-(x=y) Π ′ 1 Π ′ 2 Π ′ i Π ′ k □ Proposition 3.10.3. Every OCMT derivable in system OptSet !
m is also derivable in system OptSet ! . Proof. Consider a proof tree in system OptSet ! m . Then, without loss of generality, it has the structure described in lemma 3.10.2 on page 42. Applying the rewriting steps of proposition 3.10.1 on page 41 in reverse direction yields a proof tree in systems Opt ! and OptSet ! that derives the same OCMT. □ Theorem 3.10.4. System OptSet ! m derives opetopic sets, in the sense of theorems 3.6.15 and 3.6.17 on page 35 and on page 36. Proof. By propositions 3.10.1 and 3.10.3 on page 41 and on the current page, the OCMTs derived by system OptSet ! m and OptSet ! are the same. □

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. of example 3.7.1 on page 36 can be derived as follows. The first half of the proof tree is on the left, and the second half on the right. Moreover, for clarity, we do not repeat the typing of previously typed variables

point ▹ a ∶ ∅ pd ▹ a ⊢0 a shift ▹ a, t f ∶ ∅ f ∶ a ⊷ ∅ pd ▹ a, t f f ⊢0 a shift ▹ a, t f f, g ∶ a ⊷ ∅ point ▹ b ∶ ∅ pd ▹ b ⊢0 b shift ▹ b, t h ∶ ∅ h ∶ b ⊷ ∅ sum ▹ a, b, t f, t g, t h f, g, h (b= t f ) b = t f ▹ a, b, t f, t g, t h f, g, h (b= t g) b = t f = t g ▹ a, b, t f, t g, t h f, g, h ⋮ pd b = t f = t g ▹ a, b, t f, t g, t h f, g, h ⊢1 f shift b = t f = t g = t 2 α ▹ a, b, t f, t g, t h, t 2 α ∶ ∅ f, g, h, t α ∶ a ⊷ ∅ α ∶ f ⊷ a ⊷ ∅ (g= t α) b = t f = t g = t 2 α g = t α ▹ a, b, t f, t g, t h, t 2 α ∶ ∅ f, g, h, t α ∶ a ⊷ ∅ α ∶ f ⊷ a ⊷ ∅ (a= t h) b = t f = t g = t 2 α, a = t h g = t α ▹ a, b, t f, t g, t h, t 2 α ∶ ∅ f, g, h, t α ∶ a ⊷ ∅ α ∶ f ⊷ a ⊷ ∅
where rules of the form (x = y) are shorthands for glue-(x = y).

Example 3.11.2. The opetopic set a a a b ⇓α ⇓β h f g h h of example 3.7.2 on page 37 can be derived as follows.

point ▹ a ∶ ∅ point ▹ b ∶ ∅ sum ▹ a, b pd ▹ a, b ⊢0 a ∶ ∅ shift ▹ a, b, t f ∶ ∅ f ∶ a ⊷ ∅ glue-(b = t f ) b = t f ▹ a, b, t f f pd b = t f ▹ a, b, t f f ⊢0 t f ∶ ∅ shift b = t f ▹ a, b, t f, t g ∶ ∅ f, g ∶ t f ⊷ ∅ pd b = t f ▹ a, b, t f, t g f, g ⊢0 a ∶ ∅ shift b = t f ▹ a, b, t f, t g, t h ∶ ∅ f, g, h ∶ a ⊷ ∅ pd b = t f ▹ a, b, t f, t g, t h f, g, h ⊢1 g ∶ t f ⊷ ∅ graft b = t f ▹ a, b, t f, t g, t h f, g, h ⊢1 g(t f ← f ) ∶ a ⊷ ∅ shift b = t f = t t α ▹ a, b, t f, t g, t h, t t α ∶ ∅ f, g, h, t α ∶ a ⊷ ∅ α ∶ g(t f ← f ) ∶ a ⊷ ∅ glue-(h = t α) b = t f = t t α g = t α ▹ a, b, t f, t g, t h, t t α f, g, h, t α α glue-(a = t g) b = t f = t t α, a = t g g = t α ▹ a, b, t f, t g, t h, t t α f, g, h, t α α glue-(a = t h) b = t f = t t α, a = t g = t h g = t α ▹ a, b, t f, t g, t h, t t α f, g, h, t α α pd b = t f = t t α, a = t g = t h g = t α ▹ a, b, t f, t g, t h, t t α f, g, h, t α α ⊢1 h ∶ a ⊷ ∅ shift b = t f = t t α, a = t g = t h = t t β g = t α ▹ a, b, t f, t g, t h, t t α, t t β ∶ ∅ f, g, h, t α, t β ∶ a ⊷ ∅ α, β ∶ h ⊷ a ⊷ ∅ glue-(h = t β) b = t f = t t α, a = t g = t h = t t β g = t α, f = t β = h ▹ a, b, t f, t g, t h, t t α, t t β f, g, h, t α, t β α, β
3.12. Python implementation

The system OptSet ! m is implemented in module opetopy.NamedOpetopicSetM of [START_REF] Ho | [END_REF]]. Its usage is very similar to that of opetopy.NamedOpetope and opetopy.NamedOpetopicSet, presented in sections 3.4 and 3.8 on page 28 and on page 38 respectively. Figure 3.12.1. Derivation of example example 3.7.1 on page 36 using opetopy.NamedOpetopicSetM from NamedOpetopicSetM import Glue, Pd, Point, RuleInstance, Shift, Sum # We first derive the f , g components p1 = Shift(Pd(Point("a"), "a"), "f") p1 = Shift(Pd(p1, "a"), "g") # We then derive the h component p2 = Shift(Pd(Point("b"), "b"), "h") # We proceed to sum the two, glue some cells, and introduce alpha example = Sum(p1, p2) # type: RuleInstance example = Glue(example, "b", "tf") example = Glue(example, "b", "tg") example = Shift(Pd(example, "f"), "alpha") example = Glue(example, "b", "ttalpha") example = Glue(example, "g", "talpha") example = Glue(example, "a", "th") CHAPTER 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 on page 11 to identify cells, rather than names as in the named approach. For example, recall the opetope 3 ∈ O 2 from example 2.2.1 on page 12, drawn on the left, with its underlying Z 0 -tree represented on the right: . . .

.

⇓ ⟿ ◾ ◾ ◾ ⧫ ⧫ ⧫ ⧫ * * * [] [ * ] [ * * ]
In the unnamed approach for opetopes presented in this section, 3 will be encoded as a mapping from its set of node addresses 3

• = {[], [ * ], [ * * ]} to the set of 1-opetopes O 1 as follows: 3 ⟿ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← ◾ [ * ] ← ◾ [ * * ] ← ◾
The 1-opetope ◾ can recursively be encoded by { * ← ⧫ , which give a complete expression of 3:

⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← { * ← ⧫ [ * ] ← { * ← ⧫ [ * * ] ← { * ← ⧫
This example will be treated in depth in example 4.3.2 on page 55. In a similar manner, the opetope ω on the left, whose tree is given in the middle, can be encoded as on the right:

. . . . ⇓ ⇓ ⇛ . . . . ⇓ ⟿ 2 2 ◾ ◾ ◾ ◾ ◾ [] [[ * ]] [ * ] [ ] [ ] [ * ] ⟿ { [] ← 2 [[ * ]] ← 2
Similarly to 3, the opetope 2 can be expressed by

{ [] ← ◾ [ * ] ← ◾
, and recall that ◾ can be expressed by { * ← ⧫ . We thus have a complete encoding of ω as:

ω ⟿ ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← { [] ← { * ← ⧫ [ * ] ← { * ← ⧫ [[ * ]] ← { [] ← { * ← ⧫ [ * ] ← { * ← ⧫ 47
This example is fully treated in example 4.3.3 on page 55.

4.1.1. Preopetopes. Now we define the set P n of n-preopetopes by the following grammar:

P -1 ::= ∅ by convention

P 0 ::= ⧫ P n ::= ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ A n-1 ← P n-1 ⋮ A n-1 ← P n-1 n ≥ 1 (4.1.1) | {{P n-2 n ≥ 2 (4.1.2)
where the set A n of n-addresses is defined in section 2.2.3 on page 11. In line (4.1.1), we require further that there is at least one (n -1)-address, and that all addresses are distinct. Further, a preopetope of this form is considered as a set of expressions A n-1 ← P n-1 rather than a list: for instance, the following two (n + 1)-preopetopes are equal

{ [p 1 ] ← p 1 [p 2 ] ← p 2 = { [p 2 ] ← p 2 [p 1 ] ← p 1 for any distinct n-addresses [p 1 ], [p 2 ] ∈ A n , and any p 1 , p 2 ∈ P n .
Here are examples of a 1, 2, 3, and 4-preopetope respectively:

{ * ← ⧫ { [] ← { * ← ⧫ [ * * * * * ] ← { * ← ⧫ { [[ * ]] ← {{⧫ [[ * * ][ * ][]] ← {[] ← { * ← ⧫ {{{{⧫
As mentioned in the introduction of this chapter, the first corresponds to the unique 1-opetope ◾. We will see that the second does not correspond to an actual opetope, as it is impossible for a 2-opetope to only contain An n-preopetope p is degenerate if it is of the form of line (4.1.2), it is non-degenerate otherwise; we write dim p = n for its dimension. There is a unique 1-preopetope { * ← ⧫ , which we write ◾. If we have a non-degenerate n-preopetope of the form and [p[q]] / ∈ p • . We write p | ⊆ A n-1 for the set of leaves of p. By convention, if p is degenerate, we set p • ∶= ∅ and p | ∶={[]}, and furthermore, ⧫ • = ⧫ | ∶= ∅. Definition 4.1.4 (Improper grafting). Let p be an n-preopetope as in equation (4.1.3), and q be an (n -1)preopetope

p = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [p 1 ] ← q 1 ⋮ [p k ] ← q k (4.1.3) we call [p 1 ], . . . , [p k ] the source addresses of p (or just sources), we write p • ∶={[p 1 ], . . . , [p k ]} ⊆ A n-1 the set of addresses of p, and s [pi] p ∶= q i the [p i ]-source of p. Assume n ≥ 2. A leaf of p is an (n -1)-address of the form [p[q]] such that [p] ∈ p • , [q] ∈ (s [p] p) • ,
. If [r] ∈ p | is a leaf address of p, write p ○ [r] q ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [p 1 ] ← q 1 ⋮ [p k ] ← q k [r] ← q
and call p ○[r] q the improper grafting of q on p at address [r]. By convention, the grafting operation is associative on the right.

For example,

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← { [] ← { * ← ⧫ [ * ] ← { * ← ⧫ [[ * ]] ← { [] ← { * ← ⧫ [ * ] ← { * ← ⧫ = {[] ← { [] ← { * ← ⧫ [ * ] ← { * ← ⧫ ○ [[ * ]] { [] ← { * ← ⧫ [ * ] ← { * ← ⧫
which, together with the introduction of this chapter, means that graphically,

⎛ ⎜ ⎜ ⎝ . . . . ⇓ ⇓ ⇛ . . . . ⇓ ⎞ ⎟ ⎟ ⎠ = ⎛ ⎜ ⎜ ⎝ . . . ⇓ ⇛ . . . ⇓ ⎞ ⎟ ⎟ ⎠ ○ [[ * ]]
. .

.

⇓

The denomination "improper" is motivated by the fact that p and q do not have the same dimension. A definition of "proper" grafting is given for polynomial trees in section 2.1 on page 9. Any preopetope can be obtained by iterated improper grafting as follows.

Lemma 4.1.5. Let p be an n-preopetope as in equation (4.1.3) on the preceding page, and assume that whenever

1 ≤ i < j ≤ k, we have either [p i ] ⊑ [p j ], or [p i ] and [p j ] are ⊑-incomparable (in particular, this condition is satisfied if the [p i ]'s are lexicographically sorted). Then p ∶= (⋯ ({[p 1 ] ← q 1 ) ○ [p2] q 2 ⋯) ○ [p k ] q k .
Proof. The condition on the sequence [p 1 ], . . . , [p k ] guarantees that the successive improper graftings are welldefined. □ 4.1.2. Inference rules. We now introduce a typing system for preopetopes in order to characterize those corresponding to opetopes, which is formally shown in theorem 4.2.4 on page 54. We will deal with sequents of the form Γ ⊢ p → t, where p is an n-preopetope, t is an (n -1)-preopetope, and the context Γ is a finite set of pairs consisting of addresses [l] ∈ p | and [q] ∈ t • , denoted by [l] [q] . The preopetope p is the real object of interest, and as we will see in subsequent results, we may think of t as the "target" of p, while Γ establishes a bijection between the leaves of p and the nodes of its target.

The operation of substitution, which consists in replacing a node by a pasting scheme in an opetope, can be defined as follows in our formalism. Definition 4.1.6 (Substitution). Let t be a non degenerate n-preopetope, and Υ ⊢ q → u be a sequent, where q is an n-preopetope as well. Write t as

t = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [t 1 ] ← w 1 ⋮ [t l ] ← w l For [t i ] ∈ t • , we define t ◽ [ti]
q, the substitution by q in t at [t i ], as follows:

(1) if l = 1 and q is degenerate, then t ◽ [t1] q = q;

(2) if l ≥ 2 and q is degenerate, then

t ◽ [ti] q ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ χ[t 1 ] ← w 1 ⋮ χ[t i-1 ] ← w i-1 χ[t i+1 ] ← w i+1 ⋮ χ[t l ] ← w l where χ[t j ] ∶= { [t i ⋯] if [t j ] = [t i []⋯] [t j ] otherwise,
(3) if l ≥ 2, and q is not degenerate, write it as

q = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [q 1 ] ← v 1 ⋮ [q k ] ← v k and define t ◽ [ti] q ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ χ[t 1 ] ← w 1 ⋮ χ[t i-1 ] ← w i-1 [t i q 1 ] ← v 1 ⋮ [t i q k ] ← v k χ[t i+1 ] ← w i+1 ⋮ χ[t l ] ← w l where χ[t j ] ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ [t i a⋯] if [t j ] = [t i [b]⋯] for some [a] [b] ∈ Υ, [t j ]
otherwise.

This operation relies on the context Υ, which we leave implicit. By convention, ◽ is associative on the left.

Refer to section 4.3 on page 54 for examples of applications of this construction. We now state the inference rules of our unnamed system Opt ? in figure 4.1.1.

Introduction of points

: point ⊢ ⧫ → ∅ Introduction of degeneracies: Γ ⊢ p → t degen [] [] ⊢ {{p → {[] ← p If dim p = n, remark that dim ({{p ) = n + 2, and that dim ({[] ← p ) = n + 1. Shift to the next dimension: Assume p • = {[p 1 ], . . . , [p k ]}. Γ ⊢ p → t shift [[p1]] [p1] , . . . , [[p k ]] [p k ] ⊢ {[] ← p → p As in the previous rule, if dim p = n, then dim ({[] ← p ) = n + 1. Grafting: Assume dim p = n ≥ 2, dim q = n -1, q • = {[s 1 ], . . . , [s l ]}, and s [q] s [p] p = u. Γ, [p[q]] [r] ⊢ p → t Υ ⊢ q → u graft Γ ′ , [p[q][s1]] [rs1] , . . . , [p[q][s l ]] [rs l ] ⊢ p ○ [p[q]] q → t ◽ [r]
q where Γ ′ is given by pairs of the form (1) [a] [rxr ′ ] , where [a] [r[y]r ′ ] ∈ Γ and [x] [y] ∈ Υ, (2) [a] [b] , where [a] [b] ∈ Γ is not as above (i.e. [b] not of the form [r[y]r ′ ] for some [x] [y] ∈ Υ). 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.1.7. The transformation of context defined in rule graft in figure 4.1.1 might look complicated and unintuitive. And indeed it is, but we try to explain its purpose. Let Γ ⊢ p → t be a derivable sequent in Opt ? , with p ∈ P n . As proved in lemma 4.1.9 on the facing page, Γ exhibits a bijection between p | and t • . In theorem 4.2.4 on page 54, we prove that p corresponds uniquely to an n-opetope ω = ⟦p⟧ poly , that t ω = ⟦t⟧ poly , and that Γ corresponds to the readdressing function ℘ ω ∶ ω | → (t ω)

• (see section 2.1.1 and appendix A.1 on page 10 and on page 71).

We now turn our attention to the named approach of chapter 3 on page 15. Applying theorem 3.2.22 on page 25, we know that ω corresponds to a unique sequent (modulo variable renaming)

E ▹ Υ ⊢ n x ∶ s x ⊷ s 2 x ⊷ ⋯ ⊷ ∅
where x ∈ V. More precisely, considered as a tree, ω is encoded by the term s x, and by proposition 3.2.11 on page 22, t ω is encoded by s 2 x. In lemma 3.2.10 on page 22, we show that ℘ ω exhibits a bijection

{& s x b | b ∈ V n-2 , b ∈ (s 2 x) • } ℘ω → {& s 2 x b | b ∈ V n-2 , b ∈ (s 2 x) • } .
Say that a node of the term s 2 x is a variable b ∈ (s 2 x) • , while a leaf of s x is a variable that can be used for grafting (see rule graft in figure 3.1.1 on page 17), i.e. a variable b ∈ (s 2 x) • . Then left hand side can be considered as the set of leaf addresses of s x, while the right hand side is its set of node addresses of s 2 x, and ℘ ω maps the address of b ∈ V n-2 as a leaf of s x to the address of b as a node of s 2 x. But here, the function ℘ ω is unnecessary: this correspondence is already established by the name of the variables!

In Opt ? however, such bookkeeping is paramount since there is no such things as names. Based on the previous discussion, we conclude that Γ is precisely the desired correspondence.

We now prove basic properties of derivable sequents in Opt ? . 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

p shift {[] ← p Lemma 4.1.8. If Γ ⊢ p → t is a derivable sequent, then dim p = dim t + 1.
Proof. We proceed by induction. The only non trivial case is graft.

Remark that dim (p ○[p[q]] q) = dim p = dim q + 1 = dim (t ◽ [r] q) + 1.
□ Lemma 4.1.9. Let Γ ⊢ p → t be a derivable sequent with dim p ≥ 2. Then Γ establishes a bijection between p | and t • (i.e. as a set of pairs, Γ is the graph of a bijective function).

Proof. The fact that Γ is a relation from p | to t • (i.e. that whenever [a] [b] ∈ Γ we have [a] ∈ p | and [b] ∈ t • ) is clear from the inference rules. It is also clear that Γ is a function (i.e. that whenever [a] [b] ,

[a ′ ] [b ′ ] ∈ Γ we have [a] ≠ [a ′ ]
). Finally, the fact that it is a bijection is clear in the case of degen and shift, and is a routine verification in the case of graft. □ Proposition 4.1.10. If Γ ⊢ p → t is derivable, then t is too.

Proof. The only non obvious case is (as always) graft, where we have to show that t ◽ [r] q is derivable. Since the sequent Γ, [p[q]]

[r]

⊢ p → t has a non empty context, p and t are non-degenerate. Write t and q as in definition 4.1.6 on page 49. Up to reindexing, assume that χ[t j ] = [t j ] if and only if j < i. Assume moreover that the sequence [t 1 ], . . . , [t i-1 ] is lexicographically ordered, and likewise for [t i+1 ], . . . , [t l ]. For j > i write

[t j ] = [t i [b j ]x j ] and ℘[t j ] = [t i a j x j ], so that Υ = { [aj ] [bj ] } i<j≤l .
Then the proof tree of t ◽ [ti] q is sketched as follows:

(1) If [t i ] = [], then necessarily i = 1, and t ◽ [ti] q is derived as follows:

⋮ q ⋮ v 2 graft-[a 2 x 2 ] q ○[a2x2] v 2 ⋮ v 3 graft-[a 3 x 3 ] (q ○[a2x2] v 2 ) ○[a3x3] v 3 ⋮ (⋯ (q ○[a2x2] v 2 ) ⋯) ○[a l-1 x l-1 ] v l-1 ⋮ v l graft-[a l x l ] (⋯ (q ○[a2x2] v 2 ) ⋯) ○[a l x l ] v l and by definition, (⋯ (q ○[a2x2] v 2 ) ⋯) ○[a l x l ] v l = t ◽ [ti] q.
(2) If [t i ] ≠ [], then necessarily i > 1, and moreover [t 1 ] = []. The process goes similarly: we first derive

⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [t 1 ] ← v 1 ⋮ [t i-1 ] ← v i-1
, then graft the sources of q, and lastly graft the remaining v j 's, where j > i. □ Proposition 4.1.11. Let Γ 1 ⊢ p → t 1 and Γ 2 ⊢ p → t 2 be two derivable sequents. Then Γ 1 = Γ 2 and t 1 = t 2 .

Proof. If p is ⧫, of the form {{q , or of the form {[] ← q , then the result is clear, as both sequents have been obtained by point, degen, or shift respectively. Otherwise, both sequents have been obtained by an instance of the graft rule, so p has at least two addresses:

# p • ≥ 2. Assume # p • = 2, and write p = { [] ← q 1 [[q]] ← q 2
, for

[q] ∈ q • 1 . Note that, by induction, the sequents around q 1 and q 2 are uniquely determined. Then p has necessarily been derived as

⋮ q 1 shift {[] ← q 1 ⋮ q 2 graft-[[q]
] p whence Γ 1 = Γ 2 and t 1 = t 2 in this case. Assume now # p • > 2, and that the two contexts in the proposition statement have been derived as

⋮ p 1 ⋮ q 1 graft-[l 1 ] Γ 1 ⊢ p → t 1 ⋮ p 2 ⋮ q 2 graft-[l 2 ] Γ 2 ⊢ p → t 2
Note that, by induction again, the sequents around p i and q i , i = 1, 2, are uniquely determined. Then p 1 is p with address [l 1 ] removed, and [l 2 ] ∈ p • 1 is an address "close to the leaves", in that

∀[p] ≠ [l 1 ] ∈ p • 1 we have [l 1 ] ⋤ [p]. Likewise for p 2 . If [l 1 ] = [l 2 ],
then obviously the result holds, as both sequents have the same derivation tree. Otherwise, let a be p with addresses [l 1 ] and [l 2 ] removed. Then a is a "common ancestor" to p 1 and p 2 :

⋮ a ⋮ q 2 graft-[l 2 ] p 1 ⋮ a ⋮ q 1 graft-[l 1 ] p 2
Again, the sequent around a is uniquely determined by induction. From there, Γ 1 = Γ 2 , and t 1 = t 2 follow by routine verifications. □

We denote by P ✓ n the set of derivable n-preopetopes, i.e. the n-preopetopes p such that there exists a derivable sequent Γ ⊢ p → t. By proposition 4.1.11, this sequent is uniquely determined by p, so let t p = t be the target of p, and ℘ p ∶ p | ≅ → t • be the bijection described by Γ. As such, the sequent around a derivable opetope p can be reconstructed as ℘ p ⊢ p → t p. Remark 4.1.12. Our syntax is closely related to the one given for multitopes [Hermida et al., 2002, Section 3], called here Hmp. Briefly, in Hmp, the unique 0 and 1-opetopes are respectively denoted ☀ and # and, given an n-opetope p, the notation [p] (resp. ⌜ p ⌝ ) is used for the corresponding degenerated (resp. shifted) (n + 2) (resp.

(n + 1)) opetope. The nodes of an opetope come equipped with a canonical order (just as in our system we could require preopetopes to be always sorted according to the lexicographical order ⪯), which apparently dispenses from using addresses. In Hmp, an inductive definition of opetopes is given, in the same spirit as our sequent calculus: in particular, typing conditions involving targets when grafting opetopes (grafting is simply application in Hmp) are involved. However, no explicit definition at the level of the syntax is given for computing targets (the description given resorts to multicategorical composition), and it is not clear to us how to define it without considering addresses and maintaining more information, as we do with our sequent calculus.

Equivalence with polynomial opetopes

We now show theorem 4.2.4 on page 54, stating that the elements of P ✓ n are in bijective correspondence with the set O n of polynomial n-opetopes. To this end, we now construct a bijection ⟦-⟧ ? ∶ O n → P ✓ n . If n = 0, 1, then both sets are singletons, so that ⟦-⟧ ? is trivially defined. Assume n ≥ 2, and that ⟦-⟧ ? is defined for k < n. Recall that O n = tr Z n-2 . We distinguish three cases: Example 4.3.2 (Opetopic integers). As in example 3.3.2 on page 26, we provide the derivation of opetopic integers n ∈ O 2 . The derivation of 0 is given on the left, whereas for n ≥ 1, the opetope n is derived as on the right:

point ⊢ ⧫ degen [] [] ⊢ {{⧫ → ◾ ⋮ ⊢ ◾ → ⧫ shift [ * ] * ⊢ {[] ← ◾ → ◾ ⋮ ⊢ ◾ → ⧫ [ * ] [ * * ] * ⊢ { [] ← ◾ [ * ] ← ◾ → ◾ ⋮ ⊢ ◾ → ⧫ [ * * ] [ * * * ] * ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← ◾ [ * ] ← ◾ [ * * ] ← ◾ → ◾ ⋮ [ * n-1 ] * ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← ◾ ⋮ [ * n-2 ] ← ◾ → ◾ ⋮ ⊢ ◾ → ⧫ [ * n-1 ] [ * n ] * ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← ◾ ⋮ [ * n-1 ] ← ◾ → ◾ where * n = * ⋯ * n
, and where there is a total of n -1 instances of the graft rule. . .

. ⇓ ⋮ [ * * ] * ⊢ 2 → ◾ shift [[ * ]] [ * ] ⊢ {[] ← 2 → 2 ⋮ [ * * ] * ⊢ 2 → ◾ graft-[[ * ]] [[]] [] , [[ * ][]] [ * ] , [[ * ][ * ]] [ * * ] ⊢ { [] ← 2 [[ * ]] ← 2 → 3
Example 4.3.4 (A degenerate case). The 3-opetope on the left is derived as on the right:

.

⇓ ⇓ ⇛ . ⇓ ⋮ [ * ] * ⊢ 1 → ◾ shift [[]] [] ⊢ {[] ← 1 → 1 ⋮ [] [] ⊢ 0 → ◾ graft-[[]] ⊢ { [] ← 1 [[]] ← 0 → 0
Example 4.3.5 (Another degenerate case). The 3-opetope on the left is derived as on the right:

. .

⇓ ⇓ ⇛ . . ⇓ ⋮ [ * * ] * ⊢ 2 → ◾ shift [[]] [] , [[ * ]] [ * ] ⊢ {[] ∶ 2 → 2 ⋮ ⊢ 0 → ◾ graft-[[ * ]] [[]] [] ⊢ { [] ← 2 [[ * ]] ← 0 → 1
⋮ [ * * * ] * ⊢ 3 → ◾ s [[]] [] , [[ * ]] [ * ] , [[ * * ]] [ * * ] ⊢ {[] ← 3 → 3 ⋮ [ * * ] * ⊢ 2 → ◾ [[ * ]] [[]] [] , [[ * * ]] [ * * * ] , [[ * ][]] [ * ] , [[ * ][ * ]] [ * * ] ⊢ { [] ← 3 [[ * ]] ← 2 → 4 ⋮ [ * * ] * ⊢ 2 → ◾ [[ * ][ * ]] [[]] [] , [[ * * ]] [ * * * * ] , [[ * ][]] [ * ] , [[ * ][ * ][]] [ * * ]
,

[[ * ][ * ][ * ]] [ * * * ] ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 2 [[ * ][ * ]] ← 2 → 5 ⋮ [ * ] * ⊢ 1 → ◾ [[ * ][ * ][]] [[]] [] , [[ * * ]] [ * * * * ] , [[ * ][]] [ * ] , [[ * ][ * ][ * ]] [ * * * ]
,

[[ * ][ * ][][]] [ * * ] ⊢ ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 2 [[ * ][ * ]] ← 2 [[ * ][ * ][]] ← 1 → 5 s [[]] [] , [[[ * ]]] [[ * ]] , [[[ * ][ * ]]] [[ * ][ * ]] , [[[ * ][ * ][]]] [[ * ][ * ][]] ⊢ ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 2 [[ * ][ * ]] ← 2 [[ * ][ * ][]] ← 1 → ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 2 [[ * ][ * ]] ← 2 [[ * ][ * ][]] ← 1 ⋮ [ * ] * ⊢ 1 → ◾ s [[]] [] ⊢ {[] ← 1 → 1 ⋮ [ * * ] * ⊢ 2 → ◾ [[]] [[][]] [] , [[][ * ]] [ * ] ⊢ { [] ← 1 [[]] ← 2 → 2 [[[ * ]]] [[]] [] , [[[ * ][ * ]]] [[ * ][][ * ]] , [[[ * ][ * ][]]] [[ * ][][ * ][]] , [[[ * ]][[]] [[ * ]] , [[[ * ]][[[]]]] [[ * ][]] ⊢ ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 2 [[ * ][ * ]] ← 2 [[ * ][ * ][]] ← 1 [[[ * ]]] ← { [] ← 1 [[]] ← 2 → ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ [] ← 3 [[ * ]] ← 1 [[ * ][]] ← 2 [[ * ][][ * ]] ← 2 [[ * ][][ * ][]] ← 1
where rule s is a shorthand for shift.

Deciding opetopes

We now present in algorithm 4.4.1 the isOpetope function that, given a preopetope ω ∈ P, decides if ω ∈ P ✓ , as proved in proposition 4.4.1 on the next page. This algorithm tries to deconstruct ω by finding the last rule instance if its potential proof tree, and recursively checking the validity of the premises. We emphasize that this algorithm, while straightforward, is extremely inefficient. return isOpetope(ϕ) Proof. This algorithm tries to deconstruct the potential proof tree of ω 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 ⧫, it returns true. □

Python implementation

The derivation system Opt ? and all required syntactic constructs are implemented in module opetopy.UnnamedOpetope of [START_REF] Ho | [END_REF]. 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.5.1. 4.6. The system for opetopic sets

We now present OptSet ? , a derivation system for opetopic set that is controlled by Opt ? (unlike system OptSet ! that is based on Opt ! , see figures 3.1.1 and 3.5.1 on page 17 and on page 30).

As always, contexts are considered as sets, so that the order in which the typings are written is irrelevant, even though those typings might be interdependent. We rely on two types of judgment that can be understood as follows:

(1) Γ context means that Γ is a well-formed context, (2) Γ ⊢ P means that in context Γ, P is a well-formed pasting diagram. We now state the inference rules in figure 4.6.1 on the next page, and simultaneously assign a shape x ♮ to any variable x in a derivable context.

Points:

Γ context point Γ, x ∶ ⧫ context for x a fresh name. Such a cell x has no source, no target, and its shape is given by x ♮ ∶= ⧫. Degenerate pasting diagrams:

Γ, x ∶ T context degen Γ, x ∶ T ⊢ {{x The shape of this pasting diagram is ({{x ) ♮ ∶= {{x ♮ .
Non degenerate pasting diagrams: If there exists p ∈ P ✓ a non degenerate opetope

p = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [p 1 ] ← ψ 1 ⋮ [p k ] ← ψ k and variables x i ∶ T i , for 1 ≤ i ≤ k, such that (1) the cell x i ∶ T i is such that x ♮ i = ψ i , (2) (Inner) whenever [p j ] = [p i [q]] we have t x j = s [q] x i (the latter notation is defined in rule shift), then: Γ, x 1 ∶ T 1 , . . . , x k ∶ T k context graft Γ, x 1 ∶ T 1 , . . . , x k ∶ T k ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [p 1 ] ← x 1 ⋮ [p k ] ←
x k Denote this pasting diagram (i.e. the big expression on the right hand side of ⊢ in the conclusion of the above rule) by P. Its shape is given by P ♮ ∶= p, and let s [pi] P ∶= x i . Forming a pasting diagram in this manner is essentially an unbiased (or non binary) grafting, whence the name of the rule. Shift to the next dimension: If we have a pasting diagram P of shape

P ♮ = p, a cell x ∶ Q → a, such that (1) x ♮ = t p, (2) (Glob1) if p is non degenerate, we have t s [] P = t x, (3) (Glob2) if p is non degenerate, for all leaves [p[q]] of p we have s [q] s [p] P = s ℘p[p[q]] x, (4) (Degen) if p is degenerate, we have Q = {[] ← a , then: Γ, x ∶ Q → a ⊢ P shift Γ, x ∶ Q → a, y ∶ P → x context
for y a fresh name. The shape of y is given by y ♮ ∶= P ♮ , its source is s y ∶= P, for [p] an address in P, its [p]-source is s [p] y ∶= s [p] P, and its target is t y ∶= x.

Equivalence with opetopic sets

Let Υ and Γ = (x 1 ∶ T 1 , . . . , x k ∶ T k ) be two derivable contexts in OptSet ? . Akin to the standard definition, a substitution σ ∶ Υ → Γ is a sequence of expressions (σ 1 , . . . , σ k ) such that for 1 ≤ i ≤ k we have

σ i ∶ T i [σ 1 /x 1 ]⋯[σ i-1 /x i-1 ] ∈ Υ.
Lemma 4.7.1. In the setting above, we have σ ♮ i = x ♮ i . Proof. We proceed by induction. By definition, σ 1 = x 1 , and thus σ ♮ 1 = x ♮ 1 . By induction, take 1 ≤ i ≤ k and assume σ ♮ j = x ♮ j for j < i. Since the shape of a pasting diagram P = { [p 1 ] ← y 1 ⋮ only depends on the shape of the y j 's, we have

x ♮ i = T ♮ i = (T i [σ 1 /x 1 ]⋯[σ i-1 /x i-1 ]) ♮ = σ ♮ i . □
Let Ctx ? be the syntactic category of our sequent calculus, i.e. the category whose objects are derivable contexts, and morphisms are substitutions as defined above. We now construct the unnamed stratification functor S ? ∶ (Ctx ? ) op → Fin Ô. For Γ ∈ Ctx ? and ω ∈ O, let

S ? Γ ω = {x ∈ Γ | x ♮ = ⟦ω⟧ ? } .
If x ♮ ≠ ⧫, then the type X of x is of the form P → z, and we let t x ∶= z. This is well defined as by construction of Γ we have z

♮ = t x ♮ . For [p] ∈ ω • , we let s [p] x ∶= s [p] P. Again, this is well defined as (s [p] P) ♮ = s [p] P ♮ = s [p] x ♮ .
From there, the opetopic identities clearly hold, and S ? Γ is a finite opetopic set. To abbreviate notations, and for f ∶ ψ → ω a morphism in O, we let f = S ? Γf ∶ S ? Γ ω → S ? Γ ψ . Take now σ = (σ 1 , . . . , σ k ) ∶ Υ → Γ a substitution, where as before Γ = (x 1 ∶ T 1 , . . . , x k ∶ T k ). We define a morphism S ? σ ∶ S ? Γ → S ? Υ. For x i a variable of Γ, and ω ∈ O such that ⟦ω⟧ ? = x ♮ i , there is a corresponding cell x i ∈ S ? Γ ω , and we let S ? σ(x i ) ∶= σ i . This is well-defined since by lemma lemma 4.7.1 on the facing page, we have σ i ∈ S ? Υ ω . Lemma 4.7.2. The mapping S ? σ is a morphism of opetopic sets (i.e. a natural transformation) S ? Γ → S ? Υ.

Proof. Assume ω ≠ ⧫, so that the type of x i is P → x j for some j < i, and the type of

σ i is P[σ 1 /x 1 ]⋯[σ i-1 /x i-1 ] → σ j . Then S ? σ(t x i ) = σ j = t(S ? σ(x i )). If [p] ∈ ω • , then s [p] x i = x l ,
for some l < i, and

S ? σ(s [p] x i ) = σ l = s [p] (P[σ 1 /x 1 ]⋯[σ i-1 /x i-1 ]) = s [p] (S ? σ(x i )).
Hence, S ? σ is a morphism of opetopic sets S ? Γ → S ? Υ. □ Theorem 4.7.3. The functor S ? ∶ (Ctx ? ) op → Fin Ô is an equivalence of categories.

Proof. Let Γ, Υ ∈ Ctx ? , with Γ = (x 1 ∶ T 1 , . . . , x k ∶ T k ), and f ∶ S ? Γ → S ? Υ. Then f = S ? (f (x 1 ), . . . , f (x k )),
showing that S ? is fully faithful. We now prove that it is essentially surjective. Take X ∈ Fin Ô, and enumerate its cells as x 1 ∈ X ω1 , . . . , x k ∈ X ω k , such that whenever i < j we have dim ω i ≤ dim ω j . To each 0 ≤ i ≤ k we associate a derivable context Γ (i) = (x 1 ∶ T 1 , . . . , x i ∶ T i ) such that x i ♮ = ⟦ω i ⟧ ? , as follows:

(1) If ω i = ⧫, let Γ (i) be given by the following proof tree (so that implicitly, T i = ⧫):

Γ (i-1) context point Γ (i-1) , x i ∶ ⧫ context (
2) Assume ω i ≠ ⧫ is not degenerate. Then, by induction, for x j = t x i we have t x i ♮ = t ω i , and for all address i) is given by the following proof tree: i) is given by the following proof tree:

[p j ] ∈ ω • i , we have s [pj ] x i ♮ = s [pj ] ⟦ω i ⟧ ? . From this, Γ (
Γ (i-1) context graft Γ (i-1) ⊢ { [p 1 ] ← s [p1] x i ⋮ shift Γ (i-1) , x i ∶ { [p 1 ] ← s [p1] x i ⋮ → t x i context (3) Assume ω i is degenerate, Then Γ (
Γ (i-1) context degen Γ (i-1) ⊢ {{t t x i shift Γ (i-1) , x i ∶ {{t t x i → t x i context
Finally, the mapping x i → x i exhibits an isomorphism X → S ? Γ (k) . □

The category Ctx ? has finite limits, induced from finite colimits in Fin Ô through S ? . We conclude this section with a result similar to theorem 3.6.17 on page 36, stating that opetopic sets essentially are "models of the algebraic theory Ctx ? ". Theorem 4.7.4. We have an equivalence Ô ≃ Mod(Ctx ? , Set), where Mod is defined in theorem 3.6.17 on page 36 Proof. We proceed as in the proof of theorem 3.6.17 on page 36. □

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 4.8.1. We now derive the following opetopic set, which is not representable:

a b f g h ⇓ α
We decide to introduce all points first: point a ∶ ⧫ context point a, b ∶ ⧫ context Then we introduce f , by first specifying its source pasting diagram with the graft rule, parameterized by opetope ◾ = { * ← ⧫ , and then applying the shift rule:

⋮ a, b context graft a, b ⊢ { * ← a shift a, b, f ∶ { * ← a → b context
We proceed similarly for g and h:

⋮ a, b, f context graft a, b, f ⊢ { * ← a shift a, b, f, g ∶ { * ← a → b context graft a, b, f, g ⊢ { * ← b shift a, b, f, g, h ∶ { * ← b → a context
Lastly, we introduce α, first by specifying its source with the graft rule, parameterized by opetope 1 = {[] ← ◾ (see the opetopic integers defined in example 4.3.2 on page 55), and applying the shift rule:

⋮ a, b, f, g, h context graft a, b, f, g, h ⊢ {[] ← f shift a, b, f, g, h, α ∶ {[] ← f → g context

⇓

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

point a ∶ ⧫ context graft a ⊢ { * ← a shift a, f ∶ { * ← a → a context
Then we introduce α, by first specifying its source pasting diagram with the graft rule, parameterized by opetope

2 = { [] ← ◾ [ * ] ← ◾
(see the opetopic integers defined in example 4.3.2 on page 55), and applying the shift rule:

⋮ a, f context graft a, f ⊢ { [] ← f [ * ] ← f shift a, f, α ∶ { [] ← f [ * ] ← f → f context
Likewise, we introduce β, where the graft rule is parameterized by 3:

⋮ a, f, α context graft a, f, α ⊢ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← f [ * ] ← f [ * * ] ← f shift a, f, α, β ∶ ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ [] ← f [ * ] ← f [ * * ] ← f → f context Lastly, we introduce A, where the graft rule is parameterized by { [] ← 2 [[ * ]] ← 2 : ⋮ a, f, α, β context graft a, f, α, β ⊢ { [] ← α [[ * ]] ← α shift a, f, α, β, A ∶ { [] ← α [[ * ]] ← α → β context Example 4.8.3. The opetopic set a a a b ⇓α ⇓β h f g h h is straightforwardly derived as point a ∶ ⧫ context point a, b ∶ ⧫ context graft a, b ⊢ { * ← a shift a, b, f ∶ { * ← a → b context graft a, b, f ⊢ { * ← b shift a, b, f, g ∶ { * ← b → a context ⋮ graft a, b, f, g ⊢ { * ← a shift a, b, f, g, h ∶ { * ← a → a graft a, b, f, g, h ⊢ { [] ← g [ * ] ← f shift a, b, f, g, h, α ∶ { [] ← g [ * ] ← f → h context graft a, b, f, g, h, α ⊢ {[] ← h shift a, b, f, g, h, α, β ∶ {[] ← h → h 4.9. Python implementation
System OptSet ? is implemented in module opetopy.UnnamedOpetopicSet of [START_REF] Ho | [END_REF]]. The rules are represented by functions point, degen, graft, and shift, and are further encapsulated in rule instance classes Point, Degen, Graft, and shift.

Conclusion

We have introduced two syntactic presentations for opetopes, as well as for opetopic sets, and formally related them to preexisting definitions. Together with an adequate formulation of opetopic higher categories, it is our hope that this work will be used productively for mechanical proofs of coherence in opetopic ω-categories or opetopic ω-groupoids. where tr F is the set of F -tree (see section 2.1 on page 9), and tr | F is the set of F -trees equipped with a marked leaf.

Theorem A.1.2 (Free monad [START_REF] Kock | Polynomial functors and opetopes[END_REF], Kock, 2011]). The polynomial functor F ⋆ is canonically a polynomial monad. Moreover, the adjunction (-) ⋆ ⊣ U is monadic.

Let us abuse notations and write (-) ⋆ for the associated monad on the category PolyEnd(I). Write its laws by µ ⋆ ∶ (-) ⋆⋆ → (-) ⋆ for multiplication (or unbiased grafting), and Y ∶ id → (-) ⋆ for the unit (or introduction of corollas). T ∶= X ○

(T ○ [l] Y b ) | = T | + Y | b -{[l]} → E((t T ) ◽ ℘ T [l] b) [p] ∈ T | -{[l]} → χ (t T ) ◽ ℘ T [l] b (℘ T [l]) [e] ∈ Y
[p]

T ◯ χ -1 T ei Y i ;
where q ∈ E(t B) and {v i } i ⊆ E(t C). Then

B)

◽

[e]⋅χ -1 B q⋅[r] C = X ○ [e] B ○ χ -1 B q Y ○ [r] C ◯ χ -1 C vi Z i ,
and the reindexing χ

(A ◽ [e] B) ◽ χ A ◽ [e] B [f ] C χ A ◽ [e]
B is given by

[p] ∈ B • → [ep] → [ep] [p] ∈ C • → [e] ⋅ χ -1 B q ⋅ [rp] [e[q]s] ⋤ [f ] → [e] ⋅ χ -1 B q ⋅ [s] → [e] ⋅ χ -1 B q ⋅ [s] [f [v i ]s] → [e] ⋅ χ -1 B q ⋅ [r] ⋅ [[v i ]s] → [e] ⋅ χ -1 B q ⋅ [r] ⋅ χ -1 C v i ⋅ [s] [p] ∈ A • not as above → [p] → [p]
On the other hand, we have

A ◽ [f ] C = X ○ [e] Y t B ○ [q] Y ○ [r] C ◯ χ -1 C vi Z i .

The reindexing gives χ

A ◽ [f ] C [e] = [e],
and

(A ◽ [f ] C) ◽ [e] B = X ○ [e] B ○ χ -1 B q Y ○ [r] C ◯ χ -1 C vi Z i = (A ◽ [e]

B) ◽

[e]⋅χ -1 B q⋅ [r] C. (2) Assume [e] and [f ] are ⊑-incomparable, and write A as

The reindexing χ

(A ◽ [f ] C) ◽ [e] B χ A ◽ [f ] C is given by [p] ∈ B • → [ep] [p] ∈ C • → [f p] → [e] ⋅ χ -1 B q ⋅ [rp] [e[q]s] ⋤ [f ] → [e[q]s] → [e] ⋅ χ -1 B q ⋅ [s] [f [v i ]s] → [f ] ⋅ χ -1 C v i ⋅ [s] → [e] ⋅ χ -1 B q ⋅ [r] ⋅ χ -1 C v i ⋅ [s] [p] ∈ A • not
A = (X ○ [e] Y t B ◯ [vi] Y i ) ○ [f ] Y t C ◯ [wj ] Z j . Then A ◽ [e] B = (X ○ [e] B ◯ χ -1 B vi Y i ) ○ [f ] Y t C ◯ [wj ] Z j , the reindexing gives χ A ◽ [e] B [f ] = [f ], (A ◽ [e] B) ◽ [f ] C = (X ○ [e] B ◯ χ -1 B vi Y i ) ○ [f ] C ◯ χ -1 C wj Z j ,
and the complete reindexing

χ (A ◽ [e] B) ◽ [f ] C χ A ◽ [e]
B is given by

[p] ∈ B • → [ep] → [ep] [p] ∈ C • → [f p] [e[v i ]s] → [e] ⋅ χ -1 B v i ⋅ [s] → [e] ⋅ χ -1 B v i ⋅ [s] [f [w j ]s] → [f [w j ]s] → [f ] ⋅ χ -1 C w j ⋅ [s] [p] ∈ A • not as above → [p] → [p] On the other hand, A ◽ [f ] C = (X ○ [e] Y t B ◯ [vi] Y i ) ○ [f ] C ◯ χ -1 C wj Z j , we have χ A ◽ [f ] C [e] = [e], (A ◽ [f ] C) ◽ [e] B = (X ○ [e] B ◯ χ -1 B vi Y i ) ○ [f ] C ◯ χ -1 C wj Z j = (A ◽ [e] B) ◽ [f ]
C, and further

[p] ∈ B • → [ep] [p] ∈ C • → [f p] → [f p] [e[v i ]s] → [e[v i ]s] → [e] ⋅ χ -1 B v i ⋅ [s] [f [w j ]s] → [f ] ⋅ χ -1 C w j ⋅ [s] → [f ] ⋅ χ -1 C w j ⋅ [s] [p] ∈ A • not
(A ◽ [e] B) ◽ [ef ] C = X ○ [e] (Z ○ [f ] Y t C ◯ [wj ] T j ) ◯ α(χ -1 B vi) Y i ,
where

α(χ -1 B v i ) = { [f ] ⋅ χ -1 C w j ⋅ [r] if χ -1 B v i of the form [f [w j ]r], χ -1 B v i otherwise.
Remark that α(χ -1

B v i ) = χ -1 B ◽ [f ] C v i . The reindexing χ (A ◽ [e] B) ◽ [ef ] C χ A ◽ [e]
B is given by:

[p] ∈ C • → [ef p] [f [w j ]r] ∈ B • → [ef [w j ]r] → [ef ] ⋅ χ -1 C w j ⋅ [r] [p] ∈ B • , [f ] ⋤ [p] → [ep] → [ep] [e[v i ]r] ∈ A • → [e] ⋅ χ -1 B v i ⋅ [r] → [e] ⋅ χ -1 B ◽ [f ] C v i ⋅ [r]
On the other hand, we have

B ◽ [f ] C = Z ○ [f ] C ◯ χ -1 C wj T j , A ◽ [e] (B ◽ [f ] C) = X ○ [e] (Z ○ [f ] Y t C ◯ [wj ] T j ) ◯ χ -1 B ◽ [f ] C vi Y i = (A ◽ [e] B) ◽ [ef ]
C and the reindexing is given by

[p] ∈ C • → [f p] → [ef p] [f [w j ]r] ∈ B • → [f ] ⋅ χ -1 C w j ⋅ [r] → [ef ] ⋅ χ -1 C w j ⋅ [r] [p] ∈ B • , [f ] ⋤ [p] → [p] → [ep] [e[v i ]r] ∈ A • → [e] ⋅ χ -1 B ◽ [f ] C v i ⋅ [r]
We thus see that the square (A.1.11) commutes, and that the monad structure of M + given in definition A.2.2 on page 73 satisfies condition (Nested multiplication) of theorem A.1.9 on page 72. □

  Introduction of degeneracies. Given an n-opetope ω, we can build an (n + 2)-opetope with empty source, whose target is the globe at ω, as illustrated below for n = 0 and n = 1:. degen . Grafting. Given an (n + 1)-opetope α and an (n + 1)-pasting scheme β such that the source of β contains an n-cell of the same shape as the target of α, we can graft α to β:

  onto the lower trapezoid of the right opetope is possible:

2. 1 . 1 .

 11 The polynomial Baez-Dolan (-) + construction. We now give a brief definition of the (-) + construction, see appendix A on page 71 for details. A polynomial monad (M, µ, η) is simply a monad in the 2-category PolyEnd. This structure induces a function t ∶ tr M → B M , for each T ∈ tr M a bijection ℘ T ∶ T | → (t T ) • , called readdressing, see appendix A.1 on page 71.

Figure 3

 3 Figure 3.1.1. The Opt ! system.

  , z ← b(b ← r), . . .), we replace the grafting z ← b(b ← r) by z ← r and add b = z to the ambient equational theory, (3) and finally replace any remaining subterms of the form b(b ← v) by v. More explicitly:

  .1.4) (2) If w is an empty pasting diagram, say w = b for b ∈ V n-2 , Then, by the hypothesis of the graft rule, we have b = E s a. Then, u[b/a] is defined by cases on the form of u: (a) if u = E∪F a, then u[b/a] ∶= b; (b) if u is of the form a(b ← r), then u[b/a] ∶= r; (c) if u is of the form y(. . . , z ← a, . . .), then u[b/a] ∶= y(. . . , . . .), and we add the equality b = z to the ambient equational theory; (d) if u is of the form 1 y(. . . , z ← a(b ← r), . . .), then u[b/a] ∶= y(. . . , z ← r, . . .), as in equation (3.1.4) on the preceding page, and per equation (3.1.2) on the previous page, but we also add the equality b = z to the ambient equational theory;

  Consider the variables α, β x , and β y typed as:

  written ⟦t ∶ T ⟧ poly n+1 or even ⟦t⟧ poly n+1 for short, if no ambiguity arises. Also, if α ∈ V n+1 , then we set ⟦α⟧ poly n+1 ∶= ⟦s α⟧ poly n+1 .

  we have ⟦r⟧ poly n+1 = ⟦t⟧ poly n+1 ○ &ta Y ⟦x⟧ poly n . Proof. We have ⟦r⟧ poly n+1 = ⟦t⟧ poly n+1 ○ [l] Y ⟦x⟧ poly n , for some address [l]. Then, writing t = z( → y i ← u i ), we have, according to definition definition 3.1.1 on page 17,

  for ◽ the partial multiplication of Z n as in theorem A.1.9 on page 72,

□

  This result concludes the proof that equations (3.2.4) to (3.2.6) of definition 3.2.3 on page 21 are well defined.Corollary 3.2.13. Let (E ▹ Γ ⊢ n t ∶ T ) be a derivable sequent. Then & t exhibits a bijection between the set of n-variables of t, and (⟦t⟧ poly n+1 )• . It is also a bijection between the set of (n -1)-variables of s t and (⟦t⟧poly n+1 ) | .The rest of this section is dedicated to prove theorem 3.2.22 on page 25 stating that ⟦-⟧ poly n is a bijection modulo ≃. We first prove surjectivity, by defining a sequent ⟦ω⟧ ! such that ⟦⟦ω⟧ ! ⟧ poly n

  opetopes is in bijection with the set of natural numbers. Given n ∈ N, we denote by n the 2-opetope whose pasting diagram is a sequence of n arrows as follows:

Figure 3

 3 Figure 3.4.1. Derivation of the arrow sequent using opetopy.NamedOpetope

↪

  Figure 3.4.2. Derivation of some opetopic integers using opetopy.NamedOpetope, continuation of figure 3.4.1

Figure 3

 3 Figure 3.5.1. The OptSet ! system.

  and s [] s a = x (see definition 3.2.1 on page 20). Zero: This rules introduces the empty OCMT. zero ▹ Binary sums: This rule takes two disjoint opetopic sets (i.e. whose cells have different names), and produces their sum. If Γ ∩ Υ = ∅, then E ▹ Γ F ▹ Υ sum E ∪ F ▹ Γ ∪ Υ Quotients: This rule identifies two parallel cells in an opetopic set by extending the underlying equational theory. If a, b ∈ V Γ are such that s a = E s b and t a = E t b, then

  [p] ∈ ⟦a⟧ poly k • , Then, by corollary 3.2.13 on page 23, there is a unique b ∈ V Cx|a,k-1 such that & s a b = [p]. Write then s [p] a = b.

  Write [p] = & s a b, for some b ∈ (s a) • (see corollary 3.2.13 on page 23). Then, by corollary 3.2.8 on page 21, we have s[p] ⟦a⟧ With all the structure introduced above, C x /T x is an opetopic set.

|=

  . Then [p[q]] = & s a b for some c ∈ (s s a) • , and further, c = s[q] s [p] a. Then ℘ ⟦a⟧ poly k [p[q]] = ℘ ⟦s a⟧ poly k & s t a csince s s a = s t a,and thus s [q] s [p] a = c = s &s t a c t a = s ℘ ⟦a⟧ poly k [p[q]] t a. (4) (Degen) Assume that a is degenerate, say s a = b. Then s [] t a = b = t t a = a,where the last equality comes from the rule repr (recall that by convention a = t 0 a). □ Lemma 3.6.4. The opetopic set C x /T x is a quotient of the representable O[⟦x⟧ poly n ], where the latter is the representable at ⟦x⟧ poly n ∈ O n (see section 2.2.4 on page 13). Proof. Clearly, the poset of cells ∫ O C x /T x of C x /T x has a unique maximum element, namely x itself. Moreover, that element has shape ⟦x⟧ poly n , i.e. x ∈ (C x /T x ) ⟦x⟧ poly n . Then, by the Yoneda lemma, there is a map O[⟦x⟧ poly n

  We have an isomorphism C x /T x ≅ O[⟦x⟧ poly n

  by proposition 3.6.5 on the preceding page, and by the same argument as above, C x /T x ≅ O[⟦x⟧ poly 1

  poly n-1 by proposition 3.6.5 on the facing page. ThenC x = C y + {t k x | 0 ≤ k ≤ n}, and t t xT x t s [] x = t y. Consequently,Tx is equivalent to the theory T y + {t t x = t y}, and thusC x /T x = C y /T y + {x, t x} . By induction, C y /T y ≅ O[⟦y⟧ poly n-1 ], and # C x /T x = 2 + # C y /T y = 2 + # ⟦y⟧ poly n-1 = # ⟦x⟧poly n , which, by the same argument as above, proves the isomorphism C x /T x ≅ O[⟦x⟧ poly n ].(2) If s x = a for some a ∈ V n-2 , then ⟦x⟧

  page. Then C x = C a + {t k x | 0 ≤ k ≤ n},and t t xT x a. Therefore T x is equivalent to the theory T a + {t t x = a}, and thus

  and (E| a ▹ Γ| a ) the restriction to a. Then we have an inclusion i ∶ Γ| a /E| a ↪ Γ/E, where i ∶ b → b for all b ∈ V Γ|a , and thus we have a natural map ã ∶ O[⟦a⟧ poly k ] → Γ/E given by the composite

Figure 3

 3 Figure 3.8.1. Derivation of example 3.7.1 on page 36 using opetopy.NamedOpetopicSet

Figure 3

 3 Figure 3.9.1. The OptSet ! m system. Introduction of points: This rule introduces 0-cells, also called points. If x ∈ V 0 , then point ▹x ∶ ∅ Introduction of degenerate pasting diagrams: This rule creates a new degenerate pasting diagram. If x ∈ V Γ,k , then

  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

  occurring in t} . Zero: This rules introduces the empty OCMT. zero ▹ Binary sums: This rule takes two disjoint OCMTs (i.e. whose cells have different names), and produces their sum. If Γ ∩ Υ = ∅, then E ▹ Γ F ▹ Υ sum E ∪ F ▹ Γ ∪ Υ Quotients: This rule identifies two parallel cells in an opetopic set by extending the underlying equational theory. If a, b ∈ V Γ are such that s a = E s b and t a = E t b, then

  Likewise, if we have a proof tree as on the left of figure 3.10.1, we rewrite it as on the right.

Figure 3 .

 3 Figure 3.10.1. Proof of proposition 3.10.1 on the preceding page: commuting repr' with a graft' and shift' sequence

Figure 3 .

 3 Figure 3.10.2. Proof of lemma 3.10.2 on the facing page: commuting sum with a graft and shift sequence

Figure 3 .

 3 Figure 3.10.3. Proof of lemma 3.10.2 on page 42: commuting glue with a graft and shift sequence

  addresses [] and [ * * * * * ] (it would at least need addresses [ * ], [ * * ], [ * * * ], and [ * * * * ]), and neither does the third, as it does not have a root node (corresponding to address []). Finally, the last preopetope does represent an opetope.

Figure 4

 4 Figure 4.1.1. The Opt ? system.

  Example 4.3.3 (A classic). The 3-opetope on the left is derived as on the right:

Figure 4

 4 Figure 4.5.1. Implementation of Opt ? 's shift rule in opetopy.UnnamedOpetope.shift

Figure 4

 4 Figure 4.5.2. Derivation of the arrow sequent (see example 4.3.1 on page 54) using opetopy.UnnamedOpetope

##

  Figure 4.5.4. Derivation of example 4.3.3 on page 55 using opetopy.UnnamedOpetope

Figure 4

 4 Figure 4.6.1. The OptSet ? system.

Figure 4

 4 Figure 4.9.1. Derivation of example 4.8.2 on page 62 using opetopy.NamedOpetope

  Definition A.1.1 (Polynomial monad, classical definition). A polynomial monad M over a set I is a monoid object in the category PolyEnd(I) of polynomial endofunctors over I, where the monoidal product ⊙ is the composition of polynomial functors [Gambino and Kock, 2013]. The structure morphisms η ∶ id → M and µ ∶ M ⊙ M → M indeed give the functor M ∶ Set/I → Set/I the structure of a cartesian monad.Let PolyMnd(I) be the subcategory of PolyEnd(I) spanned by polynomial monads and morphisms of monads. We emphasize that in PolyMnd(I), morphisms are expected to be identities on the set I of colors. There is an obvious forgetful functor U ∶ PolyMnd(I) → PolyEnd(I) that turns out to have a left adjoint that we now present. Let F ∈ PolyEnd(I) be as on the left, and define a new polynomial functor F ⋆ as on the right,

  Corollary A.1.3 (Polynomial monad, algebraic definition). A polynomial monad is a (-) ⋆ -algebra, i.e. the data of a polynomial endofunctor M together with a morphism sup ∶ M ⋆ → M as I structure maps η ∶ id → M and µ ∶ M ⊙ M → M can be retrieved by noting that both id and M ⊙ M are canonically subobjects of M ⋆ . Corollary A.1.6 (Contraction associativity formula). Let T, U ∈ tr M , and[l] ∈ T | such that the grafting T ○ [l] U is defined. Then t(T ○ [l] U ) = t(Y t T ○ [℘ T [l]] Y t U ). (A.1.7) Further, for [r] ∈ U | , we have a leaf [l] ⋅ [r] = [lr] ∈ (T ○ [l] U )| , and℘ T ○ [l] U [lr] = ℘ V (℘ T [l] ⋅ ℘ U [r]) with V = Y t T ○ [℘ T [l]] Y t U . (A.1.8) Proof. Since M is a (-) ⋆ -algebra,the left diagram of (A.1.5) commutes. □ Theorem A.1.9 (Polynomial monads via partial laws). Take a polynomial endofunctor M ∈ PolyEnd(I), and write it as: ) ⋆ -algebra structure on M (i.e. a structure of polynomial monad on M ) is equivalent to the following data: (1) (Unit) a map η ∶ I → B; (2) (Partial multiplication) a map ◽ ∶ E × I B → B, where for (e, b) ∈ E × I B and a = p(e) we write a ◽ e b for ◽(e, b), and say that a ◽ e b is an admissible expression (or just admissible); in the sequel, we assume that all expressions of this kind are admissible; (3) (Partial reindexing) for a ◽ e b admissible, an isomorphism χ a ◽e b ∶ E(a) + E(b) -{e} ≅ (Trivial) for i ∈ I, we have t(η(i)) = i, and E(η(i)) is a singleton whose unique element e is such that s(e) = i; (2) (Left unit) for i ∈ I, b ∈ B, and e the unique element of E(η(i)), we have η(i) ◽ e b = b, and χ η(i) ◽e b ∶ E(b) → E(b) is the identity; (3) (Right unit) for i ∈ I, b ∈ B, and e ∈ E(b), we have b ◽ e η(i) = b, and χ b ◽e η(i) is given byE(b) + E(η(i)) -{e} → E(b) x ∈ E(b) → x y ∈ E(η(i)) → e;(4) (Disjoint multiplication) for a ◽ e b and a ◽ f c admissible expressions, and e ≠ f , we have multiplication) for a ◽ e b and b ◽ f c admissible, we have Moreover with the data above, the components of the structure map M ⋆ → M (as in diagram (A.1.4)) are inductively given by:(1) (Target) for i ∈ I,t I i = η(i); for b ∈ B, t Y b = b; for T ∈ tr M + , [l] ∈ T | , and b ∈ B such that the grafting T ○ [l] Y b is defined: t(T ○ [l] Y b ) = (t T ) ◽ ℘ T [l] b,where ℘ T is defined next; (2) (Readdressing) for b ∈ B, ℘ Y b ∶ Y | b → E(b) [e] → e; for T ∈ tr M + , [l] ∈ T | , and b ∈ B such that the grafting T ○ [l] Y b is defined, the readdressing ℘ T ○ [l] Y b is given by

|b

  → χ (t T ) ◽ ℘ T [l] b (e) Proof(sketch). Conditions (Disjoint multiplication) and (Nested multiplication) ensure that t T does not depend on the chosen decomposition, and thus define a structure map sup ∶ M ⋆ → M making the left square of (A.1.5) commute. Conditions (Trivial), (Left unit), and (Right unit) ensure that the right triangle of (A.1.5) commutes too, and thus that M is a (-) ⋆ -algebra, that is, a polynomial monad. □A.2. A complete (-) + constructionLet M be a polynomial monad and define M + as being the following polynomial functor: T ∈ tr M , the fiber u -1 T (which we shall also denote by T • ) is the set of node addresses in T , and for[p] ∈ T • , s[p] ∶= s [p] T .Definition A.2.2 (Monad structure on M + ). We endow M + with a monad structure by means of theorem A.1.9 on the preceding page. The maps η + ∶ I → B and ◽ ∶ tr • M × B tr M are defined as follows:(1) (Unit) for b ∈ B, let η + (b) ∶= Y b ; (2) (Partial multiplication) for U, T ∈ tr M , [p] ∈ U • such that s [p] U = t T ,write (recall that ○ is associative on the right) e i ]} i ⊆ Y | t T (equivalently, {e i } i ⊆ E(t T )), and define U ◽ [p]

  and χ A ◽ [e] B [f ] = χ A ◽ [e] B [e[q]r] = [e] ⋅ χ -1 B q ⋅ [r]. Thus,

  as above → [p] → [p] We see that the square (A.1.10) commutes in the case [e] ⊑ [f ].

  as above → [p] → [p] so that the square (A.1.10) commutes in the case where [e] and [f ] are ⊑-incomparable too. Finally, the monad structure of M + given in definition A.2.2 on page 73 satisfies condition (Disjoint multiplication) of theorem A.1.9 on page 72. □ Proof of (Nested multiplication). Let A, B, C ∈ tr M , [e] ∈ A • , [f ] ∈ B • , such that A ◽ [e] B and B ◽ [f ] C are admissible. Write A = (X ○ we have χ A ◽ [e] B [f ] = [ef ], and

  al., 2010].A polynomial endofunctor F over I is a Set-diagram of the form:

	I	s	E	p	B	t	I.	(2.1.1)

Elements of B are called nodes or operations, elements of the fiber E(b) ∶= p -1 (b) are the inputs or arities of b, and elements of I are colors. For b ∈ B, if e ∈ E(b), let s e (b) ∶= s(e). We will sometimes refer to I, B and E as I F , B F , and E F , respectively. A morphism f ∶ F → F ′ of polynomial functors is a diagram of the form

  1) (Objects) We set ob O = ∑ n∈N O n . (2) (Generators) Let ω ∈ O n with n ≥ 1. We introduce a generator, called target embedding: t ∶ t ω → ω. If [p] ∈ ω • ,then we introduce a generator, called source embedding: s [p] ∶ s [p] ω → ω.

	A face embedding is
	either a source or target embedding.
	(3) (Relations) We impose 4 relations described by the following commutative squares, that are well defined
	thanks to theorem lemma 2.2.4. Let ω ∈ O n with n ≥ 2
	(a) (Inner) for [

  there, this is a straightforward induction.

	poly
	n-2
	= e [l] ⟦u⟧ poly n	by proposition 3.2.7 on page 21

□ Proposition 3.2.19. In proof tree (3.2.6), the instance of graft is well-defined. Proof. Write ⟦ψ⟧ ! = (F ▹ Υ ⊢ n-1 p ∶ P ). By the previous lemma, we have a ∈ (s s u) • . Further, ⟦s a⟧ poly n-2 = ⟦e [l] u⟧ = e [l] ν = t s [] Y ψ by relation (Inner), see section 2.2.4 = t ψ = ⟦s s p⟧ poly n-2 by proposition 3.2.11 on page 22. By induction on n, the polynomial coding ⟦-⟧ poly n-2 is injective modulo ≃. Hence, we can assume s a = s s p without loss of generality, and finally, the instance of the graft rule is well-defined. □ Proposition 3.2.20. Let ω ∈ O n be a non degenerate opetope, and consider two arbitrary decompositions in corollas

  3) Lastly, the equational theories G and G ′ are the union of E ν , E ψ , and E ψ ′ , and the potential additional equalities incurred by the independent substitutions s ψ /a and s ψ

	poly 0 (2) With the same notations as in (3.2.15), and by induction, we have = ⧫.

′ /a ′ . Hence G = G ′ . □ Corollary 3.2.21. For any opetope ω ∈ O, the sequent ⟦ω⟧ ! is uniquely defined up to ≃. Proof. Clearly, proof trees (3.2.14), (3.2.15), and (3.2.16) are well-defined. In proposition 3.2.19 on the preceding page, we show that the same holds for proof tree (3.2.17). Finally, in proposition 3.2.20 on the facing page, we show that for a non degenerate opetope ω ∈ O n , the sequent ⟦ω⟧ ! does not depend on the decomposition of ω. □ Theorem 3.2.22. The polynomial coding ⟦-⟧ poly n is a bijection modulo ≃, whose inverse is ⟦-⟧ ! restricted to O n . Proof. We first show that for ω ∈ O n we have ⟦⟦ω⟧ ! ⟧ poly n = ω by opetopic induction (see remark 2.2.3 on page 12).

(1) By definition of ⟦-⟧ poly , ⟦⟦⧫⟧ ! ⟧

  be a derivable sequent, with x ∈ V n . In lemma 3.6.4, we established that C x /T x is a quotient of the representable opetopic set O[⟦x⟧

	poly
	n

  and t s [] zT z t t z, we have

  For ω ∈ P, the execution isOpetope(ω) returns true if and only if ω ∈ P ✓ .

	Proposition 4.4.1.
	6:	else
	7:	while ω has an address of the form [p[q]] do
	8:	if [p] / ∈ ω • or not isOpetope(s [p] ω) then
	9:	return false
	10:	else if [q] / ∈ (s [p] ω) • or not isOpetope(s [p[q]] ω) then
	11:	return false
	12:	else if t s [p] ω ≠ s [p[q]] ω then
	13:	return false
	14:	else
	15:	Remove address [p[q]] from ω
	16:	end if
	17:	end while
	18:	if ω is of the form {[] ← ψ then
	19:	return isOpetope(ψ)
	20:	else
	21:	return false
	22:	end if
	23:	end if
	24: end procedure

PRELIMINARIES

NAMED APPROACH

This author has received funding from the European Union's Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement №665850.

2010

(1) (Degenerate case) for ϕ ∈ O n-2 , let ⟦I ϕ ⟧ ? ∶= {{⟦ϕ⟧ ? ;

(2) (Corolla case) for ψ ∈ O n-1 , let ⟦Y ψ ⟧ ? ∶= {[] ← ⟦ψ⟧ ? ;

(3) (Graft case) for ω ∈ O n that is neither degenerate nor a corolla, write ω

and [l] ∈ ν | , then let ⟦ω⟧ ? be defined by the following proof tree:

graft-[l] ⟦ω⟧ ? or in other words, ⟦ω⟧ ? = ⟦ν⟧ ? ○[l] ⟦ψ⟧ ? .

We prove that the last case makes sense in the following three lemmas. Proof. We proceed by opetopic induction (see remark 2.2.3 on page 12).

(1) (Degenerate case) Assume ω = I ϕ , for some ϕ

(2) (Corolla case) Assume ω = Y ψ , for some ψ ∈ O n-1 , so that we have ⟦ω⟧

Similarly, by induction,

. Proof. We proceed by opetopic induction.

(1) (Degenerate case) If ω is degenerate, then ω • = ∅, so there is nothing to check in this case.

(

(

Otherwise, we have

□ Lemma 4.2.3. For ω ∈ O n , we have ⟦t ω⟧ ? = t ⟦ω⟧ ? , and ℘ ω = ℘ ⟦ω⟧ ? .

Proof. We proceed by opetopic induction.

(1) (Degenerate case) Assume

Since ω and ⟦ω⟧ ? are both degenerate (as opetope and preopetope, respectively), ℘ ω and ℘ ⟦ω⟧ ?

both map [] (the unique leaf of ω and ⟦ω⟧ ? ) to [] (the unique node of t ω and t ⟦ω⟧ ? ).

(2) (Corolla case) Assume ω = Y ψ , for some ψ ∈ O n-1 , so that we have ⟦ω⟧

and by definition we have

We finally prove that ⟦-⟧ ? is a bijection by constructing its inverse ⟦-⟧ poly ∶ P ✓ n → O n . If n = 0, 1, then both sets are singletons, so that ⟦-⟧ poly is trivially defined. Assume n ≥ 2, and that ⟦-⟧ poly is defined for k < n. We distinguish three cases:

(1) (Degenerate case) if q ∈ P ✓ n-2 , then ⟦{{q ⟧ poly ∶= I ⟦q⟧ poly ;

(2) (Corolla case) if q ∈ P ✓ n-1 , then ⟦{[] ← q ⟧ poly ∶= Y ⟦q⟧ poly ;

(3) (Graft case) for p ∈ P ✓ n , q ∈ P ✓ n-1 , and

Examples

In this section, we give example derivations in system Opt ? .

Example 4.3.1 (The arrow). The unique 1-opetope

Polynomial monads and the Baez-Dolan (-) + construction

From a polynomial monad (definition A.1.1, corollary A.1.3, and theorem A.1.9 on pages 71-72) M with set of operations B, the Baez-Dolan construction gives a new polynomial monad M + having B as its set of colors.

In this chapter, we study the monad structure of M + in depth.

A.1. Polynomial monads

A polynomial monad is classically defined as a monoid object in PolyEnd(I), for some set I. However, there are two other approaches that we present in this section. The first one presents polynomial monads as algebras over the mouthful "free polynomial monad monad" [START_REF] Gambino | [END_REF]Kock, 2013, Kock, 2011], and the other using so-called "partial laws" [START_REF] Kock | Polynomial functors and opetopes[END_REF].

(3) (Partial reindexing) for U ◽

With this definition, the (-) ⋆ -algebra structure map

The readdressing map ℘ ∶ tr | M + → tr • M also admit a somewhat simple description. Let U ∈ tr M + , and

We unfold this equality further in the special case of "level 2 trees", i.e. those trees V ∈ tr M + whose leaf addresses are of the form

Trees of this form are the operations of M + ⊙ M + . We can decompose V as

where

is a node address of T , so we may decompose it as

and

The rest of this section is dedicated to prove that A.2.2 indeed defines a monad. We thus check the conditions of theorem A.1.9 on page 72.

Proof of (Trivial

is given by Y ○

[r]