of plane trees (i.e., it is a wide subcategory), but the converse is not true as the following example illustrates:

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

Joyal used this more relaxed definition of tree morphism in order to axiomatize a notion of $\omega$-category, and his category of trees, which is equivalent to the category $\Omega$ studied by Batanin and Street [5], satisfies some important universal properties (see Theorems 1 and 2 of [5]). Despite being a non-full subcategory of the Joyal-Batanin-Street category of trees, the category of plane trees $\mathbf{PTree}$ defined above as a full subcategory of $[\omega^{op}, \Delta]$ also seems to us very natural.

Let us now prove that $\mathbf{PTree}$ corresponds to the fiber over 0 of the free bifibration generated by $p_\omega$. In order to prove this we give a more general characterization of the fiber categories $\mathcal{Bif}(p_\omega)_k$ for arbitrary $k \ge 0$. We write $\mathbf{PTree}_{\perp(k)}$ for the category whose objects are rooted plane trees with a marked vertex of height $k$ on their leftmost branch, and whose arrows are morphisms of plane trees preserving the mark. It is clear that $\mathbf{PTree} \cong \mathbf{PTree}_{\perp(0)}$, since every tree morphism $S \to T$ sends the root of $S$ to the root of $T$, and also that every tree in $\mathbf{PTree}_{\perp(k)}$ must have height at least $k$. But not every morphism between trees of height $\ge k$ is a morphism in $\mathbf{PTree}_{\perp(k)}$. For example, one of the two tree morphisms $S \to T$ depicted in (5.1) lifts to a morphism in $\mathbf{PTree}_{\perp(2)}$ (the one in blue), but the other (in red) only lifts to $\mathbf{PTree}_{\perp(1)}$.

Objects of $\mathcal{Bif}(p_\omega)_k$ may be interpreted as left-marked trees: the idea is that a bifibrational formula in $S \subset k$, corresponding to a walk that starts at height 0 and ends at height $k$, may be read as describing a walk from right to left along the tree that stops at the marked node. Under this correspondence, extending a walk by an up-step $k \to k+1$ corresponds to growing a fresh marked leaf as a left child of the marked node, while extending a walk by a down-step $k+1 \to k$ corresponds to moving the marked node down towards the root. We call these respective operations $L_k$ and $R_k$, and illustrate them below on an example for the case $k=2$:

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

It is easy to see that $L_k$ and $R_k$ extend to functors defining a family of adjunctions

<figure><img src="image_58.png" /></figure>
between the categories of left-marked plane trees.

**Theorem 5.3.** Let $F : \omega \to \text{Adj}$ be the functor sending $k$ to $\text{PTree}_{\perp(k)}$ and each arrow $f_k : k \to k+1$ to the adjunction $L_k \to R_k$ defined above. Let $p_\omega : 1 \to \omega$ be the functor mapping $*$ to $0$. Then the unique morphism of bifibrations $\text{Bif}(p_\omega) \to \int_\omega F$ sending the atomic formula $*$ to the one-vertex tree $\bullet$ is an equivalence of categories. In particular, $\text{PTree}$ is equivalent to $\text{Bif}(p_\omega)_0$.

*Proof.* Since $\pi_F(\bullet) = 0 = p_\omega(*)$, the universal property of the free bifibration determines a unique morphism of bifibrations $\llbracket - \rrbracket_\bullet : \text{Bif}(p_\omega) \to \int_\omega F$ mapping $*$ to $\bullet$.

On objects, $\llbracket - \rrbracket_\bullet$ interprets a bifibrational formula $T$ as the left-marked tree $\llbracket T \rrbracket_\bullet$ encoded by the corresponding walk. This mapping is surjective since every such tree is described by a unique walk. (It is many-to-one, since many formulas isomorphic by the pseudofunctoriality laws represent the same walk.)

As a morphism of bifibrations, the mapping on arrows is determined by its action on the homsets of the fiber categories. We now give an explicit description of a family of bijections

$$ (\psi_k)_{S,T} : \text{Bif}(p_\omega)_k(S,T) \xrightarrow{\sim} \text{PTree}_{\perp(k)}(\llbracket S \rrbracket_\bullet, \llbracket T \rrbracket_\bullet) $$

mapping zigzag morphisms to plane tree morphisms. Since these bijections are natural in $S$ and $T$, they uniquely determine $\llbracket - \rrbracket_\bullet : \text{Bif}(p_\omega) \to \int_\omega F$ as a morphism of bifibrations. We conclude that $\llbracket - \rrbracket_\bullet$ is both surjective on objects and fully faithful, hence an equivalence.

To define $\psi_k$, we rely on an inductive characterization of plane tree morphisms that we show can be reflected in both $\text{PTree}_{\perp(k)}$ and $\text{Bif}(p_\omega)_k$. Let us begin by illustrating this bijection in the case $k=0$, before explaining how to generalize it to arbitrary $k \ge 0$.

**Bijection for the case $k=0$.** A plane tree can be described inductively as a root node with a list of plane trees as children. In other words, a tree is built by taking a (possibly empty) forest of trees, and attaching the root of each tree in the forest to a new root vertex. The following grammar summarizes this inductive structure, where $T$ ranges over trees and $\Phi$ over forests:

$$ T ::= \bullet\Phi \qquad \Phi ::= \cdot | T, \Phi' \qquad (5.3) $$

Order-preserving morphisms of plane trees can similarly be defined inductively. We find it convenient to introduce two auxiliary judgments $\Phi \to T$ and $\Phi' \to \Phi$, describing forest-to-tree morphisms and forest-to-forest morphisms, respectively; we then consider tree morphisms as a special case of forest-to-tree morphisms with a singleton forest as input. The two kinds of morphisms can be built inductively using the following rules:

$$ \frac{\Phi'_1, \dots, \Phi'_i \to \Phi}{\bullet\Phi'_1, \dots, \bullet\Phi'_i \to \bullet\Phi} \qquad \frac{\Phi'_1 \to T_1 \quad \dots \quad \Phi'_n \to T_n}{\Phi'_1, \dots, \Phi'_n \to T_1, \dots, T_n} \qquad (5.4) $$

The forest-to-tree rule (on the left) expresses that the root nodes of the input forest are necessarily mapped to the unique root of the output tree, so it suffices to provide a forest-to-forest morphism at height 1. The forest-to-forest rule (on the right) expresses that a morphism into a forest with $n$ trees is determined by an ordered partition of the input forest into $n$ subforests together with a list of forest-to-tree morphisms.
It is clear that morphisms in PTree may be constructed inductively in this way—to see this, it is helpful to begin by observing that there is an isomorphism

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

where PForest is the category of (finite rooted) plane forests, that is, the full subcategory of $[\omega^{op}, \Delta]$ spanned by the functors $\Phi : \omega^{op} \to \Delta$ that eventually vanish $\Phi(k) = 0$ (with no constraint on $\Phi(0)$). Indeed, any natural transformation $\theta : S \to T$ in PTree is uniquely determined at height 0 (since $S(0) = T(0) = 1$) and induces a natural transformation $\theta' : \Phi_S \to \Phi_T$ in PForest between the underlying forests, where $S = \bullet\Phi_S$ and $T = \bullet\Phi_T$. The height 0 component of such a natural transformation $\theta'_0 : \Phi_S(0) \to \Phi_T(0)$ determines an ordered partition of the roots of $\Phi_S$ into $n$ components, where $\Phi_T = T_1, \dots, T_n$. By naturality of $\theta'$, this extends to an ordered partition of the forest itself $\Phi_S = \Phi'_1, \dots, \Phi'_n$, together with a list of natural transformations $\theta_1 : \Phi'_1 \to T_1, \dots, \theta_n : \Phi'_n \to T_n$.

Let us now explain how to similarly decompose morphisms in $\mathcal{Bif}(p_\omega)_0$, illustrating with an example. Consider the maximally multifocused proof below, which we will see corresponds to the blue morphism in (5.1):

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

We have rotated the proof 90 degrees clockwise to better fit on the page. It should be read as a morphism $S \to T$ from the zigzag $S$ at the top to the zigzag $T$ at the bottom. Remember that each zigzag describes a walk along the contour of a tree.

The idea is to begin by splitting the proof along $0=0$ boundaries:

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

This splits the proof into exactly $n$ components, where $T = \bullet(T_1, \dots, T_n)$. Next, in each of these components, we “gray out” the chords that are incident to 0:

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

Each component now implicitly describes a forest-to-tree morphism $\Phi_i \to T_i$, where $S = \bullet\Phi_S$ and $\Phi_1, \dots, \Phi_n$ is an ordered partition of $\Phi_S$. If we remove the grayed-out chords and shift levels—in terms of the sequent calculus, this corresponds to removing the pair of $R^-$ and $R^+$ steps bracketing each component, as well as a list of pairs of $L^-$ and $L^+$ steps—then we can iterate the process on smaller proofs. Eventually we obtain a full recursive decomposition of the original zigzag morphism $S \to T$ using the inductive rules in (5.4), which we can play back as a morphism $[[S]]_\bullet \to [[T]]_\bullet$ in PTree. This defines the bijection $\psi_k$ for the case $k=0$.
The bijection may be better visualized by imagining the string diagram for the zigzag morphism as a kind of topographic relief map:

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

The source and target trees are rooted at the North and South ends of this map, with the morphism exhibiting a continuous deformation between them.

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

**Bijection in the general case.** The inductive procedure we have sketched may be adapted to the general case $k \ge 0$ by extending the rules (5.3) and (5.4) to represent trees with a marked node on their leftmost branch. We begin by introducing a grammar of formulas for marked trees $\circ T$ and marked forests $\circ \Phi$:

$$ \circ T ::= \circ \Phi | \bullet \circ \Phi \qquad \circ \Phi ::= \circ T, \Phi' \qquad (5.5) $$

A marked forest $\circ \Phi$ starts with a marked tree $\circ T$ followed by an unmarked forest $\Phi'$. A marked tree $\circ T$ can be built either by taking an unmarked forest $\Phi$ and attaching the root of each tree to a marked root vertex, $\circ \Phi$, or by taking a marked forest $\circ \Phi$ and attaching each of its roots to a new unmarked root vertex, $\bullet \circ \Phi$. We introduce two additional judgments $\circ \Phi \to_k \circ T$ and $\circ \Phi' \to_k \circ \Phi$ defining marked-forest-to-marked-tree and marked-forest-to-marked-forest morphisms, where the index $k$ specifies the height of the mark:

$$ \frac{\Phi'_0, \Phi'_1, \dots, \Phi'_i \to \Phi}{\circ \Phi'_0, \bullet \Phi'_1, \dots, \bullet \Phi'_i \to_0 \circ \Phi} \qquad \frac{\circ \Phi'_0, \Phi'_1, \dots, \Phi'_i \to_k \Phi}{\bullet (\circ \Phi'_0), \bullet \Phi'_1, \dots, \bullet \Phi'_i \to_{k+1} \circ \Phi} \qquad \frac{\circ \Phi'_0 \to_k \circ T \quad \Phi \to \Phi'}{\circ \Phi'_0, \Phi \to_k \circ T, \Phi'} \qquad (5.6) $$

The key invariant enforced by these rules is that the marked node of the forest on the left is sent to the marked node of the tree or forest on the right. Just as we argued for PTree, it is clear that any morphism in PTree$_{⊥}(k)$ may be built inductively using the above rules.

Similarly, for $k > 0$, the string diagrams of morphisms in $\mathcal{Bif}(p_\omega)_k$ may be decomposed recursively by first splitting along $0 = 0$ boundaries essentially as before, with the difference that the bottom boundary (corresponding to the left side in our rotated diagrams) is of the form $k = k$. For example, the following diagram represents a morphism in $\mathcal{Bif}(p_\omega)_2$:

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

After splitting along $0 = 0$ boundaries, we obtain as before a list of components that may be interpreted as morphisms in $\mathcal{Bif}(p_\omega)_0$, except for the leftmost component which may
be reduced to a morphism in $\mathcal{Bif}(p_\omega)_1$ after removing the chords incident to 0 and shifting levels. We recognize the inductive structure of marked morphisms of (5.6).

**Naturality.** Finally we need to show that the bijections $(\psi_k)_{S,T}$ are natural in $S$ and $T$, which is equivalent to functoriality: $\psi_k(\alpha \cdot \beta) = \psi_k(\alpha) \cdot \psi_k(\beta)$ for every pair of composable zigzag morphisms $\alpha$ and $\beta$.

For example, consider our above example restricted to a prefix for clarity, along with a second morphism which is composable along the middle zigzag formula, as represented on the right.

These morphisms can be seen as relief maps: the tree morphism in $T \to T'$ is determined by the order-preserving functions $T(n) \to T'(n)$ between nodes of height $n$, which can be read from the $n$-th layer of the relief map.

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

If the two diagrams are composable, then each layer of the relief map is composable:

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

For each layer of the relief map, the order-preserving function is determined by connectedness in the diagram: each node in the input tree is related to the (unique) node in the output tree that belongs to the same connected component. This property of connectedness is preserved by diagrammatic concatenation: the connectedness relation of the composite diagram (corresponding to a layer of $\alpha \cdot \beta$) is the composition of the connectedness relations of the two diagrams. $\square$

**Proposition 5.1** is a corollary of Theorem 5.3, since the bijection between zigzags and plane trees sends zigzags that strictly alternate between 0 and 1 to trees of height 1, which may be interpreted as ordinals.

The correspondence established in Theorem 5.3 was unexpected to us, and we think its interest is that it relates two very different representations of the same categories. The calculus of maximally multifocused proofs gives an effective procedure for enumerating tree morphisms by building them up step-by-step in a linear fashion, very differently from how one might first attempt to define a natural transformation through some ad hoc procedure, or even using the inductive rules (5.4) and (5.6) described in the proof of the theorem (which are easy enough to formulate but non-linear in the sense that some of the rules have more than one premise). In Figure 7, we show the maximally multifocused proofs (and associated string diagrams) representing all morphisms $\alpha : S \to T$ between the pair of trees (5.1).
<figure><img src="image_68.png" /><figcaption>Figure 7: An exhaustive listing of maximally multifocused derivations representing all morphisms $\alpha : S \to T$ between a pair of plane trees. The derivations corresponding to the two natural transformations in (5.1) are highlighted in blue and red.</figcaption></figure>

considered earlier. These were generated by applying the proof search procedure described in Section 3.6, which we implemented as a short Haskell program.<fnref n="3" />

Before moving on to the last example, let us make one more easy observation about $\mathcal{Bif}(p_\omega)$. The ordinal $\omega$ may be seen as the category of elements of the regular action of the monoid of natural numbers $(\mathbb{N}, +, 0)$ on itself. In particular, there is an evident forgetful functor $\delta : \omega \to \mathbb{B}_{\mathbb{N}}$ into the monoid of natural numbers seen as the one-object category freely generated on a loop $f \stackrel{*}{\rightleftharpoons}$. This functor sends every pair of natural numbers $m \le n$

<footnote n="3">³ Available at github.com/noamz/free-bifibrations. This implementation was useful to us for running experiments, formulating conjectures, and generating diagrams. Counting proofs using this procedure even helped to reveal a bug in a previous incorrect formulation of the lock conditions for maximally multifocused proofs, before we arrived at the correct version in Section 3.6.</footnote>
to the unique arrow $f^k : * \to *$ such that $k = n - m$; since $\omega$ is a poset, $\delta$ is trivially a faithful functor.

**Proposition 5.4.** If $\delta : \mathcal{C} \to \mathcal{B}$ is a faithful functor then the induced morphism of bifibrations

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

is full and faithful relative to $\delta$, in the sense that the induced mapping on relative homsets $\mathrm{Bif}(p)_f(S, T) \to \mathrm{Bif}(\delta \circ p)_{\delta f}(\Lambda_\delta S, \Lambda_\delta T)$ is a bijection for all compatible $S, f, T$. (Equivalently, the induced functor from $\mathrm{Bif}(p)$ into the fiber product $\mathcal{C}_{\delta \times_{\Lambda_\delta \circ p}} \mathrm{Bif}(\delta \circ p)$ is fully faithful in the ordinary sense.)

*Proof.* The existence of the morphism of bifibrations $\Lambda_\delta : \Lambda_p \to \Lambda_{\delta \circ p}$ comes from the extended universal property (0.5) of the free bifibration $\Lambda_p$ and corresponds to functoriality of the $\Lambda$ construction. It has a simple inductive definition:

$$ \Lambda_{\delta} X = X $$

$$ \Lambda_{\delta}(f^{+} S) = (\delta f)^{+} \Lambda_{\delta} S $$

$$ \Lambda_{\delta}(g^{-} T) = (\delta g)^{-} \Lambda_{\delta} T $$

$$ \Lambda_{\delta}(f \backslash_{g} \alpha) = \delta f \backslash_{\delta g} \Lambda_{\delta} \alpha \quad \Lambda_{\delta}(\alpha.f) = \Lambda_{\delta} \alpha.\delta f \quad \Lambda_{\delta}(\bar{g}.\alpha) = \bar{\delta g} \cdot \Lambda_{\delta} \alpha \quad \Lambda_{\delta}(\alpha f / \bar{g}) = \Lambda_{\delta} \alpha \delta f / \bar{\delta g} $$

The action of $\Lambda_\delta$ may be even easier to see in terms of the double category of zigzags: every arrow of every generator is simply hit with the functor $\delta$. For example, every $\mathbf{L}f^+$-cell of $\mathbb{Z}(\mathcal{C})$ is mapped to a $\mathbf{L}(\delta f)^+$-cell of $\mathbb{Z}(\mathcal{B})$, and every $\mathbf{L}g^-$-cell to a $\mathbf{L}(\delta g)^-$-cell:

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

In general, we obtain a mapping of relative homsets of the form:

$$ \mathrm{Bif}(p)_f(S, T) \to \mathrm{Bif}(\delta \circ p)_{\delta f}(\Lambda_\delta S, \Lambda_\delta T) $$

By inspection of the action on the generators, we can see that surjectivity of this mapping reduces to functoriality of $\delta$, and that injectivity reduces to faithfulness. $\square$

**Corollary 5.5.** Let $!_N : 1 \to \mathbf{B}_N$ be the unique functor of one-object categories corresponding to the unique monoid homomorphism from the trivial monoid into $(\mathbb{N}, +, 0)$. Then the induced morphism of bifibrations $\Lambda_\delta : \Lambda_{p_\omega} \to \Lambda_{!_N}$ is fully faithful relative to $\delta : \omega \to \mathbf{B}_N$. In particular, PTree is equivalent to the full subcategory of the fiber category $\mathrm{Bif}(!_N)_*$ spanned by the objects in the image of $\Lambda_\delta$.

*Proof.* We apply Proposition 5.4 substituting $!_N = \delta \circ p_\omega$. Then we instantiate the bijection of relative homsets $\mathrm{Bif}(p_\omega)_f(S, T) \cong \mathrm{Bif}(!_N)_{\delta f}(\Lambda_\delta S, \Lambda_\delta T)$ at $f = \mathrm{id}_0$, $\delta f = \mathrm{id}_*$ and conclude using Theorem 5.3. $\square$

The category $\mathrm{Bif}(!_N)$ is in some sense more fundamental than $\mathrm{Bif}(p_\omega)$. Its objects may be interpreted as arbitrary one-dimensional walks, starting at the $x$-axis and moving up and
whose image avoids element $i$. Moreover, these generators satisfy the following standard equations (please recall that we write composition in diagrammatic order):

$$ \delta_i^n \delta_{j+1}^{n+1} = \delta_j^n \delta_i^{n+1} \qquad \text{if } i \le j \qquad (5.9) $$

$$ \sigma_{j+1}^{n+1} \sigma_i^n = \sigma_i^{n+1} \sigma_j^n \qquad \text{if } i \le j \qquad (5.10) $$

$$ \delta_i^n \sigma_j^n = \sigma_{j-1}^{n-1} \delta_i^{n-1} \qquad \text{if } i < j \qquad (5.11) $$

$$ = \mathrm{id}_n \qquad \text{if } i = j \text{ or } i = j + 1 \qquad (5.12) $$

$$ = \sigma_j^{n-1} \delta_{i-1}^{n-1} \qquad \text{if } i > j + 1 \qquad (5.13) $$

Now let $\mathcal{P} = \{\sigma_i^n | 0 \le i < n\}$ and $\mathcal{N} = \{\delta_i^n | 0 \le i \le n\}$ and consider the free $(\mathcal{P}, \mathcal{N})$-fibration generated by the inclusion $i: \mathbb{N} \to \Delta$ of the set of natural numbers viewed as a discrete category into the simplex category. Since $\mathcal{P}$ and $\mathcal{N}$ generate the epis and monos respectively, $\mathcal{P}^* = \Delta_{\mathrm{epi}}$, $\mathcal{N}^* = \Delta_{\mathrm{mono}}$, we have that $\mathrm{Bif}(i, \mathcal{P}, \mathcal{N}) \simeq \mathrm{Bif}(i, \Delta_{\mathrm{epi}}, \Delta_{\mathrm{mono}})$ by Prop. 4.3, and so $\Lambda_{i, \mathcal{P}, \mathcal{N}}: \mathrm{Bif}(i, \mathcal{P}, \mathcal{N}) \to \Delta$ is the free (epi, mono)-ambifibration on $i$.

The universal property of $\mathrm{Bif}(i, \mathcal{P}, \mathcal{N})$ and the equation $i = \mathrm{cod} \circ j$ imply that there is a canonical morphism of (epi, mono)-ambifibrations $\mathrm{Bif}(i, \mathcal{P}, \mathcal{N}) \to \Delta$.

Let us now forget about this connection with fat Delta, and just make some combinatorial observations about $\mathrm{Bif}(i, \mathcal{P}, \mathcal{N})$. We refer to objects of $\mathrm{Bif}(i, \mathcal{P}, \mathcal{N})$ as *ambisimplicial formulas*, and will pay particular attention to formulas $S \subset 0$, which we call *closed*. Observe that a closed ambisimplicial formula corresponds to a walk $n \rightsquigarrow 0$ along the graph below:

$$ 0 \longrightarrow 1 \longrightarrow 2 \longrightarrow \cdots \longrightarrow 3 \longrightarrow \cdots $$

At each positive ordinal $k+1$, we choose to either pull along some $\delta_i^k$ or push along some $\sigma_i^k$. Hence there are double factorial $(2n-1)!! = (2n-1) \cdot (2n-3) \cdots 3 \cdot 1$ many such formulas with source $\chi(S) = n$. The double factorial numbers are known to have many different combinatorial interpretations [11], and we state here another: they count $n$-leaf *increasing binary forests*, by which we mean a planar forest of binary trees where every binary node and every root node is assigned a distinct label in such a way that the labels increase when moving from parent to child, and from a binary node bounding a region to a root contained in that region. See Figure 8.

To interpret a closed ambisimplicial formula $S$ as an increasing binary forest, the idea is to start by drawing the $\chi(S) = n$ edges, and then to progressively add either a binary node (joining two edges into one) or a root node (terminating an edge), labelled $m$ and attached to the $i$th free edge, depending on whether we pushed along an epi $\sigma_i^m: m+1 \to m$ or pulled along a mono $\delta_i^m: m \to m+1$ in constructing the formula. For example, here is how we build the increasing binary forest corresponding to the formula $\delta_0^{0-} \sigma_0^{1+} \delta_1^{2-} 3$:

<figure><img src="image_71.png" /></figure>
<figure><img src="image_72.png" /><figcaption>Figure 8: Depiction of all 15 closed ambisimplicial formulas with $\chi(S) = 3$ as increasing binary forests. The labels A–G indicate the split into seven equivalence classes.</figcaption></figure>

Now, let us quickly point out that different forests/formulas can be *isomorphic* in the category Bif($i$, $\mathcal{P}$, $\mathcal{N}$). In particular, equations (5.9) and (5.10) induce natural isomorphisms

$$ \delta_i^{n-} \delta_{j+1}^{n+1-} S \equiv \delta_j^{n-} \delta_i^{n+1-} S \qquad (5.14) $$

$$ \sigma_i^{n+} \sigma_{j+1}^{n+1+} S \equiv \sigma_j^{n+} \sigma_i^{n+1+} S \qquad (5.15) $$

for all $i \le j$. In Figure 8 we indicate the equivalence classes for the case $\chi(S) = 3$ by the letters A–G. Each of these equivalence classes may be canonically represented by a strictly alternating zigzag in $\mathbb{Z}(\Delta, \Delta_{\text{epi}}, \Delta_{\text{mono}})$, as per the following correspondence for the seven equivalence classes of the figure (we only label the arrows that are not uniquely determined):

$$ \begin{array}{lclcl} A = 0 \to 3 & B = 0 \to 2 & \xleftarrow{\sigma_0} & C = 0 \to 2 & \xleftarrow{\sigma_1} \\ D = 0 \to 1 & E = 0 \to 1 & \xleftarrow{\delta_1} & F = 0 \to 1 & \xleftarrow{\delta_2} \end{array} \qquad \begin{array}{lclcl} \sigma_0 & \equiv & 3 & \sigma_1 & \equiv & 3 \\ \sigma_1 & \equiv & 3 & \sigma_2 & \equiv & 3 \end{array} $$

The sequence counting the number of equivalence classes of closed ambisimplicial formulas, 1, 1, 2, 7, 35, 226, 1787, 16717, ...,

is apparently OEIS A014307, known to have various other interpretations [46].

Perhaps most interestingly, the remaining equations of the simplex category (5.11)–(5.13), which mix $\delta$ and $\sigma$, induce non-invertible *logical entailments* between formulas:

$$ \sigma_{j-1}^{n-1+} \delta_i^{n-} S \implies \delta_i^{n-1-} \sigma_j^{n+} S \qquad \text{if } i < j \qquad (5.16) $$

$$ \delta_i^{n-} S \implies \sigma_j^{n+} S \qquad \text{if } i = j \text{ or } i = j + 1 \qquad (5.17) $$

$$ \sigma_j^{n-1+} \delta_i^{n-} S \implies \delta_{i-1}^{n-1-} \sigma_j^{n+} S \qquad \text{if } i > j + 1 \qquad (5.18) $$
Conversely, we will begin by showing more generally that if $\alpha : S \implies_f T$ is an arrow of $\mathbf{Bif}(i, \mathcal{P}, \mathcal{N})$ and $f = em$ is the epi-mono factorization of the underlying arrow in $\Delta$, then $e^+ S \leq m^- T$ in the appropriate poset $F_{k,n}$ with $n = \chi(S) = \chi(T)$ and $k = \text{cod}(e) = \text{dom}(m)$. We prove this by induction on derivations. The interesting case is when $\alpha$ ends in a non-invertible rule, for example suppose it is of the form $\alpha = \bar{g} \cdot \alpha' : g^- S \implies_{gh} T$ for some $\alpha' : S \implies_h T$ and $g \in \mathcal{N} \subset \Delta_{\text{mono}}$. By the induction hypothesis, we have that $e^+ S \leq m^- T$ where $h = em, e \in \Delta_{\text{epi}}, m \in \Delta_{\text{mono}}$. Let $f = dk, d \in \Delta_{\text{epi}}, k \in \Delta_{\text{mono}}$ be the epi-mono factorization of $f = gh$. Thus we have $dk = gem$. By the orthogonal lifting property there is a unique mono $\ell$ making the diagram below commute:

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

Hence $d^+ g^- S \leq \ell^- e^+ S \leq \ell^- m^- T \equiv k^- T$, where the first entailment is an instance of the (abcd) scheme on the square $ge = d\ell$. (Here we need a lemma that every instance of the scheme is valid, $c^+ a^- S \leq d^- b^+ S$, for $a, b \in \Delta_{\text{epi}}$ and $c, d \in \Delta_{\text{mono}}$, which we can prove by induction on the length of the $\mathcal{P}$-factorization of $c$.)

Finally, to establish the equivalence $\mathbf{Bif}(i, \mathcal{P}, \mathcal{N})_k \simeq \coprod_{n \in \mathbb{N}} F_{k,n}$ we need to verify that the fiber categories are preorders. In fact, we claim that the total category $\mathbf{Bif}(i, \mathcal{P}, \mathcal{N})$ is itself a preorder: for any pair of ambisimplicial formulas $S \subset \mathbf{n}, T \subset \mathbf{m}$ there exists at most one arrow $\alpha : S \implies_f T$ lying over a unique order-preserving function $f : \mathbf{n} \to \mathbf{m}$. Intuitively, the reason why is that left division by an epi $e$ and right division by a mono $m$ are *deterministic* and *independent* operations:

* determinism: given an arrow $f$, there is at most one $g$ such that $f = eg$ and at most one $h$ such that $f = hm$, so given any derivation $\alpha$ with underlying base arrow $f$, we can write $e \setminus \alpha$ and $\alpha / \bar{m}$ rather than $e \setminus g \alpha$ and $\alpha h / \bar{m}$ without risk of ambiguity;

* independence: if $\alpha$ is divisible on the left by $e$ and divisible on the right by $m$ (i.e., both $e \setminus \alpha$ and $\alpha / \bar{m}$ are defined), then it is simultaneously divisible on the left and right (i.e., $e \setminus \alpha / \bar{m}$ is defined), by the orthogonal lifting property:

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

Determinism and independence imply that any two derivations of arrows $\alpha_1, \alpha_2 : S \to T$ are permutation equivalent: they necessarily perform the same series of multiplication and division operations, although not necessarily in the same order, but if we examine the first place that they differ — say that $\alpha_1$ performs a left division $e \setminus \beta$ and $\alpha_2$ a right division $\beta / \bar{m}$ — then we can always replace that by a bi-division $e \setminus \beta / \bar{m}$ and continue unifying the rest of the proofs. $\square$

We remark that since $\Delta$ is both $\mathcal{P}$-FP and $\mathcal{N}$-FP (like any category relative to a class of epis and monos), every entailment $S \leq T$ in $F_{k,n}$ is witnessed by a unique maximally multifocused proof $\alpha : S \implies T$. For example, below on the right we show the maximally multifocused proof corresponding to the forest entailment on the left (we work with strictly alternating zigzags, using graphical conventions for the corresponding forests that should be clear, and we notate order-preserving functions $f : \mathbf{n} \to \mathbf{m}$ by tuples of numbers $a_0, \dots, a_{m-1}$ that
indicate the cardinalities of the fibers $a_i = |f^{-1}(i)|)$:

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

The $(F_{k,n})_{n \in \mathbb{N}}$ seem to define an interesting family of posets. For example, we observe that $F_{0,n}$ contains the *lattice of noncrossing partitions* as a quotient. A noncrossing partition of order $n$ is a partition of the ordinal $\mathfrak{n} = \{0, \dots, n-1\}$ such that the diagram defined by drawing the elements in order and then connecting all of the elements within the same block by a corolla is planar. For example, of the $\begin{Bmatrix} 4 \\ 2 \end{Bmatrix} = 7$ partitions of 4 into two blocks, all but one are noncrossing:

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

The restriction of the usual refinement ordering to noncrossing partitions of order $n$ defines a poset $K_n$ known as the *Kreweras lattice*.

**Proposition 5.7.** $K_n$ is the quotient of $F_{0,n}$ obtained by inverting (5.16) and (5.18), or equivalently by imposing the Beck-Chevalley condition on the free ambifibration $\Lambda_{i,\mathcal{P},\mathbb{N}}$.

*Proof.* The squares corresponding to equations (5.11) and (5.13) are pullback squares in $\Delta$, and hence the respective natural transformations (5.16) and (5.18) become invertible if one assumes the BC condition. The noncrossing partition associated to a closed ambisimplicial formula is obvious if one looks at the corresponding increasing forest, since imposing (5.16) and (5.18) as equivalences in addition to (5.14) and (5.15) has the effect of forgetting the
order in which nodes are created and reducing the forest down to its connected components. For instance, formulas $A_1-A_6$ from Figure 8 correspond to the partition $\{\{0\}, \{1\}, \{2\}\}$, while formulas $C_1, C_2$, and $D_1$ correspond to the partition $\{\{0\}, \{1, 2\}\}$. The only remaining law (5.17) (see right side of (5.19) for its diagrammatic depiction) exactly describes the covering relation for the refinement order on noncrossing partitions. $\square$

For example, $K_3$ is obtained from $F_{0,3}$ by identifying two pairs of equivalence classes $C \sim D$ and $B \sim G$. Proposition 5.7 and the seminal results of Kreweras [31] on the lattice of noncrossing partitions as well as related results for other Catalan lattices [7] motivate us to ask two open questions.<fnref n="4" />

**Question 5.8.** $K_n$ is a lattice for all $n$: is $F_{0,n}$ (and more generally $F_{k,n}$) likewise a lattice?

**Question 5.9.** The number of intervals $I[K_n] = \{(x, y) | x \le y\}$ in $K_n$ is given by a simple formula $|I[K_n]| = \frac{1}{2n+1} \binom{3n}{n}$: is there likewise a nice formula for $|I[F_{0,n}]|$ (and more generally for $|I[F_{k,n}]|$)?

It is known that the lattice of noncrossing partitions is self-dual $K_n \cong K_n^{op}$, and even *locally self-dual* in the sense that for every pair of noncrossing partitions $x, y \in K_n$, the restriction of $K_n$ to the interval $[x, y]$ is self-dual [52, V2:465]. It may be interesting to study this duality from a fibrational perspective, in particular relating it to the duality between $\Delta$ and the category of finite strict intervals and order-and-boundary-preserving maps [26, §1.1].

## 6. CONCLUSION AND FUTURE DIRECTIONS

This work originally began as an exercise in categorical proof theory, with our hope being that a systematic understanding of the construction of the free bifibration on a functor of categories $p: \mathcal{D} \to \mathcal{C}$ could eventually help in analyzing more complex fibrational situations that arise in logic and type theory. This “easy” exercise proved more challenging than we expected (particularly the question of characterizing normal forms to obtain a canonicity result), but was also rewarding as we realized the implicit complexity and richness contained in the problem. We were encouraged by the close connection between the sequent calculus presentation of the free bifibration and the presentation of the double category of zigzags by generators and relations, showing the unity of purpose between two basic tools in the proof-theoretic and category-theoretic repertoires; and we were excited to discover the examples of free bifibrations and ambifibrations in which the combinatorial complexity emerged from much simpler generating data. We think there are many natural paths for further study.

Perhaps the most obvious next step would be to generalize the constructions beyond functors of categories. As mentioned in the Introduction, we were originally motivated by phenomena that arise when considering bifibrations of monoidal closed categories and of generalized multicategories and polycategories. We expect that the construction of the free bifibration on a functor should generalize to functors of polycategories, but the details are by no means obvious, especially the appropriate generalization of the FP condition and whether there is a reasonable notion of maximal multifocusing. Another natural generalization would be to incorporate higher cells in the base category, such as by considering functors

<footnote n="4">⁴Soon after the original version of this paper was posted, we found out that the answer to Question 5.8 is negative: already $F_{0,4}$ is not a lattice. We thank Wenjie Fang for determining this using SageMath from data provided by our decision procedure for entailment (see Footnote 3).</footnote>
of 2-categories or double categories. Indeed, we already somewhat implicitly treated the base category as a 2-category in our conventions for drawing string diagrams where we represented equalities by vertices, as in Figure 1; taking the base to be an actual 2-category would give this convention a more formal status, and may also make it possible to relax the FP condition while retaining canonicity. It should be noted that Licata, Shulman, and Riley [37] considered bifibrations of cartesian 2-multicategories, and that 2-cells were used to good effect in their notion of “mode theory”.

We used string diagrams in this paper mainly for their evocative power (particularly in the proof of Theorem 5.3), but we believe there is value in taking them seriously as geometric objects and developing a purely topological or purely combinatorial description of free bifibrations. Dawson, Paré, and Pronk did exactly that in their description of $Π_2(C)$ for a free category, defining a bijection between 2-cells in $Π_2(C)$ and isotopy classes of planar diagrams presented by matchings on a set of oriented points. It could be worthwhile to extend such a correspondence for free bifibrations beyond the case of a free base category, to general categories or 2-categories.

Although we did not explore the direction in this paper, there is clearly a link to be developed between bifibrations or $(\mathcal{P}, \mathcal{N})$-fibrations and game semantics [23, 39]. It is noteworthy that the free bifibration on $p_2: 1 \to 2$ appeared incognito in a paper on the categorical combinatorics of innocent strategies [21], with the total category $\mathcal{Bif}(p_2)$ of the free bifibration being equivalent to the authors’ *category of schedules* $\mathcal{Y}$.

The surprising connection between the free bifibration on $p_ω: 1 \to ω$ and the Joyal-Batanin-Street category of plane trees—which contains $\mathcal{Bif}(p_ω)_0$ as a wide subcategory but is not equivalent to it—is still somewhat mysterious to us, and we are not sure whether it is a mere coincidence. Similarly, we do not know whether the free ambifibration on $i: \mathbb{N} \to \Delta$ may (like the fat Delta ambifibration) be useful for defining weak higher categories, but it appears to be an interesting object of study in its own right.

**Acknowledgments.** We warmly thank François Lamarche for stimulating discussions about his work on bifibrations [32, 33] and for his enthusiasm about the project. We also thank Nathanael Arkor, Tom Hirshowitz, Paul-André Melliès, Dorette Pronk, and Gilles Schaeffer for discussions and pointers.

This work began while the three authors were at LIX and the first author was on a postdoc supported by the ANR project Repro (ANR-20-CE48-0016). The third author was partially supported by the ANR project LambdaComb (ANR-21-CE48-0017).

## REFERENCES

[1] Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed categories. *Logical Methods in Computer Science*, 15(1), 2019. doi:10.23638/LMCS-15.1(20)2019.

[2] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *Journal of Logic and Computation*, 2(3):297–347, 1992. doi:10.1093/logcom/2.3.297.

[3] Jean-Marc Andreoli. Focussing and proof construction. *Annals of Pure and Applied Logic*, 107(1):131–163, 2001. doi:10.1016/S0168-0072(00)00032-4.

[4] Claude Auderset. Adjonctions et monades au niveau des 2-catégories. *Cahiers de topologie et géométrie différentielle*, 15(1):3–20, 1974.

[5] Michael Batanin and Ross Street. The universal property of the multitude of trees. *Journal of Pure and Applied Algebra*, 154(1-3):3–13, 2000. doi:10.1016/S0022-4049(99)00184-X.

[6] Jean Bénabou. Distributors at work. Notes from a course at TU Darmstadt in June 2000, taken by Thomas Streicher, 2000. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
[7] O. Bernardi and N. Bonichon. Intervals in Catalan lattices and realizers of triangulations. *Journal of Combinatorial Theory Series A*, 116(1):55–75, 2009. doi:10.1016/j.jcta.2008.05.005.

[8] Nicolas Blanco. Bifibrations of polycategories and classical multiplicative linear logic. PhD thesis, University of Birmingham, 2023. arXiv:2305.15139.

[9] Guillaume Boisseau, Chad Nester, and Mario Román. Cornering optics. In *Proceedings Fifth International Conference on Applied Category Theory*, 2023. doi:10.48550/arXiv.2307.15519.

[10] Francis Borceaux. *Handbook of Categorical Algebra 1: Basic Category Theory*. Cambridge University Press, 1994.

[11] David Callan. A combinatorial survey of identities for the double factorial. arXiv:0906.1317, June 2009.

[12] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, *Fifth IFIP International Conference On Theoretical Computer Science*, pages 383–396. Springer, 2008. doi:10.1007/978-0-387-09680-3_26.

[13] Kevin Coulembier, Ross Street, and Michel van den Bergh. Freely adjoining monoidal duals. *Mathematical Structures in Computer Science*, 31(7):748–768, 2021.

[14] Robert Dawson, Robert Paré, and Dorette Pronk. Adjoining adjoints. *Advances in Mathematics*, 178(1):99–140, 2003. doi:10.1016/S0001-8708(02)00068-3.

[15] Robert Dawson, Robert Paré, and Dorette Pronk. Undecidability of the free adjoint construction. *Applied Categorical Structures*, 11:403–419, 2003. doi:10.1023/A:1025712521140.

[16] Robert Dawson, Robert Paré, and Dorette Pronk. The Span construction. *Theory and Applications of Categories*, 24(13):302–377, 2010. URL: http://www.tac.mta.ca/tac/volumes/24/13/24-13abs.html.

[17] Jacopo Emmenegger, Luca Mesiti, Giuseppe Rosolini, and Thomas Streicher. A comonad for Grothendieck fibrations. *Theory and Applications of Categories*, 40(13):371–379, 2024. URL: http://tac.mta.ca/tac/volumes/40/13/40-13abs.html.

[18] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987.

[19] J. W. Gray. Fibred and cofibred categories. In *Proceedings of the Conference on Categorical Algebra*, pages 21–83. Springer-Verlag, 1966.

[20] Alexander Grothendieck et al. *Revêtements étales et groupe fondamental*, volume 224 of Lecture Notes in Mathematics. Springer-Verlag, 1971. Séminaire de Géométrie Algébrique du Bois Marie 1960–1961 (SGA 1), dirigé par A. Grothendieck, augmenté de deux exposés de M. Raynaud.

[21] Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent strategies. In *22nd IEEE Symposium on Logic in Computer Science*, pages 379–388. IEEE Computer Society, July 2007. doi:10.1109/LICS.2007.14.

[22] Lukas Heidemann, David Reutter, and Jamie Vicary. Zigzag normalisation for associative n-categories. In *37th Annual ACM/IEEE Symposium on Logic in Computer Science*. Association for Computing Machinery, 2022. doi:10.1145/3531130.3533352.

[23] Michel Hirschowitz, André Hirschowitz, and Tom Hirschowitz. A theory for game theories. In *International Conference on Foundations of Software Technology and Theoretical Computer Science*, pages 192–203. Springer, 2007.

[24] Bart P. F. Jacobs. *Categorical Logic and Type Theory*, volume 141 of *Studies in logic and the foundations of mathematics*. North-Holland, 2001.

[25] P. T. Johnstone. A note on discrete Conduché fibrations. *Theory and Applications of Categories*, 5(1):1–11, 1999. doi:10.1017/S0305004108001345.

[26] André Joyal. Disks, duality, and $\theta$-categories. preprint, 1997. URL: https://ncatlab.org/nlab/files/JoyalThetaCategories.pdf.

[27] Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. *Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970*, pages 342–376, 1983.

[28] Anders Kock. Fibrations as Eilenberg-Moore algebras. arXiv:1312.1608, December 2013.

[29] Joachim Kock. Weak identity arrows in higher categories. *International Mathematics Research Papers*, 2006:1–54, 2006.

[30] Joachim Kock. On ternary factorization systems. Comment on an n-Category Café blog post, 2010. URL: https://golem.ph.utexas.edu/category/2010/07/ternary_factorization_systems.html#c034162.

[31] Germain Kreweras. Sur les partitions non-croisées d'un cycle. *Discrete Mathematics*, 1(4):333–350, 1971.

[32] François Lamarche. Path functors in Cat. Unpublished manuscript, 2010. URL: https://hal.inria.fr/hal-00831430.
[33] François Lamarche. Modeling Martin-Löf type theory in categories. *Journal of Applied Logic*, 12:28-44, 2014. doi:10.1016/j.jal.2013.08.003.

[34] Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154-170, 1958. URL: https://www.jstor.org/stable/2310058.

[35] Joachim Lambek. Deductive systems and categories I: Syntactic calculus and residuated categories. *Math. Syst. Theory*, 2(4):287-318, 1968. doi:10.1007/BF01703261.

[36] F. W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In *Proceedings of the AMS Symposium on Pure Mathematics XVII*, pages 1-14, 1970.

[37] Daniel R. Licata, Michael Shulman, and Mitchell Riley. A fibrational framework for substructural and modal logics. In Dale Miller, editor, *2nd International Conference on Formal Structures for Computation and Deduction*, volume 84 of *LIPIcs*, pages 25:1-25:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, September 2017. doi:10.4230/LIPICS.FSCD.2017.25.

[38] Saunders Mac Lane. *Categories for the Working Mathematician*. Springer, 1998.

[39] Paul-André Melliès. Game semantics in string diagrams. In *27th Annual IEEE Symposium on Logic in Computer Science*, pages 481-490. IEEE, 2012. doi:10.1109/LICS.2012.58.

[40] Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In *42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 3-16, January 2015. doi:10.1145/2676726.2679670.

[41] Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of Lawvere's presheaf hyper-doctrine. In *31st Annual IEEE Conference on Logic in Computer Science*, pages 555-564, July 2016. doi:10.1145/2933575.2934525.

[42] Paul-André Melliès and Noam Zeilberger. An Isbell duality theorem for type refinement systems. *Mathematical Structures in Computer Science*, 28(6):736-774, 2018. doi:10.1017/S0960129517000068.

[43] David Jaz Myers. String diagrams for double categories and equipments. arXiv:1612.02762, March 2018.

[44] Chad Nester. The structure of concurrent process histories. In Ferruccio Damiani and Ornela Dardha, editors, *Coordination Models and Languages*, pages 209-224. Springer, 2021. doi:10.1007/978-3-030-78142-2_13.

[45] Stiéphen Pradal. On combinatorial aspects of fat Delta. arXiv:2506.01717, June 2025.

[46] Qingchun Ren. Ordered partitions and drawings of rooted plane trees. *Discrete Mathematics*, 338(1):1-9, 2015. doi:10.1016/j.disc.2014.08.014.

[47] Christian Sattler. Kock's fat $\Delta$ is a direct replacement of $\Delta$. Unpublished note, 2017. URL: https://www.cse.chalmers.se/~sattler/docs/fat-delta.pdf.

[48] Stephen Schanuel and Ross Street. The free adjunction. *Cahiers de topologie et géométrie différentielle catégoriques*, 27(1):81-83, 1986. URL: http://www.numdam.org/item/CTGDC_1986__27_1_81_0/.

[49] Michael Shulman. Framed bicategories and monoidal fibrations. *Theory and Applications of Categories*, 20(18):650-738, 2008. URL: http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html.

[50] Michael Shulman. LNL polycategories and doctrines of linear logic. *Logical Methods in Computer Science*, 19(2), 2023. doi:10.46298/lmcs-19(2:1)2023.

[51] Robert J. Simmons. Structural focalization. *ACM Trans. Comput. Log.*, 15(3):21:1-21:33, 2014. doi:10.1145/2629678.

[52] Richard P. Stanley. *Enumerative Combinatorics: Volumes 1 and 2*. Cambridge University Press, 1999.

[53] Tarmo Uustalu, Niccolò Veltri, and Cheng-Syuan Wan. Proof theory of skew non-commutative MILL. In Andrzej Indrzejczak and Michal Zawidzki, editors, *10th International Conference on Non-Classical Logics*, volume 358 of *EPTCS*, pages 118-135, March 2022. doi:10.4204/EPTCS.358.9.

[54] Niccolò Veltri. Maximally multi-focused proofs for skew non-commutative MILL. In Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors, *29th International Workshop on Logic, Language, Information, and Computation*, volume 13923 of *Lecture Notes in Computer Science*, pages 377-393. Springer, July 2023. doi:10.1007/978-3-031-39784-4\_24.

[55] Christian Williams. *The Metalanguage of Category Theory*. PhD thesis, UC Riverside, 2023. URL: https://escholarship.org/uc/item/84j4z67h.
APPENDIX A. SOME MORE DETAILED PROOFS

A.1. **Section 1.**

**Lemma 1.9.** *Cut is compatible with permutation equivalence. If $\alpha_1 \sim \alpha_2$ then $\alpha_1 \cdot \beta \sim \alpha_2 \cdot \beta$, and $\beta \cdot \alpha_1 \sim \beta \cdot \alpha_2$,*

*Proof.* By symmetry it suffices to prove that $\alpha_1 \cdot \beta \sim \alpha_2 \cdot \beta$. The proof is by case analysis on the proof of $\alpha_1 \sim \alpha_2$: the equivalence and congruence cases are direct induction, the more delicate cases are the generating equations, which require an induction on $\beta$.

**Case** $\overline{f}.(\alpha.h) \sim (\overline{f}.\alpha).h$. To reason about $((\overline{f}.\alpha).h) \cdot \beta$, we perform a case analysis on $\beta$, depending on whether it starts with a left rule or a right rule. (It cannot be an atom as its domain is of the form $h^+ U$.)

If $\beta$ starts with a left rule and its domain is of the form $h^+ U$, we have $\beta = h \backslash_i \beta'$ and

$$ \begin{align*} & (\overline{f}.(\alpha.h)) \cdot \beta \\ & \sim \overline{f}.((\alpha.h) \cdot \beta) \\ &= \overline{f}.((\alpha.h) \cdot (h \backslash_i \beta')) \\ &= \overline{f}.(\alpha \cdot \beta') \\ & \sim (\overline{f}.\alpha) \cdot \beta' \\ &= ((\overline{f}.\alpha).h) \cdot (h \backslash_i \beta') \\ &= ((\overline{f}.\alpha).h) \cdot \beta \end{align*} $$

If $\beta$ starts with a right rule, let us assume that it is a division $\beta = \beta' i / \bar{j}$—the multiplication case is similar. Then we have

$$ \begin{align*} & (\overline{f}.(\alpha.h)) \cdot \beta \\ &= (\overline{f}.(\alpha.h)) \cdot (\beta' i / \bar{j}) \\ & \sim ((\overline{f}.(\alpha.h)) \cdot \beta') fghi / \bar{j} \\ & \sim (((\overline{f}.\alpha).h) \cdot \beta') fghi / \bar{j} \quad \text{by induction hypothesis } (\beta' < \beta) \\ &= ((\overline{f}.\alpha).h) \cdot (\beta' i / \bar{j}) \\ &= ((\overline{f}.\alpha).h) \cdot \beta \end{align*} $$

**Case** $(f \backslash_g \alpha).h \sim f \backslash_{gh} (\alpha.h)$. This proof is in fact identical to the previous one: the proof above only depends on the fact $\overline{f}.\alpha.h$ has a multiplication on the right, not on the operation performed on the left.

**Case** $(\overline{f}.\alpha)_{fg}/\overline{h} \sim \overline{f}.(\alpha_g/\overline{h})$. To reason about $(\alpha_g/\overline{h}) \cdot \beta$, we again reason by case analysis on $\beta$, depending on whether it is a multiplication by $h$ on the left or a right-rule.

If $\beta = \overline{h}.\beta'$, then we have

$$ \begin{align*} & ((\overline{f}.\alpha)_{fg}/\overline{h}) \cdot \beta \\ &= ((\overline{f}.\alpha)_{fg}/\overline{h}) \cdot (\overline{h}.\beta') \\ &= (\overline{f}.\alpha) \cdot \beta' \\ & \sim \overline{f}.(\alpha \cdot \beta') \\ &= \overline{f}.((\alpha_g/\overline{h}) \cdot (\overline{h}.\beta')) \\ &= \overline{f}.((\alpha_g/\overline{h}) \cdot \beta) \\ & \sim (\overline{f}.(\alpha_g/\overline{h})) \cdot \beta \end{align*} $$
If $\beta$ starts with a right rule, for example $\beta = \beta'_{i/\bar{j}}$, then we have

$$ 
\begin{align*}
& ((\bar{f} \cdot \alpha)_{fg/\bar{h}}) \cdot \beta \\
&= ((\bar{f} \cdot \alpha)_{fg/\bar{h}}) \cdot (\beta'_{i/\bar{j}}) \\
&= (((\bar{f} \cdot \alpha)_{fg/\bar{h}}) \cdot \beta')_{fgi/\bar{j}} \\
&\sim (\bar{f} \cdot (\alpha_{g/\bar{h}})) \cdot \beta')_{fgi/\bar{j}} \quad \text{by induction hypothesis } (\beta' < \beta) \\
&\sim (\bar{f} \cdot (\alpha_{g/\bar{h}})) \cdot (\beta'_{i/\bar{j}}) \\
&= (\bar{f} \cdot (\alpha_{g/\bar{h}})) \cdot \beta
\end{align*}
$$

**Case** $(f \backslash_{gh} \alpha)_{g/\bar{h}} \sim f \backslash_g (\alpha_{fg/\bar{h}})$. Again, this proof is identical to the previous case, as they both have a division on the right of $\alpha$. $\square$

**Lemma 1.11 (η-expansion).**

For any $\alpha : f^+ S \implies_g T$, for any $\beta : S \implies_f g^- T$, we have:

$$ \alpha \sim f \backslash_g (f_S \cdot \alpha) \qquad \beta \sim (\beta \cdot \bar{g}_T) f/\bar{g} $$

The proof of this equation is included in the proof of the following lemma.

**Lemma 1.10 (identity is neutral).** *The identity derivations are neutral elements for cut:*

$$ \mathrm{id}_S \cdot \alpha \sim \alpha \sim \alpha \cdot \mathrm{id}_S $$

*Proof.* By induction on $S$. We prove the left neutrality case, right neutrality is symmetric.

**Case X.** If $\alpha$ has an atomic domain or codomain, it must be an atomic derivation $\delta$:

$$ \mathrm{id}_X \cdot \alpha = (\mathrm{id}_X) \cdot \delta = (\mathrm{id}_X \delta) = \delta = \alpha $$

**Case** $f^+ S$.

$$ 
\begin{align*}
& \mathrm{id}_{f^+ S} \cdot \alpha \\
&= (f \backslash_{\mathrm{id}_B} f_S) \cdot \alpha \\
&\sim f \backslash_g (f_S \cdot \alpha)
\end{align*}
$$

We now prove that any $\alpha$ is permutation equivalent to $f \backslash_g (f_S \cdot \alpha)$ by induction on $\alpha$. If $\alpha$ starts with a left rule, we must have $\alpha = f \backslash_g \alpha'$, and then:

$$ 
\begin{align*}
& f \backslash_g (f_S \cdot \alpha) \\
&= f \backslash_g ((\mathrm{id}_S \cdot f) \cdot (f \backslash_g \alpha')) \\
&= f \backslash_g (\mathrm{id}_S \cdot \alpha') \\
&\sim f \backslash_g \alpha' \qquad \text{by induction hypothesis on } S \\
&= \alpha
\end{align*}
$$

If $\alpha$ starts with a right rule, for example $\alpha = \alpha'_{g/\bar{h}}$, we have

$$ 
\begin{align*}
& f \backslash_g (f_S \cdot \alpha) \\
&= f \backslash_g (f_S \cdot (\alpha'_{g/\bar{h}}/\bar{h})) \\
&= f \backslash_g ((f_S \cdot \alpha')_{g/\bar{h}}/\bar{h}) \\
&\sim (f \backslash_g (f_S \cdot \alpha'))_{g/\bar{h}} \\
&\sim \alpha'_{g/\bar{h}} \qquad \text{by induction hypothesis on } \alpha' \\
&= \alpha
\end{align*}
$$
**Case $\bar{g}^T$.**

$$ \begin{aligned} & \mathrm{id}_{\bar{g}^T} \cdot \alpha \\ = & (\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot \alpha \end{aligned} $$

We prove that any $\alpha$ is permutation equivalent to $(\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot \alpha$ by induction on $\alpha$. If $\alpha$ starts with a left rule, we must have $\alpha = \bar{g} \cdot \alpha'$, and so

$$ \begin{align*} & (\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot \alpha \\ = & ((\bar{g} \cdot \mathrm{id}_T) \mathrm{id}_B / \bar{g}) \cdot (\bar{g} \cdot \alpha') \\ = & (\bar{g} \cdot \mathrm{id}_T) \cdot \alpha' \\ \sim & \bar{g} \cdot (\mathrm{id}_T \cdot \alpha') \\ \sim & \bar{g} \cdot \alpha' \qquad \text{by induction hypothesis on } T \\ = & \alpha \end{align*} $$

If $\alpha$ starts with a right rule, for example $\alpha = \alpha' h / \bar{i}$, we have

$$ \begin{align*} & (\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot \alpha \\ = & (\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot (\alpha' h / \bar{i}) \\ = & ((\bar{g}_T \mathrm{id}_B / \bar{g}) \cdot \alpha') h / \bar{i} \\ \sim & \alpha' h / \bar{i} \qquad \text{by induction on } \alpha' \\ = & \alpha \end{align*} $$

□

**Lemma 1.12.** *Cut is associative: $(\alpha \cdot \beta) \cdot \gamma \sim \alpha \cdot (\beta \cdot \gamma)$.*

*Proof.* The proof is by induction on $\alpha, \beta, \gamma$.

If $\alpha$ is an atomic derivation, then $\beta$ and $\gamma$ must be as well—and conversely—and then associativity is immediate:

$$ (\delta \cdot \epsilon) \cdot \zeta = (\delta \epsilon \zeta) = \delta \cdot (\epsilon \cdot \zeta) $$

If $\alpha$ starts with a left rule, then associativity is immediate. For example if $\alpha = \bar{f} \cdot \alpha'$, we have

$$ \begin{align*} & (\alpha \cdot \beta) \cdot \gamma \\ = & ((\bar{f} \cdot \alpha') \cdot \beta) \cdot \gamma \\ \sim & (\bar{f} \cdot (\alpha' \cdot \beta)) \cdot \gamma \\ \sim & \bar{f} \cdot ((\alpha' \cdot \beta) \cdot \gamma) \\ \sim & \bar{f} \cdot (\alpha' \cdot (\beta \cdot \gamma)) \qquad \text{by induction hypothesis } (\alpha' < \alpha) \\ \sim & (\bar{f} \cdot \alpha') \cdot (\beta \cdot \gamma) \\ = & \alpha \cdot (\beta \cdot \gamma) \end{align*} $$

Symmetrically, associativity is immediate if $\gamma$ starts with a right rule. When neither of those two easy cases apply, we know that $\alpha$ starts with a right rule and $\gamma$ with a left rule. We then reason by case analysis on $\beta$.
If $\beta$ starts with a multiplication on the left, $\beta = \bar{g} \cdot \beta'$, then the right rule of $\alpha$ must end a matching division, $\alpha = \alpha' f / \bar{g}$, and we have

$$ \begin{align*} & (\alpha \cdot \beta) \cdot \gamma \\ &= ((\alpha' f / \bar{g}) \cdot (\bar{g} \cdot \beta')) \cdot \gamma \\ &\sim (\alpha' \cdot \beta') \cdot \gamma \\ &\sim \alpha' \cdot (\beta' \cdot \gamma) \qquad \text{by induction hypothesis } (\alpha' < \alpha, \beta' < \beta) \\ &\sim (\alpha' f / \bar{g}) \cdot (\bar{g} \cdot (\beta' \cdot \gamma)) \\ &\sim (\alpha' f / \bar{g}) \cdot ((\bar{g} \cdot \beta') \cdot \gamma) \\ &= \alpha \cdot (\beta \cdot \gamma) \end{align*} $$

The proof is similar if $\beta$ starts with a division on the left, $\beta = g \backslash_h \beta'$ and $\alpha = \alpha' \cdot g$:

$$ \begin{align*} & (\alpha \cdot \beta) \cdot \gamma \\ &= ((\alpha' \cdot g) \cdot (g \backslash_h \beta')) \cdot \gamma \\ &\sim \alpha' \cdot (\beta' \cdot \gamma) \qquad \text{by induction hypothesis } (\alpha' < \alpha, \beta' < \beta) \\ &\sim (\alpha' \cdot g) \cdot (g \backslash_{hi} (\beta' \cdot \gamma)) \\ &\sim (\alpha' \cdot g) \cdot ((g \backslash_h \beta') \cdot \gamma) \\ &= \alpha \cdot (\beta \cdot \gamma) \end{align*} $$

The cases where $\beta$ starts with a right rule are symmetrical. $\square$

## A.2. Section 3.

### Proposition 3.16.

$$ \begin{align*} \forall \alpha_w, \quad \alpha_w &\sim \operatorname{InvSeq}(S(\alpha_w)) \\ \forall \alpha_w, \quad \forall \alpha'_w \in \operatorname{InvSeq}(S(\alpha_w)), \quad \alpha_w &\sim \alpha'_w \end{align*} $$

*Proof.* By induction on the underlying judgment of $\alpha_w$.

* If $\alpha_w$ has a non-neutral judgment $\alpha_w : \pi^+ N \implies_f \bar{\rho}^- P$, we have

$$ S(\alpha_w) := \pi \setminus S(\pi_N \cdot \alpha_w \cdot \bar{\rho}_P) / \bar{\rho} $$

For any $\alpha'_w \in \operatorname{InvSeq}(S(\alpha_w))$, $\alpha'_w$ is one of the two sequentializations of the bi-inversion $\pi \setminus \beta_w / \bar{\rho}$ for some $\beta_w \in \operatorname{InvSeq}(S(\pi_N \cdot \alpha_w \cdot \bar{\rho}_P : N \implies_{\pi f \rho} P))$. Let us show the case

where $\alpha'_w := \pi \setminus (\beta_w / \bar{\rho})$, the other case is similar. By induction hypothesis on the smaller judgment $N \implies_{\pi f \rho} P$, we have $\beta_w \sim (\pi_N \cdot \alpha_w \cdot \bar{\rho}_P)$, and therefore

$$ \begin{align*} \alpha'_w &= \pi \setminus (\beta_w / \bar{\rho}) \\ &\sim \pi \setminus ((\pi_N \cdot \alpha_w \cdot \bar{\rho}_P) / \bar{\rho}) \\ &\sim \pi \setminus (\pi_N \cdot \alpha_w) \\ &\sim \alpha_w \end{align*} $$

where the last two equivalences come from Lemma 1.11.

* Otherwise $\alpha_w$ has a neutral judgment $\alpha_w : N \implies_f P$, and we reason as in the definition of $S(\alpha_w)$ by case analysis on $\alpha_w$, which can be of the form $\bar{\sigma} \cdot \beta_w$ or $\beta_w \cdot \tau$. For example in the case $\bar{\sigma} \cdot \beta_w$ (the other case is symmetric), $N$ is of the form $\sigma^- Q$ and we have

$$ \operatorname{InvSeq}(S(\alpha_w)) = \operatorname{InvSeq}(S(\bar{\sigma} \cdot \beta_w)) = \operatorname{InvSeq}(\bar{\sigma} \cdot S(\beta_w)) $$
For any $\alpha'_w \in \text{InvSeq}(S(\alpha_w))$, $\alpha'_w$ is of the form $\bar{\sigma}.\beta'_w$ for some $\beta'_w \in \text{InvSeq}(S(\beta_w))$. We have $\beta'_w \sim \beta_w$ by induction hypothesis on the smaller judgment $Q \implies P$, and therefore

$$ \alpha'_{w} = \bar{\sigma}.\beta'_{w} \sim \bar{\sigma}.\beta_{w} = \alpha_{w} $$

□

**Proposition 3.17.**

$$ \begin{array}{l} \forall \alpha_m, \quad \alpha_m \sim_{\text{seq}} S(\text{InvSeq}(\alpha_m)) \\ \forall \alpha_m, \forall \alpha_w \in \text{InvSeq}(\alpha_m), \quad \alpha_m \sim_{\text{seq}} S(\alpha_w) \end{array} $$

*Proof.* The statement can in fact be strengthened into the following:

$$ \forall \alpha_w \in \text{InvSeq}(\alpha_m), \quad \alpha_m = S(\alpha_w) $$

This is proved by induction on the judgment of $\alpha_w$ and $\alpha_m$:

* At a non-neutral judgment $\pi^+ N \implies_f \bar{\rho} P$, $\alpha_m$ must be of the form $\pi \setminus \beta_m / \bar{\rho}$ with $\beta_m : N \implies_{\pi f \rho} P$, and $\alpha_w \in \text{InvSeq}(\alpha_m)$ must be a sequentialization of the bi-inversion $\pi \setminus \beta_w / \bar{\rho}$ for some $\beta_w \in \text{InvSeq}(\beta_m)$. By induction hypothesis we have $S(\beta_w) = \beta_m$. If $\alpha_w$ is $\pi \setminus (\beta_w / \bar{\rho})$ (the other case is similar), we have

$$ \begin{align*} S(\alpha_w) &= \pi \setminus S(\pi_N \cdot \alpha_w \cdot \bar{\rho}_P) / \bar{\rho} \\ &= \pi \setminus S(\pi_N \cdot \pi \setminus (\beta_w / \bar{\rho}) \cdot \bar{\rho}_P) / \bar{\rho} \\ &= \pi \setminus S(\beta_w / \bar{\rho} \cdot \bar{\rho}_P) / \bar{\rho} \\ &= \pi \setminus S(\beta_w) / \bar{\rho} \\ &= \pi \setminus \beta_m / \bar{\rho} \\ &= \alpha_m \end{align*} $$

* At a neutral judgment $N \implies_f P$, we reason by case analysis on $\alpha_m$. For example if it is $\bar{\sigma}.\beta_m$ (the other case $\beta_m.\tau$ is similar), we have $\alpha_w = \bar{\sigma}.\beta_w$ for $\beta_w \in \text{InvSeq}(\beta_m)$. We have $S(\beta_w) = \beta_m$ by induction hypothesis, so

$$ S(\alpha_w) = S(\bar{\sigma}.\beta_w) = \bar{\sigma}.S(\beta_w) = \bar{\sigma}.\beta_m = \alpha_m $$

□

**Theorem 3.21 (Local confluence).** *The rewrite system (par $\cup$ gra) is locally confluent: if $\beta_m \leftarrow \alpha_m \rightarrow \beta'_m$ then there exists $\gamma_m$ such that $\beta_m \rightarrow^* \gamma_m \leftarrow^* \beta'_m$.*

*Proof.* The source of each rewrite rule must be a stack of two bipoles. Thus all critical pairs (where the source of two rewrite rules overlap) can be found by considering stacks of two or three bipoles. Let us first enumerate all such stack shapes to determine which may contain critical pairs.
**Enumerating all possible critical pairs.** We exploit a symmetry that permutes *L* and *R* rules to reduce the number of cases: for example, the reduction behavior of *L* *R* stacks is symmetric to the behavior of *R* *L* stacks.

Let us consider all stacks of two bipoles. They have one of the following shapes:

(1) *L* *L*: no reduction.

(2) *L* *R*: *a par*<sub>*R*</sub><sup>*L*</sup> *rule may be applied*.

(3) *L* *L* *R*: no reduction.

(4) *R* *L*: symmetric to (2).

(5) *R* *R*: symmetric to (1), no reduction.

(6) *R* *L* *R*: symmetric to (3), no reduction.

(7) *L* *R* *L*: *a gra*<sub>*L*</sub><sup>*L*</sup> *rule may be applied*.

(8) *L* *R* *R*: symmetric to (7).

(9) *L* *R* *L* *R*: no reduction.

We next enumerate the stacks of three bipoles. Notice that if a 2-bipole stack has no reduction, then a 3-bipole stack formed by extending the 2-stack with a new bipole above or below cannot form a new critical pair not already in the above enumeration. For example, there is no reduction from *L* *L*, so extending it into *L* *L* *R* (or *L* *L* *L* *R*, or *R* *L* *L* for example) does not produce critical pairs involving all three bipoles. Any critical pair in an extension is a critical pair of 2-bipole stacks, which we have already considered.

In other words, we only need to consider extensions of the reducible 2-bipole stacks, modulo symmetry, to wit (2) *L* *R* and (7) *L* *R* *L* above:

(2.a) *L* *R* *L*: *two overlapping par rules may be applied*.

(2.b) *L* *R* *R*: extension of no-reduction (5).

(2.c) *L* *R* *L* *R*: extension of no-reduction (6).

(2.d) *L* *L* *R*: extension of no-reduction (1).

(2.e) *R* *L* *R*: symmetric to (2.a).

(2.f) *L* *R* *L* *R*: *a gra*<sub>*L*</sub><sup>*L*</sup> *rule may be applied above, and a par*<sub>*R*</sub><sup>*L*</sup> *below*.

(7.a) *L* *R* *L* *L*: extension of no-reduction (1).

(7.b) *L* *R* *L* *R*: same as (2.f).

(7.c) *L* *R* *L* *L* *R*: extension of no-reduction (3).

(7.d) *L* *L* *R* *L*: extension of no-reduction (3).

(7.e) *R* *L* *R* *L*: extension of no-reduction (6).

(7.f) *L* *R* *L* *R* *L*: extension of no-reduction (9).

**Resolving the critical pairs.** We now consider each of the above cases in turn.

(2) [*L* *R*] Two reductions from stacks of this shape must be two applications of the rule *par*<sub>*R*</sub><sup>*L*</sup>, which is deterministic under the FP condition, so the two right-hand-sides are equal.

(7) [*L* *R* *L*] As above, the critical pair is trivially resolved because *gra*<sub>*L*</sub> is deterministic, under no assumptions.
(2.a) [LR L] This is exactly the critical pair (3.6) that we resolved by introducing the gravity rules, in this case gra<sub>L</sub>:

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

(2.f) [LR L R] This critical pair between par<sub>R</sub><sup>L</sup> and gra<sub>L</sub> is resolved by composing the latter with gra<sub>R</sub> followed by par<sub>R</sub><sup>L</sup>:
<figure><img src="image_78.png" /></figure>

<figure><img src="image_79.png" /></figure>
APPENDIX B. CUT ON MULTI-FOCUSED DERIVATIONS, DIRECTLY

In Section 3.4.5 we defined horizontal composition of strongly multifocused proofs, and this definition is modulo permutation equivalence. We can also give a second, more syntactic definition of cut, directly on strongly multifocused derivations, and show that it coincides (modulo permutation equivalence) with the first definition.

Let us first define the operations $(\pi_N : \alpha_m)$, $(\alpha_m : \bar{\rho}_P)$, which are equivalent to compositions $\pi_N \cdot \alpha_m$, $\alpha_m \cdot \bar{\rho}_P$ but can be defined by a simple case analysis—we use a colon to emphasize that this is a more primitive operation:

$$ \begin{align*} (- : \bar{\rho}_P) &::= (S \implies_f \rho^- P) \to (S \implies_{f\rho} P) \\ (\beta_f / \bar{\rho}) : \bar{\rho}_P &::= \beta \\ (\pi \setminus \beta / \bar{\rho}) : \bar{\rho}_P &::= \pi \setminus_{f\rho} \beta \end{align*} $$

$$ \begin{align*} (\pi_N : -) &::= (\pi^+ N \implies_f T) \to (N \implies_{\pi f} T) \\ \pi_N : (\pi \setminus_f \beta) &::= \beta \\ \pi_N : (\pi \setminus \beta / \bar{\rho}) &::= \beta_{\pi f} / \bar{\rho} \end{align*} $$

In the case of $(\alpha_m : \bar{\rho}_P)$ for example, the definition is by case analysis, but we know by inspection of the judgment that a strongly multifocused derivation of $\alpha_m : S \implies_f \rho^- P$ can only start with an inversion or bi-inversion rule.

We can now define the general cut of two strongly multifocused formulas, from $S \implies_f U$ and $U \implies_f T$ to $S \implies_{fg} T$. The definition is first by case analysis on $S$ and $T$, with a single case if $S$ is positive or $T$ is negative, and then when $S \implies_{fg} T$ is a neutral judgment $N \implies_{fg} P$ we reason by case analysis on $\alpha_m$ and $\beta_m$.

$$ \begin{align*} (- \cdot -) &::= (\pi^+ N \implies_f U) \times (U \implies_g \rho^- P) \to (\pi^+ N \implies_{fg} \rho^- P) \\ \alpha_m \cdot \beta_m &::= \pi \setminus_{fg} ((\pi_N : \alpha_m) \cdot (\beta_m : \bar{\rho}_P)) / \bar{\rho} \end{align*} $$

$$ \begin{align*} (- \cdot -) &::= (N \implies_f U) \times (U \implies_g P) \to (N \implies_{fg} P) \\ (\bar{\sigma} \cdot \alpha'_m) \cdot (\beta'_m \cdot \tau) &::= \bar{\sigma} \cdot (\alpha'_m \cdot \beta'_m) \cdot \tau \\ (\bar{\sigma} \cdot \alpha'_m) \cdot \beta_m &::= \bar{\sigma} \cdot (\alpha'_m \cdot \beta_m) \\ \alpha_m \cdot (\beta'_m \cdot \tau) &::= (\alpha_m \cdot \beta'_m) \cdot \tau \end{align*} $$

$$ \begin{align*} (\alpha'_m \cdot \pi) \cdot (\pi \setminus_g \beta'_m) &::= \alpha'_m \cdot \beta'_m \\ (\bar{\sigma} \cdot \alpha'_m \cdot \pi) \cdot (\pi \setminus_g \beta'_m) &::= (\bar{\sigma} \cdot \alpha'_m) \cdot \beta'_m \end{align*} $$

$$ \begin{align*} (\alpha'_m f / \bar{\rho}) \cdot (\bar{\rho} \cdot \beta'_m) &::= \alpha'_m \cdot \beta'_m \\ (\alpha'_m f / \bar{\rho}) \cdot (\bar{\rho} \cdot \beta'_m \cdot \tau) &::= \alpha'_m \cdot (\beta'_m \cdot \tau) \end{align*} $$

$$ \delta \cdot \epsilon \qquad::= \delta \epsilon $$

For example, if $\alpha_m$ starts with a left-focusing rule, we propagate the left-focusing rule in the output and recursively compute a cut at a strictly simpler judgment. If $\alpha_m$ is a right-focusing or bi-focusing rule, then necessarily $\beta_m$ starts with a matching invertible rule (thanks to strong focusing) and we have a principal cut. If $\alpha_m$ starts with a left-inversion or bi-inversion rule, then its source formula $S$ is positive and we are in the first case of a
non-neutral judgment. Finally, if $\alpha_m$ starts with a right-inversion rule, then necessarily $\beta_m$ uses a focusing rule.

**Proposition B.1.** The explicit/intensional definition of $\alpha_m \cdot \beta_m$ above agrees with the extensional definition we gave earlier modulo ($\sim_{\text{seq}}$) as $S(\text{Seq}(\alpha_m) \cdot \text{Seq}(\beta_m))$.

*Proof.* For each equation that defines $\alpha_m \cdot \beta_m$, we check that there is a choice of sequentialization of $\alpha_m, \beta_m$ that gives the expected result.

For example, in the non-neutral case, $\alpha_m : \pi^+ N \implies_f U$ must be of the form $\pi \setminus_f \alpha'_m$ or $\pi \setminus \alpha'_m / \bar{\tau}$. If we have the latter form, we choose to sequentialize it into $\pi \setminus_f (\alpha'_{\pi f} / \bar{\tau})$, so that both cases can be sequentialized into a term of the form $\pi \setminus_f \alpha'_w$, where $\alpha'_w$ is a sequentialization of $\pi_N : \alpha_m$. By the same reasoning $\beta_m$ is sequentialized into a term of the form $\beta'_w g / \bar{\rho}$, with $\beta'_w$ a sequentialization of $\beta_m : \bar{\rho}_P$. Their composition as weakly focused proofs is $(\pi \setminus_f \alpha'_w) \cdot (\beta'_w g / \bar{\rho})$, which is equal to either of the two permutation-equivalent proofs $\pi \setminus_{fg} ((\alpha'_w \cdot \beta'_w)_{\pi fg} / \bar{\rho})$ or $(\pi \setminus_{fg} (\alpha'_w \cdot \beta'_w))_{fg} / \bar{\rho}$. Both choices strengthen into $\pi \setminus_S (\alpha'_w \cdot \beta'_w) / \bar{\rho}$, which by induction hypothesis is $\pi \setminus (\pi_N : \alpha_m) \cdot (\beta_m : \bar{\rho}_P) / \bar{\rho}$ as desired.

In a representative neutral case, $(\bar{\sigma} \cdot \alpha'_m \cdot \pi) \cdot (\pi \setminus_g \beta'_m)$, $\alpha'_m$ starts with a bi-inversion rule, let us assume that it is of the form $\tau \setminus \alpha''_m / \bar{\rho}$. We sequentialize $\alpha_m$ into

$$((\bar{\sigma} \cdot (\tau \setminus_{h\rho} \alpha''_w))_{\sigma h} / \bar{\rho}) \cdot \pi$$

where $\alpha''_w$ is a sequentialization of $\alpha''_m$, and we have

$$((\bar{\sigma} \cdot (\tau \setminus_{h\rho} \alpha''_w))_{\sigma h} / \bar{\rho}) \cdot \pi) \cdot (\pi \setminus_h \beta'_w) \\
= ((\bar{\sigma} \cdot (\tau \setminus_{h\rho} \alpha''_w))_{\sigma h} / \bar{\rho}) \cdot \beta'_w \\
\sim (\bar{\sigma} \cdot ((\tau \setminus_{h\rho} \alpha''_w)_{h/\bar{\rho}}) \cdot \beta'_w \\
\sim \bar{\sigma} \cdot (((\tau \setminus_{h\rho} \alpha''_w)_{h/\bar{\rho}}) \cdot \beta'_w)$$

where $((\tau \setminus_{h\rho} \alpha''_w)_{h/\bar{\rho}})$ is a valid sequentialization of $\alpha'_m$, and so this is permutation equivalent to a sequentialization of $\bar{\sigma} \cdot (\alpha_m \cdot \beta'_m)$ as desired. $\square$
CONTENTS

<table><tr><td>Introduction</td><td>1</td></tr><tr><td>1. Sequent calculus</td><td>8</td></tr><tr><td>1.1. Formulas and unary sequents</td><td>8</td></tr><tr><td>1.2. Inference rules and derivations</td><td>9</td></tr><tr><td>1.3. A term syntax for proofs</td><td>11</td></tr><tr><td>1.4. Interpreting formulas and proofs in any bifibration on p</td><td>12</td></tr><tr><td>1.5. Permutation equivalence</td><td>12</td></tr><tr><td>1.6. Cut</td><td>15</td></tr><tr><td>1.7. The free bifibration</td><td>18</td></tr><tr><td>1.8. Some proof-theoretic consequences</td><td>21</td></tr><tr><td>1.9. Related work</td><td>23</td></tr><tr><td>2. The double category of zigzags</td><td>24</td></tr><tr><td>2.1. Deriving a double category structure from a right action</td><td>24</td></tr><tr><td>2.2. From inference rules to double cells</td><td>26</td></tr><tr><td>2.3. Aside: displayed bifibrations</td><td>28</td></tr><tr><td>2.4. A dagger structure on zigzags</td><td>30</td></tr><tr><td>2.5. Recovering the free adjoint construction</td><td>31</td></tr><tr><td>2.6. From double cells to string diagrams</td><td>33</td></tr><tr><td>2.7. Related work</td><td>34</td></tr><tr><td>3. Focused normal forms</td><td>35</td></tr><tr><td>3.1. Background: invertibility, polarity, and synthetic connectives</td><td>35</td></tr><tr><td>3.2. Invertibility and polarity in the bifibrational calculus</td><td>37</td></tr><tr><td>3.3. Strictly alternating formulas, splittings, and weak focusing</td><td>38</td></tr><tr><td>3.4. Multifocusing</td><td>45</td></tr><tr><td>3.5. Normal forms via rewriting</td><td>50</td></tr><tr><td>3.6. Maximal multifocusing</td><td>54</td></tr><tr><td>3.7. Decidability and enumeration</td><td>57</td></tr><tr><td>4. Free (P, N)-fibrations</td><td>61</td></tr><tr><td>5. The combinatorics of free bifibrations and ambifibrations</td><td>63</td></tr><tr><td>5.1. Reconstructing the simplex category</td><td>64</td></tr><tr><td>5.2. Categories of trees and walks</td><td>65</td></tr><tr><td>5.3. A free ambifibration over Δ</td><td>75</td></tr><tr><td>6. Conclusion and future directions</td><td>81</td></tr><tr><td>Acknowledgments</td><td>82</td></tr><tr><td>References</td><td>82</td></tr><tr><td>Appendix A. Some more detailed proofs</td><td>85</td></tr><tr><td>A.1. Section 1</td><td>85</td></tr><tr><td>A.2. Section 3</td><td>88</td></tr><tr><td>Appendix B. Cut on multi-focused derivations, directly</td><td>93</td></tr></table>