# The free bifibration on a functor

Bryce Clarke, Gabriel Scherer, Noam Zeilberger

► To cite this version:

Bryce Clarke, Gabriel Scherer, Noam Zeilberger. The free bifibration on a functor. 2025. hal-05357986v2

HAL Id: hal-05357986

https://inria.hal.science/hal-05357986v2

Preprint submitted on 27 Dec 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# THE FREE BIFIBRATION ON A FUNCTOR

BRYCE CLARKE $^{a}$, GABRIEL SCHERER $^{b}$, AND NOAM ZEILBERGER $^{c}$

<sup>a</sup> Tallinn University of Technology, Tallinn, Estonia
*e-mail address:* bryce.clarke@taltech.ee

<sup>b</sup> Inria, IRIF, Université Paris Cité, Paris, France
*e-mail address*: gabriel.scherer@inria.fr

<sup>c</sup> LIX, CNRS, Inria, École Polytechnique, Institut Polytechnique de Paris, Palaiseau, France
*e-mail address*: noam.zeilberger@polytechnique.edu

ABSTRACT. We consider the problem of constructing the free bifibration generated by a functor of categories $p : \mathcal{D} \to \mathcal{C}$. This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Paré, and Pronk, of "freely adjoining adjoints" to a category. We develop a proof-theoretic approach to the problem, beginning with a construction of the free bifibration $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ in which objects of $\mathcal{Bif}(p)$ are formulas of a primitive "bifibrational logic", and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence. We show that instantiating the construction to the identity functor generates a *zigzag double category* $\mathcal{Z}(\mathcal{C})$, which is also the free double category with companions and conjoints (or fibrant double category) on $\mathcal{C}$. The approach adapts smoothly to the more general task of building $(\mathcal{P}, \mathcal{N})$-fibrations, where one only asks for pushforwards along arrows in $\mathcal{P}$ and pullbacks along arrows in $\mathcal{N}$ for some subsets of arrows, which encompasses Kock and Joyal's notion of *ambifibration* when $(\mathcal{P}, \mathcal{N})$ form a factorization system. We establish a series of progressively stronger normal forms, guided by ideas of *focusing* from proof theory, and obtain a canonicity result under assumption that the base category is factorization preordered relative to $\mathcal{P}$ and $\mathcal{N}$. This canonicity result allows us to decide the word problem and to enumerate relative homsets without duplicates. Finally, we describe several examples of a combinatorial nature, including a category of plane trees generated as a free bifibration over $\omega$, and a category of increasing forests generated as a free ambifibration over $\Delta$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition.

INTRODUCTION

A functor $p : \mathcal{D} \to \mathcal{C}$ between two categories is a *bifibration* when, roughly speaking, objects of $\mathcal{D}$ may be pushed and pulled along arrows of $\mathcal{C}$. If we visualize the category $\mathcal{D}$ as living over the category $\mathcal{C}$ and mapping downwards via the functor, then the structure of a bifibration on $p$ allows the arrows of $\mathcal{C}$ to be lifted upwards into the category $\mathcal{D}$, in two different kinds

Key words and phrases: bifibrations, double categories, free constructions, proof theory, combinatorics.
of ways. Formally, for any arrow $f: A \to B$ in $\mathcal{C}$ and any object $S$ in $\mathcal{D}$ such that $p(S) = A$, there should be an object $f^+ S$ and an arrow $f_S: S \to f^+ S$ of $\mathcal{D}$ such that $p(f_S) = f$,

$$ \begin{array}{ccc} \mathcal{D} & \xrightarrow{f_S} & \mathbf{f}^{+} \mathbf{S} \\ \xrightarrow{p} & & \\ \mathcal{C} & \xrightarrow{f} & B \end{array} $$

which are universal in the sense that for any arrow $g: B \to C$ in $\mathcal{C}$ and arrow $\alpha: S \to T$ in $\mathcal{D}$ such that $p(\alpha) = fg,^1$ there is a unique arrow $\beta: f^+ S \to T$ such that $\alpha = f_S \beta$.

$$ \begin{array}{ccc} S \xrightarrow{\alpha} T & = & S \xrightarrow{f_S} f^+ S \xrightarrow{\beta} T \\ A \xrightarrow{f} B \xrightarrow{g} C & & A \xrightarrow{f} B \xrightarrow{g} C \end{array} \qquad (0.1) $$

We refer to the object $f^+ S$ as the pushforward of $S$ along $f$, and to the arrow $f_S: S \to f^+ S$ as a $+-$cartesian lifting of $f$ to $S$. Note that the universal property of $+-$cartesian liftings ensures that the pushforward $f^+ S$ is determined up to unique isomorphism lying over the identity arrow $\mathrm{id}_B$, which is what justifies speaking of “the” pushforward of $S$ along $f$. Dually, for any arrow $g: B \to C$ in $\mathcal{C}$ and object $T$ in $\mathcal{D}$ such that $p(T) = C$, there should be an object $g^- T$ and an arrow $\bar{g}_T: g^- T \to T$ of $\mathcal{D}$ such that $p(\bar{g}_T) = g$,

$$ \bar{g}^- T \xrightarrow{\bar{g}_T} T $$

$$ B \xrightarrow{g} C $$

again universal in the sense that for any arrow $f: A \to B$ in $\mathcal{C}$ and arrow $\alpha: S \to T$ in $\mathcal{D}$ such that $p(\alpha) = fg$, there is a unique arrow $\beta: S \to g^- T$ such that $\alpha = \beta \bar{g}_T$.

$$ \begin{array}{ccc} S \xrightarrow{\alpha} T & = & S \xrightarrow{\beta} g^- T \xrightarrow{\bar{g}_T} T \\ A \xrightarrow{f} B \xrightarrow{g} C & & A \xrightarrow{f} B \xrightarrow{g} C \end{array} \qquad (0.2) $$

We refer to the object $g^- T$ as the pullback of $T$ along $g$, and to the arrow $\bar{g}_T: g^- T \to T$ as a $-+$cartesian lifting of $g$ to $T$. Again, the universal property of $-+$cartesian liftings ensures that the pullback $g^- T$ is determined up to unique isomorphism lying over $\mathrm{id}_B$.

An immediate consequence of the definitions is that if $p: \mathcal{D} \to \mathcal{C}$ is a bifibration then there is a one-to-one correspondence

$$ \begin{array}{ccc} S \longrightarrow f^{-} T & \Longleftrightarrow & S \longrightarrow T \\ A \stackrel{\mathrm{id}_A}{\longrightarrow} A & & A \stackrel{f}{\longrightarrow} B & B \stackrel{\mathrm{id}_B}{\longrightarrow} B \end{array} \qquad (0.3) $$

<footnote n="1">¹Here and throughout the paper we notate composition of arrows by juxtaposition in diagrammatic order, except in a few places where we explicitly write the composition symbol ◦ to mean $g \circ f = fg$.</footnote>
of arrows in $\mathcal{D}$ living over the corresponding arrows in $\mathcal{C}$. As a consequence, every arrow $f: A \to B$ of $\mathcal{C}$ induces an adjunction

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

realized by the operations of pushing and pulling along $f$, where $\mathcal{D}_A$ and $\mathcal{D}_B$ are the *fiber categories* of $A$ and $B$ relative to the functor $p$, defined as the subcategories of $\mathcal{D}$ spanned by the arrows living over the identities $\mathrm{id}_A$ and $\mathrm{id}_B$ in $\mathcal{C}$. More precisely, the functors $f^+$ and $f^-$ can be defined given any specific choice of cartesian liftings in $\mathcal{D}$, corresponding to a choice of bifibrational structure on $p: \mathcal{D} \to \mathcal{C}$. Such a bifibrational structure is called a “cleavage” or “cleaving”, and $p$ is said to be a *cloven* bifibration. We will always be working with bifibrational structures in this paper and so we usually omit the adjective “cloven”.

The categorical notion of bifibration was originally introduced by Grothendieck [20, VI], together with *fibration* and *cofibration*, the latter nowadays more commonly called *opfibration*. A functor $p: \mathcal{D} \to \mathcal{C}$ is a fibration (respectively opfibration) when one can pull (respectively, push) objects of $\mathcal{D}$ along arrows of $\mathcal{C}$, so that $p$ is a bifibration iff it is both a fibration and an opfibration. As established by Grothendieck and which motivated the original definition, the data of a cloven bifibration $p: \mathcal{D} \to \mathcal{C}$ is equivalent to the data of a pseudofunctor $F: \mathcal{C} \to \mathrm{Adj}$ into the 2-category of small categories and adjunctions. A bifibration over $\mathcal{C}$ is recovered from $F$ by defining the *category of elements* $\int_{\mathcal{C}} F$ (also called the *Grothendieck construction*) to have objects given by pairs $(A, S)$ of an object $A \in \mathcal{C}$ and an object $S \in F(A)$, and arrows $(A, S) \to (B, T)$ given by pairs $(f, \alpha)$ of an arrow $A \to B \in \mathcal{C}$ and an arrow $\alpha: F(f)^{+}(S) \to T \in F(B)$ or equivalently an arrow $\alpha: S \to F(f)^{-}(T) \in F(A)$, where we write $F(f)^{+}: F(A) \to F(B)$ and $F(f)^{-}: F(B) \to F(A)$ respectively for the left and right adjoint associated to the adjunction $F(f)$. The category of elements is equipped with an evident projection functor $\pi_F: \int_{\mathcal{C}} F \to \mathcal{C}$, which is a fibration.

We are interested in the problem of constructing the free bifibration on a functor, meaning the following. Let $p: \mathcal{D} \to \mathcal{C}$ be an arbitrary functor. The *free bifibration on p* is a category $\mathcal{Bif}(p)$ equipped with a functor $\Lambda_p: \mathcal{Bif}(p) \to \mathcal{C}$ that is a fibration, together with a functor $\eta_p: \mathcal{D} \to \mathcal{Bif}(p)$ commuting with the projections to $\mathcal{C}$:

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

Moreover, this data is universal in the sense that for any other bifibration $q: \mathcal{E} \to \mathcal{C}$ equipped with a functor $\theta: \mathcal{D} \to \mathcal{E}$ such that $q \circ \theta = p$, there is a unique morphism of bifibrations making the diagram below commute:

<figure><img src="image_4.png" /></figure>
By *morphism of bifibrations*, we mean a functor $[[−]]_θ : \mathcal{Bif}(p) \to \mathcal{E}$ sending chosen $±$-cartesian liftings to chosen $±$-cartesian liftings. A standard argument implies the universal property of $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ extends to bifibrations over any base category into which $\mathcal{C}$ can be mapped, in the sense that $[[−]]_θ$ below is uniquely determined from $θ : \mathcal{D} \to \mathcal{E}$, $q : \mathcal{E} \to \mathcal{B}$, and $δ : \mathcal{C} \to \mathcal{B}$:

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

In particular, (0.5) can be reduced to (0.4) by first pulling back $q$ along $δ$ to a bifibration over $\mathcal{C}$, using the fact that bifibrations are closed under pullback along arbitrary functors.

Whereas the free fibration $\mathcal{C} \downarrow p \to \mathcal{C}$ and the free opfibration $p \downarrow \mathcal{C} \to \mathcal{C}$ on a functor have simple and well-known descriptions, the free bifibration has been relatively little studied, and is a more complex object. As far as we are aware there is only one direct construction in the literature, in an unpublished manuscript by François Lamarche [32]. This construction was motivated by his work on a model of type theory in which dependent types were Grothendieck bifibrations [33], and identity types were modelled as bifibrations $P(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$ from a certain “path category”, of which a detailed analysis was given in the manuscript [32]. Otherwise, the problem of building the free bifibration on a functor is also closely related to the problem studied by Dawson, Paré, and Pronk [14, 15] of freely adjoining right adjoints to a category, which may be seen as a weaker version of building the free groupoid over a category. Their construction, which generalizes Schanuel and Street’s definition of the *free adjunction* [48], takes a category $\mathcal{C}$ and embeds it into a 2-category $\Pi_2(\mathcal{C})$ in which every arrow of the original category is equipped with a right adjoint.

The connection between these problems is revealed by taking the free bifibration on the identity functor $\mathrm{id}_\mathcal{C}$: as we will see, this defines a category $\mathcal{Z}(\mathcal{C}) := \mathcal{Bif}(\mathrm{id}_\mathcal{C})$ bifibered over $\mathcal{C}$ that may be equipped with the structure of a double category $\mathcal{Z}(\mathcal{C}) := \mathcal{Z}(\mathcal{C}) \twoheadrightarrow \mathcal{C}$. We call $\mathcal{Z}(\mathcal{C})$ the *zigzag double category of* $\mathcal{C}$, since its vertical arrows (corresponding to the objects of $\mathcal{Z}(\mathcal{C})$) are zigzags of arrows in $\mathcal{C}$. In fact, $\mathcal{Z}(\mathcal{C})$ is equivalent to Lamarche’s path category $P(\mathcal{C})$, and as he observed [32, p.22], any free bifibration may be recovered from this double category by the formula $\Lambda_p \equiv \mathrm{tgt}^+ \mathrm{src}^- p$, or diagrammatically:

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

In turn, taking the underlying vertical 2-category of $\mathcal{Z}(\mathcal{C})$ recovers a 2-category equivalent to Dawson, Paré, and Pronk’s $\Pi_2(\mathcal{C})$, thus reducing the problem of freely adjoining right adjoints to the problem of understanding the free bifibration on the identity functor.

Our approach to the problem differs from prior work in that we study it from a proof-theoretic perspective. It is natural to interpret the pushforward $f^+$ and pullback $g^-$ operations
as unary logical connectives, abstractions of existential and universal quantification as well as of diamond and box modalities. The rules of this primitive “bifibrational logic” may be presented by a simple sequent calculus, leading us to a description of the free bifibration wherein the objects of $\mathcal{Bif}(p)$ are formulas and its arrows are equivalence classes of sequent calculus derivations. See Figure 1 for an example derivation in this sequent calculus parameterized by a specific functor $p : \mathcal{D} \to \mathcal{C}$, representing an arrow $\beta : f^- f^+ X \to h^- g^+ Y$ in $\mathcal{Bif}(p)$ such that $\Lambda_p(\beta) = \mathrm{id}_A$. The close connection with the zigzag double category also leads to an isomorphic representation of derivations as stacks of double cells in $\mathbb{Z}(\mathcal{C})$, as well as to a string diagram calculus.

It should be emphasized that we do not postulate the Beck-Chevalley condition. Although bifibrations satisfying the BC condition are commonly used in categorical logic after Lawvere [36] to model extensions of predicate logic with either substitution and existential quantification or substitution and universal quantification (see, e.g., Jacobs [24]), we are rather interested in free bifibrations where the BC condition fails. These model more general situations including ones where the adjoint pair of pushforward and pullback operations $f^+ \dashv f^-$ themselves represent generalized existential and universal quantifiers $\exists_f := f^+$, $\forall_f := f^-$, and hence by alternating these operations one can in some sense define objects of arbitrary quantifier complexity.

<figure><img src="image_7.png" /><figcaption>Figure 1: Upper left: an example functor, depicting objects and arrows of the category above over their images below. Lower left: a sequent calculus proof representing an arrow of $\mathcal{Bif}(p)$. Right: the same proof depicted as a stack of double cells in $\mathbb{Z}(\mathcal{C})$ acting on an arrow in $\mathcal{D}$, overlaid with the corresponding string diagram.</figcaption></figure>
One of our original motivations for studying this problem from this perspective was the observation, made independently by Melliès and Zeilberger [40, 41, 42] and by Licata, Shulman, and Riley [37], that substructural and modal logics may be naturally modelled in certain bifibrations: specifically bifibrations of monoidal closed categories or multicategories in which the base moreover contains an object with some algebraic structure. As a typical example, any monoid $(A, m, e)$ in the base of a bifibration of multicategories $p : \mathcal{E} \to \mathcal{B}$ generates a monoidal closed fiber category $\mathcal{E}_A$, with the tensor product and internal hom defined by pushing and pulling along the multiplication map $m : A, A \to A$. For more recent work in this spirit see Nicolas Blanco's PhD thesis [8] developing the theory of bifibrations of polycategories as models of classical linear logic, as well as Shulman [50] on LNL doctrines, which axiomatize a wide variety of categorical structures and type theories. The problem of constructing free bifibrations may therefore be seen as a natural problem in proof theory (cf. [50, §8]), and we were motivated to study the “pure” version of the problem for functors of categories as an eventual stepping stone to the more sophisticated case of monoidal closed categories or generalized multicategories and polycategories. In the present paper we do already consider a simple but practically significant generalization of the problem, namely to free $(\mathcal{P}, \mathcal{N})$-fibrations where one only asks for `+cartesian liftings` (resp. `--cartesian liftings`) of the arrows in $\mathcal{P}$ (resp. $\mathcal{N}$). In particular when the pair $(\mathcal{P}, \mathcal{N})$ form a factorization system for the base category this defines what Joachim Kock and André Joyal refer to as an *ambifibration*.

As it turns out, even very simple functors can generate free bifibrations (and free ambifibrations) with surprisingly rich combinatorial structure. For instance, let $p_2 : 1 \to 2$ be the functor from the terminal category to the interval category sending the unique object of 1 to the initial object of 2:

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

Now consider the free bifibration generated by $p_2$. It is easy to see that any object of $\mathcal{Bif}(p_2)$ must be isomorphic to an alternating sequence of pushes and pulls along the arrow $f$ starting at the point *, with even-length sequences yielding an object in the fiber over 0, and odd-length sequences an object in the fiber over 1. Let us write $n := (f^- f^+)^{n*}$ and $n' := f^+(f^- f^+)^{n*}$ for the objects in the respective fibers (e.g., $3 = f^- f^+ f^- f^+ f^- f^+ *$). From the fact that the morphisms in the fibers are generated by the unit and counit of the push-pull adjunction $f^+ \dashv f^-$, with a bit of mental exercise (or familiarity with Schanuel and Street's paper [48], building on Auderset's earlier work [4]) one can check that an arrow $m \to n$ in $\mathcal{Bif}(p_2)_0$ should correspond to an order-preserving map $\{1, \dots, m\} \to \{1, \dots, n\}$. Indeed, $\mathcal{Bif}(p_2)_0 \cong \Delta$ is equivalent to the (augmented) simplex category of finite ordinals and order-preserving maps, while $\mathcal{Bif}(p_2)_1 \cong \Delta_\perp$ is equivalent to the category of non-empty finite ordinals and order-and-least-element-preserving maps. The push-pull adjunction of the free bifibration instantiates to the free / forgetful adjunction

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

where $L$ freely adds a least element $\perp$ to turn an order-preserving map $m \to n$ into an order-and-least-element-preserving map $m' \to n'$, while the right adjoint $R$ interprets $m'$
as $1+m$ and forgets that a map is $\perp$-preserving. This much may be unshocking to readers familiar with the free adjunction $\mathcal{A}$, which can be obtained by freely adjoining adjoints to the interval category, $\mathcal{A} = \Pi_2(2)$, as Dawson, Paré, and Pronk already observed [14, p.139]—although we emphasize the free bifibration is another way of organizing the data.

More strikingly, this example generalizes in the following way. Replace the interval category 2 by the ordinal $\omega$ (that is, the total order on the natural numbers) and consider the free bifibration generated by the functor $p_{\omega}: 1 \to \omega$ mapping the point to 0, as depicted below:

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

What is the fiber of $\mathcal{Bif}(p_{\omega})$ over 0? Objects are isomorphic to sequences of pushes and pulls along $f_i$'s, such that, reading a formula from right to left, the running total of pushes never exceeds the running total of pushes, and the total numbers of pushes and pulls are equal. In other words, up to isomorphism the objects of $\mathcal{Bif}(p_{\omega})_0$ may be read as *Dyck words*. Via a well-known bijection (see Stanley [52, V2:169–170]), Dyck words are in one-to-one correspondence with rooted plane trees, and thus $\mathcal{Bif}(p_{\omega})_0$ may be interpreted as a category of trees. Under a natural encoding of plane trees as functors $T: \omega^{op} \to \Delta$, it turns out that this fiber category of the free bifibration is equivalent to a full subcategory of $[\omega^{op}, \Delta]$, and embeds as a wide subcategory into a category of finite plane trees defined by Joyal [26].

An example of a different nature is obtained by considering the free $(\Delta_{\text{epi}}, \Delta_{\text{mono}})$-fibration generated by the inclusion $i: \mathbb{N} \to \Delta$ of the set of natural numbers (seen as a discrete category) into the simplex category. This is a free ambifibration, and its universal property ensures that it is equipped with a canonical morphism into the so-called “fat Delta” category introduced by Kock [29]. The category $\mathcal{Bif}(i, \Delta_{\text{epi}}, \Delta_{\text{mono}})$ appears to have a rich combinatorial structure that we only begin to analyze here. For example, the *lattices of noncrossing partitions* (see Stanley [52, V1:515, V2:226]) are recovered by quotienting this free ambifibration by the Beck-Chevalley condition.

**Outline of the paper.** After introducing the sequent calculus in Section 1 and after defining and analyzing the double category of zigzags in Section 2, the technical core of the paper is in Section 3, where we establish a series of progressively stronger normal form results, guided by ideas from proof theory. The strongest of these (Theorem 3.23), which holds under the assumption that the base category $\mathcal{C}$ is factorization preordered (FP), leads to an inductive definition of the relative homsets of the free bifibration that does not use any kind of quotient by an equivalence relation, representing arrows by *maximally multifocused* derivations. The FP condition also showed up in Dawson, Paré, and Pronk's work on the $\Pi_2(\mathcal{C})$ construction, where they observed that equality of 2-cells is undecidable in general but is decidable when $\mathcal{C}$ is factorization preordered [15]. As a corollary of our canonicity theorem, we obtain both an analogous decidability result for equality of arrows in $\mathcal{Bif}(p)$ as well as a procedure for enumerating relative homsets without duplicates. Section 4 briefly describes how our constructions and results adapt to free $(\mathcal{P}, \mathcal{N})$-fibrations. This is technically straightforward but has the useful consequence that one can weaken the assumption needed for canonicity, only requiring that the base category be factorization preordered relative to each class $\mathcal{P}$ and $\mathcal{N}$ independently. Finally, in Section 5 we use the tools developed in the paper to analyze
the three examples described above. Section 6 concludes and suggests some directions for further exploration.

**Remark.** This work mixes domains and techniques that will be familiar to different audiences, and we expect most readers to be unfamiliar with some of them. We tried to find a presentation that would be accessible to people only familiar but not expert in category theory, and people unfamiliar with sequent calculus and proof theory. We ask the reader for forgiveness if they find the exposition too basic in places, for the small doses of redundancy this introduces, and for the length of the resulting presentation.

# 1. SEQUENT CALCULUS

In this section we will explain how the free bifibration $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ on an arbitrary functor $p : \mathcal{D} \to \mathcal{C}$ may be constructed proof-theoretically, as an inductively-defined sequent calculus for a primitive “bifibrational logic”, starting from the data of $p$. The idea will be to take the objects of $\mathcal{Bif}(p)$ to be formulas of the sequent calculus and its arrows to be proofs modulo a notion of *permutation equivalence* to be defined below. This sequent calculus is cut-free, but the cut rule is admissible, giving a definition of composition of arrows in the category $\mathcal{Bif}(p)$. We will establish a series of properties leading to the main result of this section (Theorem 1.17), that the sequent calculus indeed gives a presentation of the free bifibration on $p$.

## 1.1. Formulas and unary sequents.
To define the formulas of the logic, we find it helpful to introduce the judgment $S \sqsubseteq A$ to mean that $S$ is a formula (= object of $\mathcal{Bif}(p)$) lying over (or “refining”) the object $A$ of $\mathcal{C}$. We usually refer to formulas simply as “formulas”, but sometimes for clarity we refer to them as *bifibrational formulas*, being formulas of bifibrational logic. Bifibrational formulas are defined inductively by the following rules:

$$ \frac{X \in \mathcal{D} \quad p(X) = A}{X \sqsubseteq A} \qquad \frac{S \sqsubseteq A \quad f : A \to B}{f^+ S \sqsubseteq B} \qquad \frac{g : B \to C \quad T \sqsubseteq C}{g^- T \sqsubseteq B} $$

Here we are using standard notation for inference rules: the judgment below the horizontal bar is the *conclusion* of the inference rule, and the judgments above the bar are its *premises*. Each rule asserts that if its premises are valid, then its conclusion is valid. We refer to formulas of the form $X$ as *atomic formulas*, and formulas of the form $f^+ S$ or $g^- T$ as *push formulas* and *pull formulas* respectively. All of the formulas $S'$ appearing in the inductive construction of a bifibrational formula $S$ are said to be *subformulas* of $S$. We denote the subformula relation $S' \leq S$, and the strict subformula relation $S' < S$.

In set-theoretic terms, each object $A$ of $\mathcal{C}$ determines a set $\text{Frm}_A = \{S \mid S \sqsubseteq A\}$ of formulas lying over $A$, and the collection of sets of formulas $(\text{Frm}_A)_{A \in \mathcal{C}}$ is the least family of sets closed under the following three conditions:

* if $X \in \mathcal{D}$ and $p(X) = A$ then $X \in \text{Frm}_A$;

* if $S \in \text{Frm}_A$ and $f : A \to B$ is an arrow of $\mathcal{C}$ then $f^+ S \in \text{Frm}_B$;

* if $T \in \text{Frm}_C$ and $g : B \to C$ is an arrow of $\mathcal{C}$ then $g^- T \in \text{Frm}_B$.

Besides the judgment $S \sqsubseteq A$ describing well-formedness of formulas, the main judgment of interest of the calculus is the *unary sequent arrow* of the form

$$ S \underset{h}{\implies} T \qquad (1.1) $$
where $S \sqsubseteq A$ and $T \sqsubseteq C$ are formulas lying over objects $A$ and $C$ respectively, and where $h: A \to C$ is an arrow of $\mathcal{C}$. For comparison, it is worth keeping in mind traditional sequents of intuitionistic sequent calculus, which take the form

$$P_1, \dots, P_n \implies Q$$

(often written with $\vdash$ in place of an arrow) and which may be read as asserting an entailment from the conjunction of the formulas on the left-hand side to the formula on the right-hand side. In the bifibrational calculus, unary sequents of the form (1.1) may be read as asserting an entailment from $S$ to $T$ “fibered over $h$”. We refer to $S$ as the *left side*, to $T$ as the *right side*, and to $h$ as the *base* of the sequent. The definition of the sequent calculus will ensure that a proof of the judgment $S \implies_h T$ corresponds to an arrow $\alpha: S \to T$ in $\mathcal{Bif}(p)$ such that $\Lambda_p(\alpha) = h$.

## 1.2. Inference rules and derivations.
The calculus includes four logical inference rules:

$$ \begin{array}{ccc} \frac{S \underset{fg}{\implies} T}{f^+ S \underset{g}{\implies} T} & \Leftrightarrow & Lf^+ \\ \frac{S' \underset{f'}{\implies} S}{S' \underset{f'f}{\implies} f^+ S} & \Leftrightarrow & Rf^+ \\ \frac{T \underset{g'}{\implies} T'}{g^- T \underset{gg'}{\implies} T'} & \Leftrightarrow & Lg^- \\ \frac{S \underset{fg}{\implies} T}{S \underset{f}{\implies} g^- T} & \Leftrightarrow & Rg^- \end{array} $$

together with an *initial axiom* for every arrow of $\mathcal{D}$:

$$ \frac{\delta : X \to Y \in \mathcal{D} \quad p(\delta) = f}{X \underset{f}{\implies} Y} \delta $$

In general in sequent calculus, one can define a *derivation* to be a finite rooted tree whose edges are labelled by sequents, and whose nodes are labelled by valid instances of the inference rules. Moreover, one can distinguish between *open* and *closed* derivations, where open derivations have premises corresponding to open edges of the tree. Another name for a closed derivation is a *proof*. A special property of the bifibrational sequent calculus is that every inference rule has at most one premise, so that derivations are completely linear (i.e., they are just *lists* rather than proper trees), and a derivation is closed just in case it is terminated by a unique initial axiom.

The overall format of the rules follows the tradition of sequent calculus with left rules and right rules for every connective, which in this case are the pushforward $f^+$ and pullback $g^-$ connectives parameterized by arrows $f$ and $g$ of $\mathcal{C}$.

In set-theoretic terms, the rules may be seen as specifying closure conditions that inductively define a family of sets of proofs of judgments. For example, the $Lf^+$ rule says that for any formulas $S$ and $T$ and arrows $f$ and $g$, given a proof of $S \implies_{fg} T$ there should be a proof of $f^+ S \implies_g T$. Note that the rules have implicit side-conditions that the judgments are well-formed. For example, in the $Lf^+$ rule, the arrows $f$ and $g$ should be composable, with $f: A \to B$ and $g: B \to C$ for some objects $A, B, C$ such that $S \sqsubseteq A$ and $T \sqsubseteq C$.

We refer the reader back to Figure 1 from the Introduction, which gives an example derivation in the sequent calculus relative to a simple functor.

Finally, we emphasize that the underlying base arrows are more than a mere annotation on the sequent judgments: they really do restrict the applicability of the inference rules. For example, applying the $Lf^+$ rule to a derivation of a judgment $S \implies_h T$ requires factoring the arrow as a composite $h = fg$.
We do not include explicit identity and cut rules in the definition of the sequent calculus,

$$ \frac{S \sqsubseteq A}{S \underset{\mathrm{id}_A}{\Longrightarrow} S} \mathrm{id}_S \qquad \frac{S \underset{f}{\Longrightarrow} U \qquad U \underset{g}{\Longrightarrow} T}{S \underset{fg}{\Longrightarrow} T} \text{ cut} $$

but these rules are *admissible* in the proof-theoretic sense as we will explain below. Since derivations are cut-free, they satisfy a variation of the standard subformula property:

**Proposition 1.1** (Subformula property). *A derivation of $S \Longrightarrow_f T$ involves only sequents of the form $S' \Longrightarrow_g T'$ where $S' \leq S$ and $T' \leq T$ are subformulas of S and T.*

We now define closed derivations corresponding to the identity rule below, deferring the treatment of cut to Section 1.6.

**Definition 1.2** (identity). For any formula $S \sqsubseteq A$, there is a proof $\mathrm{id}_S$ of $S \Longrightarrow_{\mathrm{id}_A} S$ constructed by induction on $S$ as follows:

$$ \frac{X \in \mathcal{D} \qquad p(X) = A}{X \sqsubseteq A} \qquad \Rightarrow \qquad \mathrm{id}_X := \overline{X \underset{\mathrm{id}_A}{\Longrightarrow} X}^{\mathrm{id}_X} $$

$$ \frac{S \sqsubseteq A \qquad f : A \to B}{f^+ S \sqsubseteq B} \qquad \Rightarrow \qquad \mathrm{id}_{f^+ S} := \frac{\overline{S \underset{\mathrm{id}_A}{\Longrightarrow} S}^{\mathrm{id}_S} \qquad f^+ S \qquad \mathrm{R} f^+}{f^+ S \underset{\mathrm{id}_B}{\Longrightarrow} f^+ S} \qquad \mathrm{L} f^+ $$

$$ \frac{g : B \to C \qquad T \sqsubseteq C}{g^- T \sqsubseteq B} \qquad \Rightarrow \qquad \mathrm{id}_{g^- T} := \frac{\overline{T \underset{\mathrm{id}_C}{\Longrightarrow} T}^{\mathrm{id}_T} \qquad g^- T \underset{g}{\Longrightarrow} T}{g^- T \underset{\mathrm{id}_B}{\Longrightarrow} g^- T} \qquad \mathrm{R} g^- $$

□

Observe that proofs corresponding to the unit and counit of the canonical family of adjunctions $f^+ \dashv f^-$ of a bifibration may be constructed as

$$ \frac{\overline{S \underset{\mathrm{id}_A}{\Longrightarrow} S}^{\mathrm{id}_S} \qquad f^+ S \qquad \mathrm{R} f^+}{S \underset{f}{\Longrightarrow} f^+ S} \qquad \overline{f^- U \underset{\mathrm{id}_B}{\Longrightarrow} U}^{\mathrm{id}_U} \qquad \mathrm{L} f^- \\ \frac{S \underset{\mathrm{id}_A}{\Longrightarrow} f^- f^+ S}{f^- f^+ S \qquad \mathrm{R} f^-} $$

$$ \frac{\overline{U \underset{\mathrm{id}_B}{\Longrightarrow} U}^{\mathrm{id}_U} \qquad f^- U \underset{f}{\Longrightarrow} U}{f^+ f^- U \underset{\mathrm{id}_B}{\Longrightarrow} U} \qquad \mathrm{L} f^+ $$

where we make use of the identity derivations from Definition 1.2 to terminate the proofs.
$$ \frac{\delta : X \to Y \in \mathcal{D} \qquad p(\delta) = f}{\delta : X \underset{f}{\Rightarrow} Y} $$

$$ \frac{\alpha : S \underset{fg}{\Rightarrow} T}{f \backslash_g \alpha : f^+ S \underset{g}{\Rightarrow} T} $$

$$ \frac{\alpha : S' \underset{f'}{\Rightarrow} S}{\alpha.f : S' \underset{f'f}{\Rightarrow} f^+ S} $$

$$ \frac{\alpha : T \underset{g'}{\Rightarrow} T'}{\bar{g} \cdot \alpha : \bar{g}^{-} T \underset{gg'}{\Rightarrow} T'} $$

$$ \frac{\alpha : S \underset{fg}{\Rightarrow} T}{\alpha_f / \bar{g} : S \underset{f}{\Rightarrow} \bar{g}^{-} T} $$

<caption>Figure 2: Term-annotated inference rules of the bifibrational calculus.</caption>

**1.3. A term syntax for proofs.** A term syntax is a compact notation to describe derivations that can be convenient for defining some operations and equations. We introduce here a syntax of terms generated by the following grammar:

$$ \alpha ::= \begin{array}{l} \delta \quad \text{for } \delta : X \to Y \in \mathcal{D} \\ | \quad f \backslash_g \alpha \\ | \quad \alpha.f \\ | \quad \bar{g}.\alpha \\ | \quad \alpha_f / \bar{g} \end{array} $$

which are assigned to derivations as shown in Figure 2.

Formally, this defines a new judgment $\alpha : S \implies_h T$ whose derivations are in one-to-one correspondence with derivations of $S \implies_h T$. In other words, for a judgment $S \implies_h T$, a derivation of the judgment uniquely determines a term $\alpha$ and a derivation of $\alpha : S \implies_h T$. We will only consider valid terms, that do correspond to a derivation, and will use the term $\alpha$ and the underlying derivation interchangeably.

We sometimes call *multiplications* the term-formers $\alpha.f$ and $\bar{g}.\alpha$ and *divisions* the term-formers $f \backslash_g \alpha$ and $\alpha_f / \bar{g}$. The reason why our division notation takes an explicit subscript $f$ or $g$ is that its meaning depends on a choice of decomposition of the arrow $h$ underlying $\alpha$ as $h = fg$; there is no such ambiguity for multiplications.

**Examples.** The terms for the identity derivations can be defined recursively as follows:

$$ \mathrm{id}_X := \mathrm{id}_X \in \mathcal{D} \qquad \mathrm{id}_{f^+ S} := f \backslash_{\mathrm{id}_B} (\mathrm{id}_S \cdot f) \qquad \mathrm{id}_{\bar{g}^{-} T} := (\bar{g} \cdot \mathrm{id}_T) \backslash_{\mathrm{id}_B} \bar{g} $$

and the unit and co-unit derivations as follows:

$$ \eta_S := (\mathrm{id}_S \cdot f) \mathrm{id}_A / \bar{f} \qquad \epsilon_T := f \backslash_{\mathrm{id}_B} (\bar{f} \cdot \mathrm{id}_U) $$

These examples use subterms of the form $\mathrm{id}_S \cdot f$ and $\bar{f} \cdot \mathrm{id}_S$, which we will later show correspond to cartesian liftings in the free bifibration:

$$ f_S : S \underset{f}{\Rightarrow} f^+ S \quad := \quad \mathrm{id}_S \cdot f \qquad \bar{g}_T : \bar{g}^{-} T \underset{g}{\Rightarrow} T \quad := \quad \bar{g} \cdot \mathrm{id}_T $$
1.4. **Interpreting formulas and proofs in any bifibration on $p$.** In this section we suppose given an arbitrary bifibration $q: \mathcal{E} \to \mathcal{C}$ equipped with a functor $\theta: \mathcal{D} \to \mathcal{E}$ such that $q \circ \theta = p$. As explained in the Introduction, we expect $\theta$ to factor uniquely via the free bifibration in the diagram below:

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

We describe now how to interpret formulas and proofs of the sequent calculus as objects and arrows of $\mathcal{E}$, which will determine the functor $[[\cdot]]_\theta$ once we have completed the definition of the category $\mathbf{Bif}(p)$.

We interpret any formula $S$ as an object $[[S]]_\theta$ of $\mathcal{E}$, and any proof $\alpha: S \Longrightarrow_h T$ as an arrow $[[\alpha]]_\theta: [[S]]_\theta \to [[T]]_\theta$ such that $q( [[\alpha]]_\theta ) = h$.

**Interpretation of formulas.** Defined by induction on the formula:

$$[[X]]_\theta = \theta(X)$$

$$[[f^+ S]]_\theta = f^+ [[S]]_\theta$$

$$[[g^- T]]_\theta = g^- [[T]]_\theta$$

That is, we interpret the pushforward and pullback connectives using pushforward and pullback in $\mathcal{E}$, and atomic formulas using the action of the functor $\theta: \mathcal{D} \to \mathcal{E}$ on objects.

**Interpretation of terms.** By gentle abuse of notation, for any arrow $\alpha: X \to Y \in \mathcal{E}$ such that $q(\alpha) = fg$, let us write $f \backslash_g \alpha$ for the unique $\beta: f^+ X \to Y$ such that $\alpha = f_X \beta$, and $\alpha f / \bar{g}$ for the unique $\beta: X \to \bar{g}^- Y$ such that $\alpha = \beta \bar{g}_Y$, both of these derived using the respective universal properties (0.1) and (0.2) of cartesian liftings. We thus reuse the notation for division to denote arrows in an arbitrary bifibration. Let us also allow ourselves to write $f$ for $f_X$ and $\bar{g}$ for $\bar{g}_Y$, when the object can be deduced from the context.

The interpretation of terms is then defined by induction as follows:

$$[[\delta]]_\theta = \theta(\delta)$$

$$[[\alpha.f]]_\theta = [[\alpha]]_\theta f$$

$$[[f \backslash_g \alpha]]_\theta = f \backslash_g [[\alpha]]_\theta$$

$$[[\bar{g}.\alpha]]_\theta = \bar{g} [[\alpha]]_\theta$$

$$[[\alpha f / \bar{g}]]_\theta = [[\alpha]]_\theta f / \bar{g}$$

Initial axioms are interpreted using the action of $\theta$ on arrows of $\mathcal{D}$, multiplications (corresponding to the inference rules $L\bar{g}^-$ and $Rf^+$) are interpreted by pre- and post-composition with cartesian liftings in $\mathcal{E}$ (we remind the reader that we write composition by juxtaposition in diagrammatic order), and divisions ($Lf^+$ and $R\bar{g}^-$) are interpreted using division in $\mathcal{E}$, i.e., using the universal properties of the cartesian liftings.

1.5. **Permutation equivalence.** Let us begin by observing that some algebraic laws relating multiplication and division hold in any bifibration $q: \mathcal{E} \to \mathcal{B}$.
**Proposition 1.3.** For $\alpha : X \to Y \in \mathcal{E}$ such that $q(\alpha) = fg$, and $\beta : X \to Y'$ such that $q(\beta) = fgg'$, the following equalities hold:

$$ 
\begin{aligned}
\overline{f'} (\alpha_f / \overline{g}) &= (\overline{f'} \alpha) f'f / \overline{g} \\
(f \backslash_g \alpha) g' &= f \backslash_{gg'} (\alpha g') \\
(f \backslash_{gg'} \beta) g / \overline{g'} &= f \backslash_g (\beta fg / \overline{g'})
\end{aligned}
 $$

*Proof.* The uniqueness condition on the arrows obtained by division can be expressed as an equivalence: $\beta = (\alpha_f / \overline{g}) \iff \beta \overline{g} = \alpha$ and $\beta = (f \backslash_g \alpha) \iff f \beta = \alpha$. The proofs for the desired equalities are then as follows:

$$ 
\begin{array}{rcl@{\qquad}rcl}
\iff & \overline{f'} (\alpha_f / \overline{g}) = (f' \alpha) f'f / \overline{g} & \iff & (f \backslash_g \alpha) g' = f \backslash_{gg'} (\alpha g') \\
\iff & \overline{f'} (\alpha_f / \overline{g}) \overline{g} = \overline{f'} \alpha & \iff & f (f \backslash_g \alpha) g' = \alpha g' \\
\iff & (\alpha_f / \overline{g}) \overline{g} = \alpha & \iff & f (f \backslash_g \alpha) = \alpha \\
\iff & \alpha_f / \overline{g} = \alpha_f / \overline{g} & \iff & f \backslash_g \alpha = f \backslash_g \alpha \\
& & & \\
& (f \backslash_{gg'} \beta) g / \overline{g'} = f \backslash_g (\beta fg / \overline{g'}) \\
\iff & f (f \backslash_{gg'} \beta) g / \overline{g'} = \beta \overline{fg} / \overline{g'} \\
\iff & f ((f \backslash_{gg'} \beta) g / \overline{g'}) \overline{g'} = \beta \\
\iff & ((f \backslash_{gg'} \beta) g / \overline{g'}) \overline{g'} = f \backslash_{gg'} \beta \\
\iff & ((f \backslash_{gg'} \beta) g / \overline{g'}) = (f \backslash_{gg'} \beta) g / \overline{g'}
\end{array}
 $$

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

These laws imply that different derivations of the sequent calculus $\alpha_1, \alpha_2 : S \implies_h T$ will be interpreted by the same arrow $[[\alpha_1]]_\theta = [[\alpha_2]]_\theta : [[S]]_\theta \to [[T]]_\theta$ in $\mathcal{E}$ under the bifibrational interpretation described in the previous section. In order for derivations to form a bifibration themselves, we must quotient them by a *permutation equivalence relation* ($\sim$) that relates any such pair of derivations equated in all interpretations.

**Definition 1.4.** We define *permutation equivalence* ($\sim$) as the smallest congruence that contains the four generating equations below. A congruence is an equivalence relation that is also closed under the derivation term-formers: if $\alpha_1 \sim \alpha_2$, then we also have $\alpha_1.g' \sim \alpha_2.g'$, and $f \backslash_g \alpha_1 \sim f \backslash_g \alpha_2$, etc., whenever both sides of the equation are valid terms. The generating equations of ($\sim$) are (whenever both sides of the equation are valid):

$$ 
\begin{array}{l@{\qquad}l}
(\overline{f}.\alpha).h \sim \overline{f}.(\alpha.h) & \text{for } \alpha \text{ over } g \qquad (1.2) \\
(f \backslash_g \alpha).h \sim f \backslash_{gh}(\alpha.h) & \text{for } \alpha \text{ over } fg \qquad (1.3) \\
(\overline{f}.\alpha)_{fg}/\overline{h} \sim \overline{f}.(\alpha_g/\overline{h}) & \text{for } \alpha \text{ over } gh \qquad (1.4) \\
(f \backslash_{gh} \alpha)_{g/\overline{h}} \sim f \backslash_g (\alpha_{fg}/\overline{h}) & \text{for } \alpha \text{ over } fgh \qquad (1.5)
\end{array}
 $$
The generators of the permutation equivalence relation may be defined equivalently (albeit less compactly) as the following relations on derivations:

$$ \frac{S \underset{fg}{\overset{g}{\Rightarrow}} T}{f^{-} S \underset{fg}{\overset{fg}{\Rightarrow}} T} L f^{-} \sim \frac{S \underset{gh}{\overset{g}{\Rightarrow}} T}{f^{-} S \underset{gh}{\overset{gh}{\Rightarrow}} h^{+} T} R h^{+} \sim \frac{S \underset{fg}{\overset{fg}{\Rightarrow}} T}{f^{+} S \underset{gh}{\overset{g}{\Rightarrow}} T} L f^{+} \sim \frac{S \underset{fg}{\overset{fg}{\Rightarrow}} T}{f^{+} S \underset{gh}{\overset{gh}{\Rightarrow}} h^{+} T} R h^{+} $$

$$ \frac{S \underset{gh}{\overset{gh}{\Rightarrow}} T}{f^{-} S \underset{fg}{\overset{fg}{\Rightarrow}} T} L f^{-} \sim \frac{S \underset{gh}{\overset{gh}{\Rightarrow}} T}{f^{-} S \underset{fg}{\overset{fg}{\Rightarrow}} h^{-} T} R h^{-} \sim \frac{S \underset{fg}{\overset{fg}{\Rightarrow}} T}{f^{+} S \underset{gh}{\overset{gh}{\Rightarrow}} T} L f^{+} \sim \frac{S \underset{fg}{\overset{fg}{\Rightarrow}} T}{f^{+} S \underset{g}{\overset{g}{\Rightarrow}} h^{-} T} R h^{-} $$

Observe that each of the relations permutes a left rule with a right rule.

**Lemma 1.5.** *Interpretation in any bifibration respects permutation equivalence: if $\alpha_1 \sim \alpha_2$, then $[[\alpha_1]]_\theta = [[\alpha_2]]_\theta$.*

*Proof.* The equivalence and congruence rules are obviously respected by the interpretation. It suffices to check that the four generating equations are also respected. The equation with two multiplications holds by associativity of composition:

$$ [[(\bar{f}' \cdot \alpha) \cdot g']_{\theta} = \bar{f}'_{S'} \alpha g'_{T} = [[f' \cdot (\alpha \cdot g')]_{\theta}} $$

The three other equations exactly correspond to the equalities in Proposition 1.3, which hold in any bifibration. $\square$

**Remark 1.6.** The first permutation rule (1.2) is really an associativity property for left and right multiplication: a term outline $\bar{f} \cdot \alpha \cdot h$ can be read in two ways depending on the parenthesis placement, the two terms are valid (if $\alpha$ is) and are equivalent.

The second permutation rule (1.3) can be oriented from left to right: if the term $(f \backslash_g \alpha) \cdot h$ is valid, then one can “push the multiplication inside”, in the sense that the term $f \backslash_{gh} (\alpha \cdot h)$ is also valid and is equivalent. But going in the other direction, the validity of a term of the form $f \backslash_k (\alpha \cdot h)$ does not uniquely determine a corresponding term of the form $(f \backslash_l \alpha) \cdot h$. This depends on the solutions $l$ of the equation $k = lh$: it may be that no such $l$ exists, and there is no valid term of this shape, or that several $l$ exist giving different possible rewrites. For example, we saw that for any $S \subset A$ and $f: A \to B$ the identity derivation $\mathrm{id}_{f^+ S} : f^+ S \implies_{\mathrm{id} B} f^+ S$ is of the form $\mathrm{id}_{f^+ S} = f \backslash_{\mathrm{id} B} (\mathrm{id} S \cdot f)$, but there are not necessarily any derivations of the form $(f \backslash_g \mathrm{id} S) \cdot f$. Indeed, $(f \backslash_g \mathrm{id} S) \cdot f \sim \mathrm{id}_{f^+ S}$ is an instance of permutation rule (1.3) just in case $g: B \to A$ exists and is inverse to $f$.

Similarly, the third permutation rule (1.4) can be oriented from right to left: one can always “push the multiplication inside” by moving from a term of the shape $\bar{f} \cdot (\alpha / \bar{h})$ to an equivalent term of the shape $(\bar{f} \cdot \alpha) / \bar{h}$, but the other direction is not always possible or is non-deterministic.

Finally, the fourth permutation rule (1.5) is also an associativity-like property that can be read in both directions: the two terms of the form $f \backslash \alpha / \bar{h}$ are equally valid (not always valid, but in the same situations) and equivalent. For example, let us assume that a term of the form $(f \backslash \alpha) / \bar{h}$ is valid and is over some morphism $g$; then the term must be of the form $(f \backslash \alpha) g / \bar{h}$, so $f \backslash \alpha$ must be over the morphism $gh$: our original term is uniquely determined
to be $(f \backslash_{gh} \alpha)_g / \bar{h}$, and $\alpha$ must be over $fgh$. By the same reasoning, any valid term of the form $f \backslash (\alpha / \bar{h})$ over $g$ must be $f \backslash_g (\alpha_{fg} / \bar{h})$, this term is always valid (assuming that the other term is) and equivalent.

**Remark 1.7.** This situation, where multiplications can be pushed inside divisions but not necessarily outside, is reminiscent of Lambek calculus [34], which inspires our notation. Indeed, the generators of the permutation equivalence relation are analogous to the natural transformations

$$ (A \bullet B) \bullet C \xrightarrow{\sim} A \bullet (B \bullet C) \qquad A \backslash (B/C) \xrightarrow{\sim} (A \backslash B)/C \quad (1.6) $$

$$ (A \backslash B) \bullet C \longrightarrow A \backslash (B \bullet C) \qquad A \bullet (B/C) \longrightarrow (A \bullet B)/C \quad (1.7) $$

that exist in any monoidal biclosed category, where the transformations (1.6) are always invertible, but the transformations (1.7) in general are not. For example, considering the special case of cartesian closed categories, the former correspond to the natural isomorphisms $(A \times B) \times C \cong A \times (B \times C)$ and $(B^C)^A \cong (B^A)^C$, while the latter correspond to the natural transformations $B^A \times C \to (B \times C)^A$ and $A \times B^C \to (A \times B)^C$ that may be derived in any ccc, but are very rarely invertible.

**1.6. Cut.** From a logical perspective, cut is an expected rule for any logic, that ensures that sequences of reasoning can be chained as expected. The surprising insight behind Gentzen's invention of sequent calculus was that the cut rule is in a sense logically redundant. The original approach for demonstrating this was to include a cut rule directly in the inference system and then show *cut elimination*: any closed proof can be rewritten without using the cut rule. We use the alternative but nearly equivalent approach of first defining a cut-free system and then showing that the cut rule is admissible. Recall that a reasoning rule is *admissible* if, given closed derivations for its premises, there is a closed derivation for its conclusion.

**Definition 1.8.** The following cut rule is admissible

$$ \frac{\alpha : S \underset{g}{\Rightarrow} T \qquad \beta : T \underset{h}{\Rightarrow} U}{\alpha \cdot \beta : S \underset{gh}{\Rightarrow} U} $$

via a composition function $\alpha \cdot \beta$ defined up to permutation equivalence ($\sim$).

*Proof.* The cut, or horizontal composition, written $\alpha \cdot \beta$, is defined by induction in the usual style of cut-elimination arguments: we reason by case analysis on the derivations $\alpha$ and $\beta$, and we may use instances of the cut rule on strictly smaller arguments (more precisely: in each case both arguments are at least as small and one of them is strictly smaller).

Principal cuts:

$$ \frac{\displaystyle\frac{\delta : X \to Y \in \mathcal{D}}{\delta : X \underset{g}{\Rightarrow} Y} \qquad \displaystyle\frac{\epsilon : X \to Y \in \mathcal{D}}{\epsilon : Y \underset{h}{\Rightarrow} Z}}{\delta \cdot \epsilon : X \underset{gh}{\Rightarrow} Z} \qquad \Rightarrow \qquad \frac{\delta \epsilon : X \to Z \in \mathcal{D}}{\delta \epsilon : X \underset{gh}{\Rightarrow} Z} $$
$$ \frac{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{fh}{\overset{\beta}{\Rightarrow}} U}{\alpha : f : S \underset{gf}{\overset{\alpha}{\Rightarrow}} f^+ T \qquad \overline{f \setminus h} : \beta : f^+ T \underset{h}{\overset{\beta}{\Rightarrow}} U} \qquad \alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{fh}{\overset{\beta}{\Rightarrow}} U \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \alpha \cdot \beta : S \underset{gfh}{\overset{\alpha}{\Rightarrow}} U $$

$$ \frac{\alpha : S \underset{gf}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\alpha_{g/\bar{f}} : S \underset{g}{\overset{\alpha}{\Rightarrow}} f^{-} T \qquad \overline{\bar{f}} : \beta : f^{-} T \underset{fh}{\overset{\beta}{\Rightarrow}} U} \qquad \alpha : S \underset{gf}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \alpha_{g/\bar{f}} \cdot \bar{f} : \beta : S \underset{gfh}{\overset{\alpha}{\Rightarrow}} U \qquad \alpha \cdot \beta : S \underset{gfh}{\overset{\alpha}{\Rightarrow}} U $$

Commutative cuts:

$$ \frac{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\overline{\bar{f}} : \alpha : f^{-} S \underset{fg}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U} \qquad \overline{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\alpha \cdot \beta : S \underset{gh}{\overset{\alpha}{\Rightarrow}} U} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \overline{\bar{f}} : (\alpha \cdot \beta) : f^{-} S \underset{fgh}{\overset{\alpha}{\Rightarrow}} U} $$

$$ \frac{\alpha : S \underset{fg}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{f \setminus g : \alpha : f^{+} S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U} \qquad \overline{\alpha : S \underset{fg}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\alpha \cdot \beta : S \underset{fgh}{\overset{\alpha}{\Rightarrow}} U} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad f \setminus gh : (\alpha \cdot \beta) : f^{+} S \underset{gh}{\overset{\alpha}{\Rightarrow}} U} $$

$$ \frac{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\beta : f : T \underset{hf}{\overset{\beta}{\Rightarrow}} f^{+} U} \qquad \overline{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{h}{\overset{\beta}{\Rightarrow}} U}{\alpha \cdot \beta : S \underset{gh}{\overset{\alpha}{\Rightarrow}} U} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad (\alpha \cdot \beta) : f : S \underset{ghf}{\overset{\alpha}{\Rightarrow}} f^{+} U} $$

$$ \frac{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{hf}{\overset{\beta}{\Rightarrow}} U}{\beta : h/\bar{f} : T \underset{h}{\overset{\beta}{\Rightarrow}} U} \qquad \overline{\alpha : S \underset{g}{\overset{\alpha}{\Rightarrow}} T \qquad \beta : T \underset{hf}{\overset{\beta}{\Rightarrow}} U}{\alpha \cdot \beta : S \underset{ghf}{\overset{\alpha}{\Rightarrow}} U} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad (\alpha \cdot \beta)_{gh/\bar{f}} : S \underset{gh}{\overset{\alpha}{\Rightarrow}} f^{-} U} $$

These rules cover all possible cases for a pair of derivations $\alpha, \beta$ whose judgments are composable judgments—the codomain of $\alpha$ is the domain of $\beta$. In particular, notice that when $\alpha$ starts with a right rule, for example a multiplication $\alpha = \alpha'.f, \beta$ must start with the opposite rule on the same arrow, here a division by $f: \beta = f \setminus h \beta'$. This is the only possibility because we know that the two judgments must compose at a type of the form $f^+ T'$, and this formula admits only one left (respectively right) rule.
The definition exhibits some non-determinism on the raw syntax of derivations, as it may be the case that two commutative cut rules are applicable. We consider it well-defined as a function *up to* permutation equivalence (~): whenever several of the cases above would apply, all derivations that can be defined from the definition are permutation equivalent.

Note that this happens only in the cases where the derivation on the left starts with the left rule, and the derivation on the right starts with a right rule. There are four such critical pairs (shapes of derivations that can be composed in two different ways), corresponding to all four permutations of generators. Two pairs are symmetric to each other, so we only need to check three.

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

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

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

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

We will refer to Definition 1.8 as a “cut-elimination procedure”, even if technically speaking it is a proof of cut-admissibility.

**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 sketch.* The proof (detailed in Appendix A.1) proceeds by equational reasoning on proof terms. The following piece of equational reasoning is representative of the rest of the proof, and many other proofs in this section:
$$ 
\begin{align*}
& (\bar{f}.(\alpha.h)) \cdot \beta \\
\sim & \bar{f}.((\alpha.h) \cdot \beta) \\
= & \bar{f}.((\alpha.h) \cdot (h \setminus i \beta')) \\
= & \bar{f}.(\alpha \cdot \beta') \\
\sim & (\bar{f}.\alpha) \cdot \beta' \\
= & ((\bar{f}.\alpha).h) \cdot (h \setminus i \beta') \\
= & ((\bar{f}.\alpha).h) \cdot \beta
\end{align*}
$$

Each reasoning step is by definition of cut-elimination. Principal cuts are defined unambiguously, for example we have $(\alpha.h) \cdot \beta = (\alpha.h) \cdot (h \setminus i \beta')$ by definition. Commutative cuts (left rule in the left derivation, or right rule in the right derivation) are only defined up to permutation equivalence, for example we only have $\bar{f}.(\alpha \cdot \beta') \sim (\bar{f}.\alpha) \cdot \beta'$. $\square$

**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.* See Appendix A.1. $\square$

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

**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 \setminus_g (f_S \cdot \alpha) \qquad \beta \sim (\beta \cdot \bar{g}_T) f / \bar{g} $$

*Proof.* See Appendix A.1. $\square$

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

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

*Proof.* See Appendix A.1. $\square$

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

**1.7. The free bifibration.** We can now formally define $\mathcal{Bif}(p)$ as a category where:

* The objects are the valid formulas $S \sqsubseteq A$, (Section 1.1).

* The arrows between $S \sqsubseteq A$ and $T \sqsubseteq B$ are the valid (closed) derivations of the judgment $S \implies_f T$ for any $f : A \to B \in \mathcal{C}$ (Section 1.2), quotiented by the permutation equivalence relation ($\sim$) (Section 1.5).

* The identity arrow for $S \sqsubseteq A$ is (the equivalence class of) the derivation $\mathrm{id}_S$ (Defn. 1.2).

* The composition of $\alpha : S \implies_g T$ and $\beta : T \implies_h U$ is the cut $\alpha \cdot \beta : S \implies_{gh} U$ (Defn. 1.8).

**Lemma 1.13.** $\mathcal{Bif}(p)$ is a category.

*Proof.* We proved that composition is well-defined on derivations quotiented by permutation equivalence (Lemma 1.9), and that identity and cut satisfy neutrality (Lemma 1.10) and associativity (Lemma 1.12). $\square$

Next we show that $\mathcal{Bif}(p)$ is the domain of a bifibration $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ equipped with a functor $\eta_p : \mathcal{D} \to \mathcal{Bif}(p)$ such that $\Lambda_p \circ \eta_p = p$. We define $\Lambda_p$ by

(1) $\Lambda_p(S \sqsubseteq A) := A$

(2) $\Lambda_p(\alpha : S \implies_f T) := f$

**Lemma 1.14.** $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ is a bifibration.
*Proof.* For any arrow $f: A \to B$ in $\mathcal{C}$ and formula $S \subset A$, the pushforward of $S$ along $f$ is precisely the formula $f^+ S \subset B$, and we have previously defined the arrow $f_S : S \to f^+ S$ as (the equivalence class of) $\mathrm{id}_S \cdot f$. Let us show universality, i.e., that $f_S$ is $+$-cartesian.

For any $g : B \to C$ and $\alpha : S \implies f_g T$, we can take $\beta := f \backslash_g \alpha : f^+ S \implies_g T$. We have to show $\alpha \sim f_S \cdot \beta$:

$$ \begin{align*} & f_S \cdot \beta \\ = & (\mathrm{id}_S \cdot f) \cdot (f \backslash_g \alpha) \\ = & \mathrm{id}_S \cdot \alpha \\ \sim & \alpha \end{align*} $$

as well as unicity: if $\alpha \sim f_S \cdot \beta'$ then

$$ \begin{align*} & \beta' \\ \sim & f \backslash_g (f_S \cdot \beta') \quad \text{by } \eta\text{-expansion (Lemma 1.11)} \\ \sim & f \backslash_g \alpha \\ = & \beta \end{align*} $$

The case for $\bar{g}_T : g^T T \to T$ is symmetrical. $\square$

We define the functor $\eta_p : \mathcal{D} \to \mathcal{Bif}(p)$ by interpreting every object $X$ of $\mathcal{D}$ as an atomic formula and every arrow $\delta : X \to Y$ as an initial axiom, and it is immediate that $\Lambda_p \circ \eta_p = p$.

Lastly, we need to show that $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ is universal in the sense explained before, that for any bifibration $q : \mathcal{E} \to \mathcal{C}$ equipped with a functor $\theta : \mathcal{D} \to \mathcal{E}$ such that $q \circ \theta = p$, there exists a unique morphism of bifibrations $\llbracket - \rrbracket_\theta : \Lambda_p \to q$ making the diagram below commute:

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

We already defined the interpretation $\llbracket - \rrbracket_\theta$ of formulas and proof terms in Section 1.4, and showed that it respects permutation equivalence (Lemma 1.5). We now establish that it is a functor $\llbracket - \rrbracket_\theta : \mathcal{Bif}(p) \to \mathcal{E}$, and that it is the unique morphism of bifibrations making the diagram above commute.

**Lemma 1.15.** $\llbracket - \rrbracket_\theta : \mathcal{Bif}(p) \to \mathcal{E}$ is a functor.

*Proof.* We prove the interpretation respects identities $\llbracket \mathrm{id}_S \rrbracket_\theta = \mathrm{id}_{\llbracket S \rrbracket_\theta}$ by induction on $S$:

$$ \llbracket \mathrm{id}_X \rrbracket_\theta = \theta(\mathrm{id}_X) = \mathrm{id}_{\theta(X)} = \mathrm{id}_{\llbracket X \rrbracket_\theta} $$

$$ \begin{align*} & \llbracket \mathrm{id}_{f^+ S} \rrbracket_\theta \\ = & \llbracket f \backslash_{\mathrm{id}_B} (\mathrm{id}_S \cdot f) \rrbracket_\theta \\ = & f \backslash_{\mathrm{id}_B} \left( \llbracket \mathrm{id}_S \rrbracket_\theta f_{\llbracket S \rrbracket_\theta} \right) \\ = & f \backslash_{\mathrm{id}_B} \left( \mathrm{id}_{\llbracket S \rrbracket_\theta} f_{\llbracket S \rrbracket_\theta} \right) \quad \text{by induction on } S \\ = & f \backslash_{\mathrm{id}_B} f_{\llbracket S \rrbracket_\theta} \\ = & \mathrm{id}_{\llbracket S \rrbracket_\theta} \quad \text{property of cartesian liftings} \end{align*} $$
(The case of the identity on $\bar{g}^T$ is symmetrical.)

We prove that the interpretation respects composition $[[\alpha \cdot \beta]]_{\theta} = [[\alpha]]_{\theta} [[\beta]]_{\theta}$ by simultaneous induction on the derivations $\alpha$ and $\beta$. Representative cases follow:

$$ \begin{aligned} [[\delta \cdot \epsilon]]_{\theta} &= [[\delta \epsilon]]_{\theta} = \theta(\delta \epsilon) = [[\delta]]_{\theta} [[\epsilon]]_{\theta} && \text{by (0.1)} \\ &= [[\alpha \cdot \beta]]_{\theta} f_{\llbracket S \rrbracket_{\theta}} (f \setminus h [[\beta]]_{\theta}) \\ &= [[\alpha]]_{\theta} [[\beta]]_{\theta} \\ &= [[\alpha \cdot \beta]]_{\theta} \\ &= [[(\alpha \cdot f) \cdot (f \setminus h \beta)]]_{\theta} \end{aligned} $$

$$ \begin{aligned} [[\alpha \cdot (\beta.f)]_{\theta} &= [[\alpha \cdot (\beta h / \bar{f})]]_{\theta} \\ = [[(\alpha \cdot \beta).f]]_{\theta} &= [[(\alpha \cdot \beta) gh / \bar{f})]]_{\theta} \\ = [[\alpha \cdot \beta]]_{\theta} f_{\llbracket U \rrbracket_{\theta}} &= [[\alpha]]_{\theta} [[\beta]]_{\theta} gh / \bar{f} \\ = [[\alpha]]_{\theta} [[\beta]]_{\theta} f_{\llbracket U \rrbracket_{\theta}} &= [[\alpha]]_{\theta} ([\beta]_{\theta} h / \bar{f}) \quad \text{by Proposition 1.3} \\ = [[\alpha]]_{\theta} [[\beta.f]]_{\theta} &= [[\alpha]]_{\theta} [[\beta h / \bar{f}]]_{\theta} \end{aligned} $$

□

**Lemma 1.16.** $[[\cdot]]_{\theta} : \Lambda_{p} \to q$ is the unique morphism of bifibrations such that $[[\cdot]]_{\theta} \circ \eta_{p} = \theta$.

*Proof.* Recall that the interpretation was defined as follows on terms:

$$ [[\delta]]_{\theta} = \theta(\delta) $$

$$ [[\alpha.f]]_{\theta} = [[\alpha]]_{\theta} f \qquad [[f \setminus_g \alpha]]_{\theta} = f \setminus_g [[\alpha]]_{\theta} $$

$$ [[\bar{g}.\alpha]]_{\theta} = \bar{g} [[\alpha]]_{\theta} \qquad [[\alpha f / \bar{g}]]_{\theta} = [[\alpha]]_{\theta} f / \bar{g} $$

The equation $[[\cdot]]_{\theta} \circ \eta_{p} = \theta$ holds immediately by construction.

To be a morphism of bifibrations, the interpretation must send cartesian arrows to cartesian arrows of the same type. This follows from the definition and the previous lemma. For $+-$cartesian arrows for example, we have:

$$ [[f_S]]_{\theta} = [[\mathrm{id}_S \cdot f]]_{\theta} = [[\mathrm{id}_S]]_{\theta} f_{\llbracket S \rrbracket_{\theta}} = \mathrm{id}_{\llbracket S \rrbracket_{\theta}} f_{\llbracket S \rrbracket_{\theta}} = f_{\llbracket S \rrbracket_{\theta}} $$

Finally, for unicity we remark that each of the five equations defining the interpretation $[[\cdot]]_{\theta}$ must hold for any morphism of bifibrations $\tau : \Lambda_{p} \to q$ such that $\tau \circ \eta_{p} = \theta$, so necessarily $\tau = [[\cdot]]_{\theta}$. □

Putting it all together, we conclude with the main theorem of this section.

**Theorem 1.17.** $\Lambda_{p} : \mathrm{Bif}(p) \to \mathcal{C}$ is the free bifibration on $p : \mathcal{D} \to \mathcal{C}$.

An immediate consequence—applying one of the equivalent characterizations of adjunctions [38, Theorem IV.1.2(ii), p.83]—is that we can construct a functor

$$ \Lambda : \mathrm{Cat}/\mathcal{C} \to \mathrm{BifCat}(\mathcal{C}) $$
Logical equivalence should be distinguished from the weaker notion of isomorphism $S \cong T$ given by isomorphism in the total category $\mathcal{Bif}(p)$, i.e., a pair of derivations $\alpha : S \implies_f T$ and $\beta : T \implies_g S$ such that $\alpha \cdot \beta \sim \mathrm{id}_S$ and $\beta \cdot \alpha \sim \mathrm{id}_T$ (where one does not require $f$ and $g$ to be identity arrows or that $S \subset A$ and $T \subset B$ lie over the same object).

**Proposition 1.21** (Pseudofunctoriality). The following logical equivalences hold

$$ (g \circ f)^+ S \equiv g^+ f^+ S \qquad (1.10) $$

$$ (f g)^- T \equiv f^- g^- T \qquad (1.11) $$

$$ \mathrm{id}^+ U \equiv U \equiv \mathrm{id}^- U \qquad (1.12) $$

for all $f, g, S, T, U$ of the appropriate type.

*Proof.* By Proposition 1.20, this is a corollary of Lemma 1.14, since these isomorphisms hold in the fiber categories of any bifibration. Working out the derivation explicitly, the equivalence (1.10), for instance, is witnessed by the following derivations (parameterized by $S \subset A$, $f : A \to B$, and $g : B \to C$), whose compositions are permutation equivalent to the identity derivations on $(g \circ f)^+ S$ and $g^+ f^+ S$:

$$ \begin{array}{c} \overline{S \implies_S S} \\ \overline{S \implies_f f^+ S} \\ \overline{S \implies_{fg} g^+ f^+ S} \\ \hline \overline{(g \circ f)^+ S \implies_{\mathrm{id}_C} g^+ f^+ S} \end{array} \qquad \begin{array}{c} \overline{S \implies_S S} \\ \overline{S \implies_{fg} (g \circ f)^+ S} \\ \overline{f^+ S \implies_g (g \circ f)^+ S} \\ \hline \overline{g^+ f^+ S \implies_{\mathrm{id}_C} (g \circ f)^+ S} \end{array} $$

□

More generally, by Theorem 1.17 we have

**Corollary 1.22.** Given a functor $p : \mathcal{D} \to \mathcal{C}$, two bifibrational formulas $S_1, S_2 \subset A$ are logically equivalent $S_1 \equiv S_2$ iff their interpretations are isomorphic $[[S_1]]_\theta \cong [[S_2]]_\theta$ in every fiber category $\mathcal{E}_A$ for every bifibration $q : \mathcal{E} \to \mathcal{C}$ and functor $\theta : \mathcal{D} \to \mathcal{E}$ such that $q \circ \theta = p$.

Finally, let us observe that the free bifibration construction is *conservative*.

**Proposition 1.23** (Conservativity). The functor $\eta_p : \mathcal{D} \to \mathcal{Bif}(p)$ is full and faithful.

Conservativity is obvious by inspection of the sequent calculus, since the only way to prove an atomic sequent $X \implies_f Y$ is by providing an arrow $\delta : X \to Y$ in $\mathcal{D}$ such that $p(\delta) = f$. Faithfulness of $\eta_p$ is also a corollary of the following stronger statement, whose proof only uses the universal property of the free bifibration, and which will serve us in the next section.

**Proposition 1.24.** The functor $\eta_p : \mathcal{D} \to \mathcal{Bif}(p)$ is equipped with a left inverse $\chi_p : \mathcal{Bif}(p) \to \mathcal{D}$, such that the pairing $(\chi_p, \Lambda_p) : \mathcal{Bif}(p) \to \mathcal{D} \times \mathcal{C}$ is a morphism of bifibrations from $\Lambda_p$ to the trivial bifibration $\pi_2 : \mathcal{D} \times \mathcal{C} \to \mathcal{C}$.
*Proof.* Projection functors $\pi_2 : \mathcal{D} \times \mathcal{C} \to \mathcal{C}$ are always bifibrations, with cartesian liftings defined by

$$ (X, A) \xrightarrow{(\mathrm{id}_X, f)} (X, B) := f^+(X, A) \qquad g^-(X, C) := (X, B) \xrightarrow{(\mathrm{id}_X, g)} (X, C) $$
$$ A \xrightarrow{f} B \qquad B \xrightarrow{g} C $$

By the universal property of the free bifibration, we therefore obtain a unique morphism of bifibrations $\llbracket - \rrbracket_\theta : \Lambda_p \to \pi_2$

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

where $\theta := (\mathrm{id}_{\mathcal{D}}, p)$. This proves the proposition, taking $\chi_p := \pi_1 \circ \llbracket - \rrbracket_\theta$ and using the universal property of the product of categories. $\square$

In terms of our concrete description of the free bifibration, $\chi_p : \mathrm{Bif}(p) \to \mathcal{D}$ is the functor sending a bifibrational formula to its atomic source and sending an equivalence class of derivations to the necessarily unique initial axiom with which all of the derivations begin.

**1.9. Related work.** There is a well-known construction, originally due to Gray [19], of the free fibration on a functor (or dually the free opfibration) as a comma category. The standard construction actually defines a *split* (op)fibration, in the sense that the pseudofunctoriality laws (1.10)–(1.12) collapse to strict equalities, although one can represent non-split fibrations and opfibrations as pseudo-algebras for the corresponding pseudomonads (see the account by Anders Kock [28], as well as recent work of Emmenegger, Mesiti, Rosolini, and Streicher on an alternative construction of fibrations [17]). Conversely, our construction produces a non-split bifibration, but one can recover a split bifibration by restricting to *nonidentity strictly alternating formulas* (see Section 3.3 below, and in particular Theorem 3.5). It is worth mentioning that since a functor is a bifibration just in case it is both a fibration and an opfibration, the free bifibration monad is formally the coproduct of the free fibration and the free opfibration monads—but this characterization does not give much help in constructing it explicitly.

We will discuss Lamarche's construction of the free bifibration on a functor along with Dawson, Paré, and Pronk's closely related $\Pi_2(\mathcal{C})$ construction, both already referenced in the Introduction, further in Section 2.

The notation $S \subset A$ to denote an object $S \in \mathrm{Bif}(p)$ such that $\Lambda_p(S) = A$ is taken from Melliès and Zeilberger's work on functors as type refinement systems [40], and more broadly our proof-theoretic construction is inspired in part from their suggestive type-theoretic reading of bifibrations [41, 42], as well as from the bifibrational calculus of Licata, Shulman, and Riley [37]. This approach of course owes much to the tradition of categorical proof theory as pioneered by Lambek [35].
and prove that it is associative and neutral relative to $U$. We will recover vertical composition $\odot$ as the special case $p = \mathrm{id}_c$ of a more general action

$$ \circled{p} : \mathcal{B}if(p) \Lambda_p \times_{\mathrm{src}} \mathcal{Z}(\mathcal{C}) \to \mathcal{B}if(p) $$

of $\mathcal{Z}(\mathcal{C})$ on any free bifibration $\mathcal{B}if(p)$.

To define this action, let us begin by observing that the sequent calculus for $\mathcal{Z}(\mathcal{C})$ shares the same logical inference rules as any free bifibration $\mathcal{B}if(p)$ over the same base category: their sequent calculi only differ in the choice of atomic formulas and initial axioms. Moreover, both atomic formulas and initial axioms of $\mathcal{Z}(\mathcal{C})$ carry no information, since they are uniquely determined by the underlying object/arrow of the base category. These observations make clear that we can define the action of $\mathcal{Z}(\mathcal{C})$ on $\mathcal{B}if(p)$ as follows:

* at the level of formulas, given a formula $S \subset A$ and a zigzag $Z : A \rightsquigarrow B$, the formula $S \circled{\ast} Z \subset B$ is obtained by substituting $S$ for the unique atom $A$ in $Z$;

* at the level of proofs (i.e., representatives of arrows), given $\alpha \in \mathcal{B}if(p)$ such that $\Lambda_p(\alpha) = f$ and $\zeta \in \mathcal{Z}(\mathcal{C})$ such that $\mathrm{src}(\zeta) = f$ and $\mathrm{tgt}(\zeta) = g$, the proof $\alpha \circled{\ast}_p \zeta \in \mathcal{B}if(p)$ such that $\Lambda_p(\alpha \circled{\ast}_p \zeta) = g$ is obtained by substituting $\alpha$ for the unique initial axiom $f$ in $\zeta$.

As a visual aid, let us write "$\square$" for the uniquely determined atoms and axioms in a zigzag formula/proof. Formally, the action can then be expressed inductively as follows:

$$ S \circled{\ast}_p \square = S $$

$$ S \circled{\ast}_p (f^+ Z) = f^+(S \circled{\ast}_p Z) $$

$$ S \circled{\ast}_p (g^- Z) = g^-(S \circled{\ast}_p Z) $$

$$ \alpha \circled{\ast}_p \square = \alpha $$

$$ \alpha \circled{\ast}_p (\zeta.f) = (\alpha \circled{\ast}_p \zeta).f $$

$$ \alpha \circled{\ast}_p (f \backslash_g \zeta) = f \backslash_g (\alpha \circled{\ast}_p \zeta) $$

$$ \alpha \circled{\ast}_p (\bar{g} \cdot \zeta) = \bar{g} \cdot (\alpha \circled{\ast}_p \zeta) $$

$$ \alpha \circled{\ast}_p (\zeta f / \bar{g}) = (\alpha \circled{\ast}_p \zeta) f / \bar{g} $$

**Proposition 2.1.** *The action extends to a functor $\circled{\ast}_p : \mathcal{B}if(p) \Lambda_p \times_{\mathrm{src}} \mathcal{Z}(\mathcal{C}) \to \mathcal{B}if(p)$.*

*Proof.* Since $\circled{\ast}_p$ is defined as a substitution operator, it is immediate that it respects permutation equivalence of proofs in the sense that we can define $[\alpha] \circled{\ast}_p [\zeta] := [\alpha \circled{\ast}_p \zeta]$ without ambiguity. To show that it is functorial, we need to verify the permutation equivalence

$$ (\alpha \cdot \alpha') \circled{\ast}_p (\zeta \cdot \zeta') \sim (\alpha \circled{\ast}_p \zeta) \cdot (\alpha' \circled{\ast}_p \zeta') \quad (2.1) $$

for all $\alpha, \alpha' \in \mathcal{B}if(p)$ and $\zeta, \zeta' \in \mathcal{Z}(\mathcal{C})$ for which these operations are defined. This follows from the definition of cut (Definition 1.8) by a straightforward induction on $\zeta$ and $\zeta'$. $\square$

We can now define the vertical composition functor $\odot : \mathcal{Z}(\mathcal{C}) \xrightarrow{\mathrm{tgt}} \mathrm{src} \mathcal{Z}(\mathcal{C}) \to \mathcal{Z}(\mathcal{C})$ as the action of $\mathcal{Z}(\mathcal{C})$ on itself, $\odot := \circled{\ast}_{\mathrm{id}_c}$, and use that to define the double category of zigzags.

**Proposition 2.2.** *Vertical composition $\odot$ is strictly associative and neutral relative to $U$.*

*Proof.* Immediate from the definition of $\circled{\ast}_p$ as a substitution operator. $\square$

**Definition 2.3.** The **zigzag double category** of $\mathcal{C}$, notated $\mathbb{Z}(\mathcal{C})$, is defined as a strict double category by the data $\mathbb{Z}(\mathcal{C}) := (\mathcal{C}, \mathcal{Z}(\mathcal{C}), \mathrm{src}, \mathrm{tgt}, U, \odot)$, where

$$ \mathbb{Z}(\mathcal{C}) := \mathcal{B}if(p) \quad \mathrm{src} := \chi_p \quad \mathrm{tgt} := \Lambda_p \quad U := \eta_p \quad \odot := \circled{\ast}_p $$

as explained above, for $p = \mathrm{id}_c$.
Notice that with this definition, equation (2.1) specializes to the interchange axiom for the double category $\mathbb{Z}(\mathcal{C})$. We already saw in Section 1.5 that the permutation equivalence relations were necessary for obtaining a bifibration, but it is worth mentioning that this axiom also forces the definition of permutation equivalence. For example, the permutation relation (1.3) may be rederived as follows:

$$
\begin{align*}
(f \backslash_g \alpha).h &= (\alpha \circledast (f \backslash_g fg)) \cdot (\mathrm{id}_T . h \circledast h) & \text{defn. of } \circledast \\
&\sim (\alpha \cdot (\mathrm{id}_T . h)) \circledast ((f \backslash_g fg) \cdot h) & \text{by (2.1)} \\
&\sim (\alpha.h) \circledast (f \backslash_{gh} fgh) & \text{properties of cut and id} \\
&= f \backslash_{gh} (\alpha.h) & \text{defn. of } \circledast
\end{align*}
$$

Similar observations were made by Dawson, Paré, and Pronk [14, §1.5] and by Lamarche [32, p.12].

2.2. **From inference rules to double cells.** Having established that the free bifibration on the identity functor $\mathrm{id}_\mathcal{C} : \mathcal{C} \to \mathcal{C}$ generates a double category of zigzags in $\mathcal{C}$, at this point let us develop a more diagrammatic presentation of $\mathbb{Z}(\mathcal{C})$ that is isomorphic to Definition 2.3 but will help us to better visualize it as a double category.

An easy but important observation is that what we have called “zigzag formulas” (that is, objects of the free bifibration $\mathbb{Z}(\mathcal{C}) := \mathrm{Bif}(\mathrm{id}_\mathcal{C}))$ really are in one-to-one correspondence with zigzags of arrows in the category $\mathcal{C}$. Of course we have not defined what a “zigzag of arrows” is formally, but one possible definition is, say, as a graph homomorphism $Z : \tilde{L} \to \mathcal{C}$ from some orientation $\tilde{L}$ of the line graph $L_n$ with $n$ edges and $n+1$ vertices into the underlying graph of $\mathcal{C}$, for some $n \ge 0$. It is clear that such a graph homomorphism can be represented as a zigzag formula with $n$ total pushes and pulls, and vice versa. For example, if $\mathcal{C}$ is the category on the left and $Z$ is the (preformally defined!) zigzag on the right,

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

then $Z$ can be encoded isomorphically either as a graph homomorphism $Z : \tilde{L} \to \mathcal{C}$ where

$$
\begin{align*}
\tilde{L} &= v_0 \xrightarrow{e_1} v_1 \xrightarrow{e_2} v_2 \xleftarrow{e_3} v_3 \xrightarrow{e_4} v_4 \\
Z(v_0) &= A \quad Z(v_1) = Z(v_3) = B \quad Z(v_2) = D \quad Z(v_4) = C \\
Z(e_1) &= f \quad Z(e_2) = h \quad Z(e_3) = g \quad Z(e_4) = g
\end{align*}
$$

or by the zigzag formula $Z = g^+ h^- h^+ f^+ A$. One important point is that both of these representations allow us to represent the *empty zigzag*, which corresponds to a choice of object in $\mathcal{C}$, and should not be confused with a one-step zigzag along an identity arrow.

Now turning to double cells, observe that each logical inference rule of the sequent calculus, recalled below for reference, may be interpreted as a generating double cell of $\mathbb{Z}(\mathcal{C})$
from the transpose of the zigzag double category into the double category of spans of sets,
by the following mappings:

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

Note the transpose is necessary because the tight morphisms of $\mathbb{Z}(\mathcal{C})$ are sent to loose morphisms of $\operatorname{Span}(\operatorname{Set})$.

In particular, $\partial \Lambda_p$ maps each generator of $\mathbb{Z}(\mathcal{C})$ to a double cell of spans:

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

One might think of this interpretation as internalizing the idea of an inference rule as a transformation from a proof of the premise(s) into a proof of the conclusion. Notice that this double functor $\partial \Lambda_p : \mathbb{Z}(\mathcal{C})^\top \to \operatorname{Span}(\operatorname{Set})$

• *strictly preserves composition of zigzags*: since $\circled_p$ is a strict action, with the equation $x \circled (a \odot b) = (x \circled a) \circled b$ corresponding to simple chaining of logical connectives and inference rules;

• *laxly preserves composition of arrows in $\mathcal{C}$*: since the span morphisms $\mathrm{Pf}_f \cdot \mathrm{Pf}_g \to \mathrm{Pf}_{fg}$, which correspond to cut-elimination, are typically not invertible.

In fact, this construction is very general and can be applied to any bifibration $q : \mathcal{E} \to \mathcal{C}$ to derive a lax double functor $\partial q : \mathbb{Z}(\mathcal{C})^\top \to \operatorname{Span}(\operatorname{Set})$. On the horizontal category $\mathcal{H}(\mathbb{Z}(\mathcal{C})) = \mathcal{C}$, this functor sends every object $A \in \mathcal{C}$ to the set $\mathrm{Ob}_A = \{S \in \mathcal{E} \mid q(S) = A\}$ of objects lying over it, and similarly every arrow $f : A \to B$ to the set $\mathrm{Arr}_f = \{\alpha \in \mathcal{E} \mid q(\alpha) = f\}$ of arrows lying over it, which is equipped with evident projections $\mathrm{Ob}_A \leftarrow \mathrm{Arr}_f \to \mathrm{Ob}_B$. This
extends to the generators of $\mathbb{Z}(\mathcal{C})$ by interpreting the span morphisms

$$
\begin{tikzcd}
& & \operatorname{Ob}_A \arrow[r] \arrow[d] & \operatorname{Ob}_C \arrow[d] \\
\operatorname{Ob}_B \arrow[r] \arrow[d] & \operatorname{Arr}_{fg} \arrow[r] \arrow[d] & \operatorname{Ob}_C \arrow[d] \\
\operatorname{Ob}_C \arrow[r] & \operatorname{Arr}_{g'} \arrow[r] \arrow[d] & \operatorname{Ob}_{C'} \arrow[d] \\
\operatorname{Ob}_B \arrow[r] & \operatorname{Arr}_{gg'} \arrow[r] \arrow[d] & \operatorname{Ob}_{C'}
\end{tikzcd}
\qquad
\begin{tikzcd}
& & \operatorname{Ob}_{A'} \arrow[r] \arrow[d] & \operatorname{Ob}_A \arrow[d] \\
\operatorname{Ob}_{A'} \arrow[r] & \operatorname{Arr}_{f'} \arrow[d] & \operatorname{Ob}_B \arrow[d] \\
\operatorname{Ob}_A \arrow[r] & \operatorname{Arr}_{fg} \arrow[r] \arrow[d] & \operatorname{Ob}_C \arrow[d] \\
\operatorname{Ob}_A \arrow[r] & \operatorname{Arr}_f \arrow[r] \arrow[d] & \operatorname{Ob}_B
\end{tikzcd}
\qquad (2.6)
$$

using the bifibrational structure of $q$, very similarly to how we defined the interpretation
functor $\underline{\otimes}^-\theta : \Lambda_p \to \mathcal{E}$ from the free bifibration in Section 1.4. For example, the function
$f^+ : \operatorname{Ob}_A \to \operatorname{Ob}_B$ maps any object $S \in \mathcal{E}$ lying over $A$ to (the object component of)
its pushforward $f^+ S$, the span morphism $\mathrm{L}^+ : \operatorname{Arr}_{fg} \to \operatorname{Arr}_g$ is interpreted using the
universal property of this pushforward, and $\mathrm{R}^+ : \operatorname{Arr}_{f'} \to \operatorname{Arr}_{f'f}$ by postcomposition with
the associated $+-$cartesian arrow $S \to f^+ S$.

Conversely, any such lax double functor $F : \mathbb{Z}(\mathcal{C})^{\top} \to \mathbb{Span}(\mathcal{Set})$ determines a category $\int_{\mathcal{C}} F$ together with a functor $\pi_{\mathcal{C}} : \int_{\mathcal{C}} F \to \mathcal{C}$ equipped with the structure of a bifibration. Indeed, the category $\int_{\mathcal{C}} F$ is constructed in the usual way as a displayed category: objects of $\int_{\mathcal{C}} F$ are given by pairs $(A, S)$ of an object $A \in \mathcal{C}$ and an element $S \in F(A)$, arrows are given by pairs $(f, \alpha)$ of an arrow $f \in \mathcal{C}$ and an element $\alpha \in F(f)$ (meaning an element of the apex of the span $F(A) \leftarrow F(f) \to F(B)$), and composition and identity arrows are defined using the lax structure of $F$.

In turn, the tight component of the lax double functor $F : \mathbb{Z}(\mathcal{C})^{\top} \to \mathbb{Span}(\mathcal{Set})$ enables
us to go further and equip the projection functor $\pi_{\mathcal{C}} : \int_{\mathcal{C}} F \to \mathcal{C}$ with the structure of a
bifibration. For example, the pushforward along an arrow $f : A \to B$ is defined using
the functions $F(f^+ A) : F(A) \to F(B)$ to compute pushforward objects, and applying
$F(\mathrm{R}^+) : F(\mathrm{id}_A) \to F(f)$ to an identity arrow to compute the associated cartesian arrow.
The universal property of this pushforward is derived from the interpretation of $F(\mathrm{L}^+)$ and
the defining equations of $\mathbb{Z}(\mathcal{C})$.

The constructions $\partial$ and $\int$ witness an equivalence

$$
\begin{tikzcd}
& & \mathcal{D} \\
& & \arrow[r, "\cong"] \\
\mathcal{C} & \arrow[rr, "\text{bifibration}", "\simeq"] & \mathbb{Z}(\mathcal{C})^{\top} \arrow[r, "\text{lax}", "\xrightarrow{\phantom{\text{bifibration}}} \text{Span}(\mathcal{Set})"'] & \text{Span}(\mathcal{Set})
\end{tikzcd}
$$

and one might therefore reasonably refer to a lax double functor $F : \mathbb{Z}(\mathcal{C})^{\top} \to \mathrm{Span}(\mathcal{Set})$ as
a "displayed bifibration".

We will not pursue these reflections further in this paper, although we think they could
eventually be helpful for developing a more algebraic perspective on the sequent calculus.

2.4. **A dagger structure on zigzags.** One advantage of considering free bifibrations in terms of the double category of zigzags is that the latter clearly has a large degree of symmetry. Of particular relevance is a dagger-type involution

$(-)^{\dagger} : \mathbb{Z}(\mathcal{C}) \to \mathbb{Z}(\mathcal{C})^{\nu}$
that reverses the direction of vertical arrows and double cells. Formally, this corresponds to
an endofunctor on $Z(C)$ swapping source and target while leaving the underlying arrows in
$C$ invariant:

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

At the level of formulas, $(-)^{\dagger}$ turns pushforwards into pullbacks and vice versa while reversing the sequence of connectives applied (e.g., $(h^{+} g^{-} f^{+} \Box)^{\dagger} = f^{-} g^{+} h^{-} \Box$). More geometrically, the transformation may be visualized as reflecting the generating cells (2.2) across the $x$-axis (or equivalently reading them from bottom to top), which swaps $Lf^{+}$ with $Lf^{-}$ and $Rg^{+}$ with $Rg^{-}$. The $(-)^{\dagger}$ transformation extends to arbitrary stacks of double cells by $(\gamma_1 \odot \cdots \odot \gamma_n)^{\dagger} = \gamma_n^{\dagger} \odot \cdots \odot \gamma_1^{\dagger}$. The following is immediate.

**Proposition 2.6.** $(-)^{\dagger}$ is an involutive isomorphism.

As a corollary, we can derive that the pairing of the source and target functors is a bifibration.

**Theorem 2.7 (Lamarche [33, Theorem 3]).** (src, tgt) : $Z(C) \to C \times C$ is a bifibration.

*Proof.* By Proposition 2.6, $\text{src} : Z(C) \to C$ is a bifibration since it inherits a bifibrational structure from $\text{tgt}$ via the $(-)^{\dagger}$ involution. As we saw earlier by Proposition 1.24, the pairing $(\text{src}, \text{tgt}) : Z(C) \to C \times C$ is a morphism of bifibrations from $\text{tgt}$ to $\pi_2$, which means that $\text{tgt}$-cartesian arrows in $Z(C)$ are mapped by $\text{src}$ to identity arrows in $C$. Symmetrically, applying the $(-)^{\dagger}$ involution, it is also a morphism of bifibrations from $\text{src}$ to $\pi_1$. This ensures that the pairing is a bifibration $(\text{src}, \text{tgt}) : Z(C) \to C \times C$, since the two bifibrational structures act independently. $\square$

**2.5. Recovering the free adjoint construction.** Given a double category $\mathbb{E}$ seen as an internal category $\mathbb{E} = (\mathbb{C}, \mathcal{E}, \text{src}_{\mathcal{E}}, \text{tgt}_{\mathcal{E}}, U_{\mathcal{E}}, \odot_{\mathcal{E}})$, we write $\mathcal{H}(\mathbb{E}) = \mathbb{C}$ for its underlying horizontal category. Any double category $\mathbb{E}$ also induces a vertical 2-category denoted $\mathcal{V}(\mathbb{E})$, with same set of objects, 1-cells given by vertical arrows $F : A \dashrightarrow B$, and 2-cells $\alpha : F \Longrightarrow G$ given by globular double cells

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

that is, cells whose source and target are identities.

A double category $\mathbb{E}$ is said to be *fibrant* (or to be a *framed bicategory* [49]) just in case the pairing of its source and target functors $(\text{src}_{\mathcal{E}}, \text{tgt}_{\mathcal{E}}) : \mathcal{E} \to \mathbb{C} \times \mathbb{C}$ is a fibration, or equivalently an opfibration, and therefore a bifibration [49, Theorem 4.1]. This is equivalent to asking that the double category has all *companions and conjoints* meaning that for every
horizontal arrow $f: A \to B$ there is both a vertical arrow $F_f: A \dashrightarrow B$ and a vertical arrow $G_f: B \dashrightarrow A$ equipped with a pair of cells

$$ \begin{array}{ccc} A & = & A \\ \Vert & \alpha & \phi_{F_f} \\ A & \underset{f}{\to} & B \end{array} \qquad \begin{array}{ccc} B & = & B \\ G_f \phi & \beta & \Vert \\ A & \underset{f}{\to} & B \end{array} $$

satisfying a few equations (see [16] and [49, Theorem A.2]); note that the conventions for the roles of horizontal and vertical arrows are often swapped in the literature).

Fibrant double categories are moreover essentially equivalent to proarrow equipments [49, Appendix C]. In particular, any fibrant double category $\mathcal{E}$ canonically determines an identity-on-objects pseudofunctor $(-)^+ : \mathcal{C} \to \mathcal{K}$ from its underlying horizontal category $\mathcal{C} = \mathcal{H}(\mathcal{E})$ to its vertical 2-category $\mathcal{K} = \mathcal{V}(\mathcal{E})$ that sends every horizontal arrow $f$ to its vertical companion $F_f$, which has a right adjoint $F_f \dashrightarrow G_f$ given by the vertical conjoint. Conversely, given a 2-category $\mathcal{K}$ equipped with a pseudofunctor $I : \mathcal{C} \to \mathcal{K}$ such that every arrow $f \in \mathcal{C}$ is mapped to an arrow $If \in \mathcal{K}$ with a right adjoint, one can define an associated double category $\mathcal{E}_{\mathcal{K}}$ whose objects and horizontal arrows are the objects and arrows of $\mathcal{C}$, whose vertical arrows $M : A \to B$ are 1-cells $M : IA \to IB$ in $\mathcal{K}$, and whose double cells

$$ \begin{array}{ccc} A & \underset{f}{\to} & C \\ M \underset{\downarrow}{\phi} & \alpha & \underset{\downarrow}{\phi} N \\ B & \underset{g}{\to} & D \end{array} $$

are 2-cells $\alpha : M \cdot Ig \Rightarrow If \cdot N$ in $\mathcal{K}$. Then $\mathcal{E}_{\mathcal{K}}$ is a fibrant double category [49, Prop. C.3].

The correspondence between fibrant double categories and proarrow equipments means that we can recover Dawson, Paré, and Pronk's free adjoint construction $\Pi_2(\mathcal{C})$ up to equivalence as the vertical 2-category of $\mathbb{Z}(\mathcal{C})$.

**Theorem 2.8.** $\mathbb{Z}(\mathcal{C})$ is the free fibrant double category over $\mathcal{C}$.

*Proof.* By Theorem 2.7, $\mathbb{Z}(\mathcal{C})$ is a fibrant double category. Moreover, given any other fibrant double category $\mathcal{E} = (\mathcal{C}, \mathcal{E}, \text{src}_{\mathcal{E}}, \text{tgt}_{\mathcal{E}}, U_{\mathcal{E}})$ with underlying horizontal category $\mathcal{H}(\mathcal{E}) = \mathcal{C}$, there exists a unique double functor $\mathbb{Z}(\mathcal{C}) \to \mathcal{E}$ whose underlying functor $\mathbb{Z}(\mathcal{C}) \to \mathcal{E}$ is a morphism of bifibrations from $(\text{src}, \text{tgt})$ to $(\text{src}_{\mathcal{E}}, \text{tgt}_{\mathcal{E}})$. Indeed, any double functor $\mathbb{Z}(\mathcal{C}) \to \mathcal{E}$ is determined by the image of the generators (2.2), and the image of the generators is uniquely determined by the bifibrational structure of $\text{src}_{\mathcal{E}} : \mathcal{E} \to \mathcal{C}$ and $\text{tgt}_{\mathcal{E}} : \mathcal{E} \to \mathcal{C}$. $\square$

In particular, there is an identity-on-objects pseudofunctor $(-)^+ : \mathcal{C} \to \mathcal{V}(\mathbb{Z}(\mathcal{C}))$ mapping every arrow $f: A \to B$ of $\mathcal{C}$ to the forward zigzag $f^+ A: A \dashrightarrow B$, which has a right adjoint given by the backward zigzag $f^- B: B \dashrightarrow A$. Observe that $(-)^+$ is only a pseudofunctor rather than a strict functor because, as we already observed, the free bifibration is not split in the sense that the canonical identities $(g \circ f)^+ S \equiv g^+ f^+ S$ and $\text{id}^+ U \equiv U$ only hold as isomorphisms in the fiber categories rather than as strict equalities. In contrast, Dawson, Paré, and Pronk constructed $\Pi_2(\mathcal{C})$ in a way that admits a strict embedding functor $(-)^+ : \mathcal{C} \to \Pi_2(\mathcal{C})$. Nevertheless, up to splitting of the free bifibration (see Theorem 3.5 below), the two constructions are equivalent.

**Corollary 2.9.** $\mathcal{V}(\mathbb{Z}(\mathcal{C})) \simeq \Pi_2(\mathcal{C})$.
**2.6. From double cells to string diagrams.** Another reward of the double categorical analysis is that it leads to a natural graphical calculus, derived by applying standard conventions of string diagrams to the generators of $\mathbb{Z}(\mathcal{C})$. The idea is simple: we begin by dualizing the generators (2.2) geometrically, so that cells become vertices and objects become regions, while arrows become edges separating the regions which meet at a vertex:

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

Then we remove the vertices, depicting the cells by simply bending edges appropriately:

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

The permutation equivalences (1.2)–(1.5) corresponding to the stack relations (2.3) now have natural interpretations as planar isotopies. For example, (1.2) and (1.3) (which permute $\mathbb{R}^+$ with $\mathbb{L}^-$ and $\mathbb{L}^+$ respectively) may be depicted as follows:

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

The equations defining cut-elimination (Definition 1.8) also have natural topological interpretations. Below we illustrate one principal cut case and one commutative cut case:

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

We recover in this way the calculus of planar arc diagrams that was used by Dawson, Paré, and Pronk [14, §6] to represent 2-cells in $\Pi_2(\mathcal{C})$ for the special case that $\mathcal{C}$ is a free category. More generally, when $\mathcal{C}$ is not free we also need to include vertices representing equations
in the base category. For example, an equation $h = fg$ that is applied implicitly within a sequent proof, as depicted on the left side of Figure 1, may be represented by a trivalent vertex in the corresponding string diagrammatic proof, as depicted on the right side of that figure. As also depicted there, we also need to include terminating vertices corresponding to the initial axioms in $\mathcal{D}$.

The graphical calculus that we thus obtain is comparable to the string diagram calculus for proarrow equipments of David Jaz Myers [43].

Given the isomorphisms between the three different ways of representing arrows of free bifibrations—as sequent calculus proofs, as stacks of double cells, or as string diagrams—in the sequel we will freely interweave them without comment.

**2.7. Related work.** Since $\mathcal{Bif}(p)$ and $\Pi_2(\mathcal{C})$ are determined by their universal properties, a detailed comparison with the constructions of Dawson, Paré, and Pronk (DPP) [14] and of Lamarche [32] feels a bit superfluous, and the reader interested in the details of those constructions is referred to those papers. Still, a few points are worth highlighting. Zigzags and morphisms between them are essential in all three constructions, but whereas Lamarche (like us) considers zigzags as not necessarily alternating sequences of signed arrows, DPP restrict to strictly alternating zigzags beginning and ending with a forward arrow. This is motivated by the fact that they wanted the embedding of $\mathcal{C}$ into $\Pi_2(\mathcal{C})$ to define a strict functor $(-)^+ : \mathcal{C} \to \Pi_2(\mathcal{C})$ rather than a pseudofunctor. Although the free bifibration is not split and hence $(-)^+ : \mathcal{C} \to \mathcal{V}(\mathbb{Z}(\mathcal{C}))$ defines a proper pseudofunctor, we will also have motivations to consider strictly alternating zigzags beginning in Section 3.3.

All three constructions likewise involve first introducing some notion of “pre-morphism” between zigzags and then defining zigzag morphisms as equivalence classes of pre-morphisms modulo an equivalence relation. Lamarche notes that “these classes can be quite complex, and there is no hope of finding normal forms in general” [32, p.16]. In the next section we will establish that it is possible to obtain normal forms in the case that the base category is factorization preordered, a condition that was also identified by DPP as a sufficient condition for decidability.

Interestingly, categories and double categories of zigzags have also been introduced in other contexts. A category of zigzags and zigzag morphisms was defined by Heidemann, Reutter, and Vicary [22] motivated by the formalization of higher-dimensional diagrams and *n*-categories. Their definition of zigzag map [22, Def. 2.2] is nearly identical to DPP's definition of *fence* [14, Def. 1.2], without condition (c) which enforces globularity. However, Heidemann, Reutter, and Vicary do not quotient zigzag maps by permutation equivalence. Hence their zigzag category is *not* equivalent to $\mathcal{Z}(\mathcal{C})$, but rather to Lamarche's category $\mathcal{Re}(\mathcal{C})$, from which $\mathcal{P}(\mathcal{C}) \simeq \mathcal{Z}(\mathcal{C})$ is obtained as the quotient by permutation equivalence. Our zigzag double category $\mathbb{Z}(\mathcal{C})$ is equivalent to the “weave double category” by Williams [55, Def. 22], as follows from Williams’ definition as a fibered coproduct of arrow and oparrow double categories, which freely add companions and conjoints respectively. As mentioned, Lamarche first identified the double category structure on $\mathcal{P}(\mathcal{C}) \simeq \mathcal{Z}(\mathcal{C})$, although it was not emphasized in his papers [32, 33].<fnref n="2" /> An alternative double categorical perspective on

<footnote n="2">²According to personal communication from François Lamarche (November 2025), he noticed the close connection between this double category and the 2-category $\Pi_2(\mathcal{C})$, discussing it in October 2013 by email with Paré, Dawson, and Pronk. Although the originally submitted version of the manuscript [32] did not mention DPP's work, Lamarche says that this was an oversight and that he had originally intended to include</footnote>
the $\Pi_2(\mathcal{C})$ construction was also developed by DPP at the end of their paper on the Span construction [16].

Perhaps one of the most interesting open questions in double category theory is an explicit construction that freely adds companions and conjoints to a double category $\mathcal{D}$. For each category $\mathcal{C}$, there is a double category $\mathbb{H}(\mathcal{C})$ whose objects and tight morphisms are the objects and morphism of $\mathcal{C}$, and whose loose morphisms and cells are identities. In Theorem 2.8, we established $\mathbb{Z}(\mathcal{C})$ as the free companion and conjoint completion of the double category $\mathcal{D} = \mathbb{H}(\mathcal{C})$. The free cornering of a strict monoidal category, introduced by Nester [44] (see also Section 1 of [9]) is another example of a free companion and conjoint completion, in this case, of a strict monoidal category viewed as a double category. Coulembier, Street, and van den Bergh likewise considered the closely related problem of freely adjoining duals to specified objects of a monoidal category [13]

### 3. FOCUSED NORMAL FORMS

In Section 1, we described how to construct $\mathcal{Bif}(p)$, the total category of the free bifibration on a functor $p: \mathcal{D} \to \mathcal{C}$, by taking its arrows to be equivalence classes of derivations in a sequent calculus modulo a notion of permutation equivalence, with composition defined by the admissible cut rule. In this section we will use additional ideas from proof theory—in particular the notion of *focusing* originating in the proof theory of linear logic—to get a more precise characterization of the relative homsets $\mathcal{Bif}(p)_f(S, T)$, via a series of sequent calculi with progressively more rigid structure. In the case that $\mathcal{C}$ is *factorization preordered* in the sense of Johnstone [25], we derive a normal form theorem that leads to a complete inductive characterization of these relative homsets, without any quotienting. As a corollary, we obtain a simple procedure for deciding permutation equivalence of derivations, as well as for enumerating relative homsets without duplicates.

Lurking in the background is the fact that in the general case, permutation equivalence is undecidable. Dawson, Paré, and Pronk [15] established an analogue of this undecidability result for their freely adjoining adjoints construction $\Pi_2(\mathcal{C})$, and their proof translates readily to our presentation of the zigzag double category $\mathbb{Z}(\mathcal{C})$. Nevertheless, we will see in Sections 4 and 5 that the canonicity result has wide applications.

#### 3.1. Background: invertibility, polarity, and synthetic connectives.

Focusing, introduced by Andreoli [2] as an optimization for linear logic proof search and subsequently applied in other settings, combines several observations about the rules of sequent calculus and the way that they determine the behavior of the connectives. To provide some context and motivation for our approach, we take a moment here to briefly recall these observations in the setting of linear logic [18], before explaining how to transfer these ideas to analyze free bifibrations.

We consider a fragment of the sequent calculus for intuitionistic linear logic, containing the inference rules for tensor $\otimes$ (also called *multiplicative conjunction*) and internal hom $\to$ (also called *linear implication*):

$$ \frac{A, B, \Gamma \vdash C}{A \otimes B, \Gamma \vdash C} \Leftrightarrow \frac{\Gamma \vdash A \quad \Delta \vdash B}{\Gamma, \Delta \vdash A \otimes B} \Rightrightarrows \frac{\Gamma \vdash A \quad B, \Delta \vdash C}{A \to B, \Gamma, \Delta \vdash C} \Leftrightarrow \frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B} \Rightrightarrows $$

<footnote>a comparison. The manuscript [32] was submitted for publication but unfortunately ran into some negative referee reports and never made it to print.</footnote>
Here the basic judgment $\Gamma \vdash B$ takes a single formula $B$ on the right and a list of formulas $\Gamma = A_1, \dots, A_n$ on the left considered up to reordering, and we write a comma for concatenation of lists. The above inference rules are combined with initial axioms of the form $X \vdash X$ for every atomic formula $X$. Identity derivations for arbitrary formulas as well as the cut rule

$$ \frac{\Gamma \vdash A \quad A, \Delta \vdash B}{A \vdash A} \qquad \text{id}_A \qquad \frac{\Gamma, \Delta \vdash B}{\Gamma, \Delta \vdash B} \text{ cut} $$

are admissible, similarly to how we saw in Section 1.

A basic observation about the inference rules for the logical connectives is that the rules $L \otimes$ and $R \to$ are *invertible* in the proof-theoretic sense, meaning that if the conclusion is derivable then the premise is derivable. Indeed, we can derive inverses of $L \otimes$ and $R \to$ using the admissible cut and identity rules, combined with instances of $R \otimes$ and $L \to$:

$$ \frac{\frac{\begin{array}{c} A \vdash A \\ A, B \vdash A \otimes B \end{array}}{A, B, \Gamma \vdash C} \quad \begin{array}{c} B \vdash B \\ A \otimes B, \Gamma \vdash C \end{array}}{A, B, \Gamma \vdash C} \qquad \frac{\begin{array}{c} A \vdash A \\ A \to B, A \vdash B \end{array}}{\Gamma, A \vdash B} \qquad \frac{\begin{array}{c} B \vdash B \\ A \to B, A \vdash B \end{array}}{\Gamma, A \vdash B} $$

One interest of invertible inference rules is that they may be safely applied as *goal transformers* during proof search. For example, if our goal is to prove a sequent of the form $A \otimes B, \Gamma \vdash C$, we can immediately apply the $L \otimes$ rule and try to prove $A, B, \Gamma \vdash C$, knowing that if there is any proof of the original goal then there is one that goes via $L \otimes$. Moreover, if a goal matches the conclusion of more than one invertible rule, then the order in which these rules are invoked is irrelevant. For example, a goal of the form $A \otimes B, \Gamma \vdash C \to D$ can be transformed into the equivalent goal $A, B, \Gamma, C \vdash D$ by applying the $L \otimes$ and $R \to$ rules in either order.

On the other hand, the rules $R \otimes$ and $L \to$ are not invertible in this sense. Intuitively, this is due to the fact that list concatenation is not an invertible operation, meaning that passing from the conclusion to the premises requires finding an appropriate splitting of the formulas on the left-hand side of the turnstile. As a simple counterexample to invertibility of $R \otimes$, consider the sequent $X \otimes Y \vdash X \otimes Y$. It is derivable, but attempting to prove it using the rule $R \otimes$ produces two unprovable premises—no matter how we decide to distribute the unique formula on the left of the sequent:

$$ \frac{X \otimes Y \vdash X \qquad \begin{array}{c} \cdot \vdash Y \\ X \otimes Y \vdash X \otimes Y \end{array}}{X \otimes Y \vdash X \otimes Y} \qquad \frac{\cdot \vdash X \quad X \otimes Y \vdash Y}{X \otimes Y \vdash X \otimes Y} $$

Focusing originally arose from the idea that proof search could be structured to alternate between an *inversion phase*, during which invertible rules are applied eagerly as goal transformers, and a *focus phase*, during which non-invertible rules are applied to decompose a single formula and its subformulas. It was found that this greatly reduces the overall non-determinism of the sequent calculus, leading to more efficient proof search. Moreover, an interesting duality emerges, with half of the connectives being invertible on the *left* and half being invertible on the *right*.

This left or right bias was referred to as “polarity”—with $\otimes$ being a *positive* connective and $\to$ a *negative* connective—and helped to explain some of the distinctive associativity, distributivity, and non-distributivity properties of linear logic. For example, like tensor, additive disjunction $\oplus$ is also invertible on the left, and distributes through $\otimes$ by the
equivalence $A \otimes (B \oplus C) \equiv (A \otimes B) \oplus (A \otimes C)$. Similarly, additive conjunction & is invertible on the right, like internal hom, and distributes through the codomain of $\to$ by the equivalence $A \to (B \& C) \equiv (A \to B) \& (A \to C)$.

Related to these properties is the possibility of considering certain compositions of the logical connectives as “synthetic connectives” [3]. For example, consider the composite formula $A_1 \to (A_2 \to B)$. By applying the left rule twice and the right rule twice, we can build the following open derivations:

$$ \frac{\Gamma_1 \vdash A_1 \qquad \frac{\Gamma_2 \vdash A_2 \qquad B, \Delta \vdash C}{A_2 \to B, \Gamma_2, \Delta \vdash C} \quad L \to \qquad \frac{\Gamma, A_1, A_2 \vdash B}{\Gamma, A_1 \vdash A_2 \to B} \quad R \to}{A_1 \to (A_2 \to B), \Gamma_1, \Gamma_2, \Delta \vdash C} \quad L \to \qquad \frac{\Gamma, A_1, A_2 \vdash B}{\Gamma \vdash A_1 \to (A_2 \to B)} \quad R \to} $$

If we remove the intermediate steps, then these derivations could be seen as inference rules for a new ternary connective $(A_1, A_2) \to' B$:

$$ \frac{\Gamma_1 \vdash A_1 \qquad \Gamma_2 \vdash A_2 \qquad B, \Delta \vdash C}{(A_1, A_2) \to' B, \Gamma_1, \Gamma_2, \Delta \vdash C} \quad L \to' \qquad \frac{\Gamma, A_1, A_2 \vdash B}{\Gamma \vdash (A_1, A_2) \to' B} \quad R \to' $$

Adding this new connective and these inference rules preserves all the important properties of the sequent calculus, in particular admissibility of identity and cut. On the other hand, not every combination of basic connectives can be viewed as a first-class, synthetic connective. For example, there is no good way to define a right rule for the composite connective $A \to (B_1 \otimes B_2)$, intuitively because after applying the invertible rule $R \to$ to decompose the outer implication, we may need to examine the formula $A$ on the left before applying the non-invertible rule $R \otimes$ to decompose the tensor.

**3.2. Invertibility and polarity in the bifibrational calculus.** Returning to bifibrational logic, we begin by observing that pushforward behaves like a positive connective and pullback like a negative connective, since $f^+$ has an invertible left rule and non-invertible right rule, while $g^-$ has an invertible right rule and non-invertible left rule. We already established the invertibility of $Lf^+$ and $Rg^-$ with Lemma 1.11, in the strong sense that they define bijections between proofs of their premises and proofs of their conclusions up to permutation equivalence. Indeed, for any derivation $\alpha : f^+ S \Longrightarrow_g T$ there is a permutation equivalent derivation ending in the $Lf^+$ rule, namely the one represented by the term $f \setminus_g (f_S \cdot \alpha)$, which is $Lf^+$ applied to the derivation of $S \Longrightarrow_{fg} T$ obtained by cutting $\alpha$ with the cartesian lifting $f_S : S \Longrightarrow_f f^+ S$. Dually, for any derivation $\beta : S \Longrightarrow_f g^- T$ there is a permutation equivalent derivation ending in the $Rg^-$ rule, namely $(\beta \cdot \bar{g}_T) f / \bar{g}$.

To see why the $Rf^+$ rule is *not* invertible in general, consider the free bifibration on the functor depicted below

$$ \begin{array}{ccc} \mathcal{D} & \xrightarrow{\delta} & Y \\ \mathcal{C} \downarrow^p & & \\ & & \\ & & \\ \mathcal{E} & \xrightarrow{e_1} & A \xrightarrow{f} B \end{array} $$

where the base category $\mathcal{C}$ contains two parallel arrows $e_1, e_2$ and a third arrow $f$ such that $e_1 f = e_2 f = h$, and where $\mathcal{D}$ is generated by a single arrow $\delta$ such that $p(\delta) = e_1$. Observe that the sequent $X \Longrightarrow_h f^+ Y$ is derivable by applying $Rf^+$ to the atomic derivation
$\delta : X \implies_{e_1} Y$. Since $h = e_2 f$ is another valid factorization, if the $Rf^+$ rule were invertible then there should also be some derivation of $X \implies_{e_2} Y$. But by conservativity (Prop. 1.23) we can immediately tell that there isn't, contradicting invertibility of $Rf^+$. Dualizing the example establishes non-invertibility of the $Lg^-$ rule. Of course these counterexamples do not preclude the possibility of $Rf^+$ and $Lg^-$ being invertible in specific cases—for example, they will be when $\mathcal{C}$ is a groupoid. Nevertheless, the behavior of the connectives in the general case justifies our adopting the polarity terminology to bifibrational formulas, and from now on we will refer to pushforwards as positive and pullbacks as negative, with atomic formulas having neutral polarity.

Continuing the analogy with linear logic, compositions of like-polarity connectives may be grouped into synthetic connectives, in the sense that $g^+ f^+$ can be represented by $(g \circ f)^+$ and $f^- g^-$ can be represented by $(f g)^-$, corresponding to the pseudofunctoriality laws of a bifibration. We already explained how these laws are witnessed by logical equivalences in the bifibrational calculus (Prop. 1.21). Here we simply point out that, similarly to the linear logic situation discussed in Section 3.1, the inference rules for the synthetic connectives are operationally equivalent to compositions of basic inference rules, in the sense that, for example, by composing the left rules and right rules for pushforward along $f$ and $g$,

$$ \frac{\begin{array}{l} S \underset{fgh}{\implies} T \\ \frac{f^+ S \underset{gh}{\implies} T}{g^+ f^+ S \underset{h}{\implies} T} \end{array}}{L} f^+ \qquad \frac{\begin{array}{l} S' \underset{f'}{\implies} S \\ \frac{S' \underset{f'f}{\implies} f^+ S}{S' \underset{f'fg}{\implies} g^+ f^+ S} \end{array}}{R} f^+ \qquad \frac{\begin{array}{l} S' \underset{f'f}{\implies} S \\ \frac{S' \underset{f'fg}{\implies} (g \circ f)^+ S}{S' \underset{f'fg}{\implies} (g \circ f)^+} \end{array}}{R} g^+ $$

we obtain derivations with identical premises to the rules for the pushforward along $g \circ f$:

$$ \frac{\begin{array}{l} S \underset{fgh}{\implies} T \\ \frac{(g \circ f)^+ S \underset{h}{\implies} T}{L} \end{array}}{R} (g \circ f)^+ $$

A difference with the linear logic situation is that such “synthetic” connectives are already contained in the logic, since we assume pushforward and pullback along arbitrary arrows, and the arrows of a category are closed under composition. On the other hand, in general it is not possible to reduce opposite-polarity composites like $f^+ g^-$ or $g^- f^+$ to a single pushforward or pullback, just like alternating quantifiers $\exists \forall$ or $\forall \exists$ in predicate logic cannot be reduced to a single quantifier in general.

**3.3. Strictly alternating formulas, splittings, and weak focusing.** Motivated by the preceding observations, in this section we introduce a restriction of the sequent calculus in which sequences of invertible rules and sequences of non-invertible rules must be performed all at once, on the left or right, but without (yet) placing any restrictions on their interleavings. This calculus may be said to be “weakly focused”, and will serve as an intermediate point before our introduction of a strongly focused calculus in the next section.

**3.3.1. Strictly alternating formulas.** Before defining the calculus itself, we motivate it logically and categorically by observing that every bifibrational formula is canonically isomorphic to a strictly alternating formula.

**Definition 3.1.** A bifibrational formula is **strictly alternating** if it contains no subformula of the form $g^+ f^+ S$ or $f^- g^- T$.
It is easy to see that by repeatedly applying the equivalences $g^+ f^+ S \equiv (g \circ f)^+ S$ and $f^- g^- T \equiv (f g)^- T$ (Prop. 1.21), any formula $S$ may be normalized to a logically equivalent strictly alternating formula $[S]$. Let us write $\theta_S : S \equiv [S]$ for this family of equivalences, and define a function on derivations

$$ \begin{array}{ccc} [-] & : & (S \underset{f}{\Rightarrow} T) \rightarrow ([S] \underset{f}{\Rightarrow} T) \\ [-] & := & \alpha \quad \mapsto \quad \theta_S^{-1} \cdot \alpha \cdot \theta_T \end{array} $$

which we call the *strictification map*. Observe that by the subformula property (Prop. 1.1), the strictification map transforms any derivation into a derivation involving only strictly alternating formulas, since every subformula of a strictly alternating formula is strictly alternating.

Now let $sa\mathcal{Bif}(p)$ denote the full subcategory of $\mathcal{Bif}(p)$ spanned by the strictly alternating formulas, let $i : sa\mathcal{Bif}(p) \to \mathcal{Bif}(p)$ be the full and faithful inclusion functor, and let us write $\Lambda_p|_{sa} = \Lambda_p \circ i : sa\mathcal{Bif}(p) \to \mathcal{C}$ for the restriction of the domain of the free bifibration to strictly alternating formulas.

**Theorem 3.2.** *Strictification extends to a functor $[-] : \mathcal{Bif}(p) \to sa\mathcal{Bif}(p)$ realizing an equivalence of categories over $\mathcal{C}$:*

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

*Proof.* It is immediate from the definition of the $[-]$ map on derivations that

(1) it respects permutation equivalence (since, by Lemma 1.9, cut does so);

(2) it satisfies the functor laws $[\alpha \cdot \beta] \sim [\alpha] \cdot [\beta]$ and $[\mathrm{id}_S] \sim \mathrm{id}_{[S]}$ (since the derivations $\theta_S$ and $\theta_S^{-1}$ cancel out);

(3) it leaves the underlying objects and arrows in $\mathcal{C}$ unchanged;

(4) it is invariant on derivations in the strictly alternating fragment.

Hence strictification defines a functor $[-] : \mathcal{Bif}(p) \to sa\mathcal{Bif}(p)$ that commutes with the projection functors and such that $[-] \circ i = \mathrm{id}_{sa\mathcal{Bif}(p)}$. Finally, the family of logical equivalences $\theta_S : S \equiv [S]$ realize an isomorphism $i \circ [-] \cong \mathrm{id}_{\mathcal{Bif}(p)}$ that is natural by construction. Indeed, it suffices to show that the square

$$ \begin{array}{ccc} S & \xrightarrow{\alpha} & T \\ \theta_S \downarrow & & \theta_T \downarrow \\ i[S] & \xrightarrow{i[\alpha]} & i[T] \end{array} $$

commutes for every arrow $\alpha : S \to T$ in $\mathcal{Bif}(p)$, which is equivalent to asserting that every derivation $\alpha : S \Rightarrow_f T$ may be factored up to permutation equivalence as

$$ S \underset{f}{\stackrel{\alpha}{\Rightarrow}} T \sim S \stackrel{\theta_S}{\equiv} [S] \stackrel{[\alpha]}{\underset{f}{\Rightarrow}} [T] \stackrel{\theta_T^{-1}}{\equiv} T. \qquad (3.1) $$
This holds by definition of the strictification map $[-]$, as we have

$$ \theta_S \cdot [\alpha] \cdot \theta_T = \theta_S \cdot (\theta_S^{-1} \cdot \alpha \cdot \theta_T^{-1}) \cdot \theta_T \sim \alpha $$

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

**Corollary 3.3.** *The functor $\Lambda_p|_{sa} : sa\mathbf{Bif}(p) \to \mathcal{C}$ is a bifibration.*

**Remark 3.4.** The bifibrational structure of $\Lambda_p|_{sa}$ may be described explicitly, with the pushforward and pullback of strictly alternating formulas in $sa\mathbf{Bif}(p)$ along arrows of $\mathcal{C}$ defined by cases depending on the polarity of the formulas, so as to ensure strict alternation. For instance, the pushforward of a strictly alternating formula $S \subset A$ along an arrow $f : A \to B$ is defined as follows:

* If $S$ is negative or atomic, then the pushforward is given by $f^+ S$ equipped with the “free” cartesian lifting $f_S : S \to f^+ S$.

* If $S$ is positive, i.e., of the form $S = f^+ S'$ for some $S' \subset A'$ and $f' : A' \to A$, then $f^+ S$ is defined as the pushforward along the composite $f^+ S := (f \circ f')^+ S'$, equipped with the cartesian arrow given by composing $f_S : f^+ S' \to f^+ f^+ S'$ with the logical equivalence $f^+ f^+ S' \equiv (f \circ f')^+ S'$.

The pullback is defined symmetrically.

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

**3.3.2. Aside: splitting bifibrations.** It is worth observing that the bifibrational structure on the subcategory of strictly alternating formulas described in Remark 3.4 is *nearly split*: the pushforward and pullback functors preserve composition on the nose, but identity is only preserved up to isomorphism witnessed by the logical equivalences $id^+ U \equiv U$ and $id^- U \equiv U$. Thus the associated pseudofunctor $\mathcal{C} \to \mathrm{Adj}$ representing the bifibration $sa\mathbf{Bif}(p) \to \mathcal{C}$ is not fully strict (it is not “normalized”), although it is a strict functor of semicategories.

It is clear that a split bifibration could be obtained, if desired, by adjusting the construction to deal explicitly with identity arrows. Indeed, it suffices to restrict further to the full subcategory of $\mathbf{Bif}(p)$ spanned by the formulas that strictly alternate along nonidentity arrows, which we denote $nsa\mathbf{Bif}(p)$. The equivalence $\mathbf{Bif}(p) \simeq nsa\mathbf{Bif}(p)$ can be established just like Theorem 3.2, applying the full suite of pseudofunctoriality laws (1.10)–(1.12) to normalize any formula to an equivalent nonidentity strictly alternating formula. The split bifibrational structure on $nsa\mathbf{Bif}(p)$ is then almost identical to what was described for $sa\mathbf{Bif}(p)$ in Remark 3.4, but taking care to never push or pull along an identity arrow. For example, when defining the pushforward of $f^+ S'$ along $f$, if $f \circ f' = \mathrm{id}$ then we choose the pushforward object to be $S'$. We can derive the following as a consequence.

**Theorem 3.5 (cf. [28, Theorem 7.1]).** *Every bifibration is equivalent to a split bifibration.*

*Proof.* Let $q : \mathcal{E} \to \mathcal{C}$ be a bifibration. The free bifibration $\Lambda_q : \mathbf{Bif}(q) \to \mathcal{C}$ is equipped with a canonical morphism of bifibrations $\llbracket - \rrbracket_\mathcal{E} : \mathbf{Bif}(q) \to \mathcal{E}$, which restricts to a functor $nsa\mathbf{Bif}(q) \to \mathcal{E}$. Now consider the *full image* of this functor. This defines a category $\llbracket nsa\mathbf{Bif}(q) \rrbracket_\mathcal{E}$ with same objects as $nsa\mathbf{Bif}(q)$ (that is, whose objects are nonidentity strictly alternating formulas) and whose arrows are given by arbitrary arrows $\llbracket S \rrbracket_\mathcal{E} \to \llbracket T \rrbracket_\mathcal{E}$ in $\mathcal{E}$. Since every object of $\mathcal{E}$ is equal to its interpretation as an atomic formula $\llbracket X \rrbracket_\mathcal{E} = X$, the full and faithful functor $\llbracket nsa\mathbf{Bif}(q) \rrbracket_\mathcal{E} \to \mathcal{E}$ is surjective on objects and hence an equivalence of categories. Finally, the composite $q \circ \llbracket - \rrbracket_\mathcal{E} : \llbracket nsa\mathbf{Bif}(q) \rrbracket_\mathcal{E} \to \mathcal{C}$ may be equipped with the structure of a split bifibration by transferring the structure of the free split bifibration $\Lambda_q|_{nsa} : nsa\mathbf{Bif}(q) \to \mathcal{C}$ along the morphism $\llbracket - \rrbracket_\mathcal{E}$. □

<figure><img src="image_34.png" /></figure>
The above proof is similar to the proof of the analogous fact for fibrations described by Anders Kock [28, Theorem 7.1] as Giraud’s “left adjoint splitting” construction, which is also analyzed (together with the “right adjoint splitting”) by Emmenegger, Mesiti, Rosolini, and Streicher [17].

In the rest of the paper we are not particularly concerned with obtaining fully split bifibrations, and so unless otherwise stated we do not forbid pushing and pulling along identity arrows.

### 3.3.3. A syntax of alternating formulas.
We now introduce a new sequent calculus, whose purpose is to force strict alternation at the level of derivations without restricting the language of formulas. It does this by performing multiple inference steps at once, in one large step, precisely where the $[-]$ translation would force them to be grouped together.

Strictly alternating formulas $[S]$ admit a simple inductive characterization: a formula is strictly alternating just in case it is either atomic $X$, or the pushforward $f^+[N]$ of a non-positive strictly alternating formula, or the pullback $g^-[P]$ of a non-negative strictly alternating formula.

$$ 
\begin{array}{lclcl}
[S] & ::= & [P] & | & [N] \\
[P] & ::= & X & | & f^+[N] \\
[N] & ::= & X & | & g^-[P]
\end{array}
 $$

Here we use “non-positive” and “non-negative” in the expected sense, to mean that $N$ is either atomic or a pullback formula, and $P$ is either atomic or a pushforward formula. Note that our definition of strictly alternating allows for pushing and pulling along identity arrows (cf. §3.3.2).

In fact, any bifibrational formula can be described in a similar alternating way, if instead of pushing or pulling applying a single arrow $f$ or $g$, we push or pull along a sequence $\pi$, where $\pi$ denotes a non-empty sequence of composable arrows $(f_0, \dots, f_n)$. We introduce an explicit strictly-alternating grammar for arbitrary formulas $S_{sa}$, non-positive formulas $N_{sa}$ and non-negative formulas $P_{sa}$.

$$ 
\begin{array}{lclcl}
S_{sa} & ::= & P_{sa} & | & N_{sa} \\
P_{sa} & ::= & X & | & \pi^+ N_{sa} \\
N_{sa} & ::= & X & | & \pi^- P_{sa}
\end{array}
 $$

Formulas described in this way can be interpreted in two different ways, depending on the interpretation of sequences $\pi = (f_0, \dots, f_n)$:

(1) If we interpret $\pi^+$ as an *iterated push* $f_n^+ \cdots f_0^+$, a formula $S_{sa}$ in alternating syntax is interpreted as an arbitrary formula (not strictly alternating) that we denote $[S_{sa}]$.

(2) If we interpret $\pi^+$ as a push along the composite arrow $[\pi] := f_0 \cdots f_n$, a formula $S_{sa}$ is interpreted as a strictly alternating formula that we denote $[S_{sa}]$.

For example if we take $N_{sa} = (f, g)^+ (h, i)^- X$, we have $[N_{sa}] = g^+ f^+ h^- i^- X$ and $[N_{sa}] = (f g)^+ (h i)^- X$. All bifibrational formulas are in the image of $[-]$, all strictly-alternating bifibrational formulas are in the image of $[-]$, and for any $S_{sa}$ we have $[S_{sa}] = [[S_{sa}]]$.

To keep notations lighter, we write $S$ to mean either a bifibrational formula $S$ or its alternating presentation (the unique $S_{sa}$ determined by $[S_{sa}] = S$).
$$ \begin{align*} \pi &::= (f_0, \dots, f_n) \\ \alpha_w &::= \delta \mid \bar{\pi} \cdot \alpha_w \mid \pi \backslash_g \alpha_w \mid \alpha_w \cdot \pi \mid \alpha_w f / \bar{\pi} \end{align*} $$

$$ \frac{\delta : X \to Y \in \mathcal{D} \qquad p(\delta) = f}{\delta : X \underset{f}{\Longrightarrow} Y} \delta $$

$$ \frac{\alpha_w : N \underset{\pi g}{\Longrightarrow} T}{\pi \backslash_g \alpha_w : \pi^+ N \underset{g}{\Longrightarrow} T} L_{\pi^+} $$

$$ \frac{\alpha_w : S \underset{f}{\Longrightarrow} N}{\alpha_w \cdot \pi : S \underset{f \pi}{\Longrightarrow} \pi^+ N} R_{\pi^+} $$

$$ \frac{\alpha_w : P \underset{g}{\Longrightarrow} T}{\bar{\pi} \cdot \alpha_w : \bar{\pi} P \underset{\pi g}{\Longrightarrow} T} L_{\pi^-} $$

$$ \frac{\alpha_w : S \underset{f \pi}{\Longrightarrow} P}{\alpha_w f / \bar{\pi} : S \underset{f}{\Longrightarrow} \bar{\pi} P} R_{\pi^-} $$

<caption>Figure 3: Rules of the weakly focused calculus.</caption>

### 3.3.4. Weak focusing as a syntax of alternating derivations.
We now introduce a weakly focused calculus as a sequent calculus on formulas in the alternating syntax. We present the inference rules in Figure 3 at the same time as a more compact term syntax for derivations, similar to one that we introduced in §1.3.

Just as formulas $S_{sa}$ in alternating syntax admit two natural interpretations, each derivation $\alpha_w : S_{sa} \Longrightarrow_f T_{sa}$ in the weakly focused calculus admits two additional interpretations besides its formal interpretation as a sequence of applications of the above rules:

(1) As a derivation $[\alpha_w] : [S_{sa}] \Longrightarrow_f [T_{sa}]$ in the unrestricted sequent calculus, by expanding the “big-step” rules $L\pi^+$, $R\pi^+$, $L\pi^-$, and $R\pi^-$ appropriately in terms of the “small-step” rules $Lf^+$, $Rf^+$, $Lg^-$, and $Rg^-$. This corresponds to translating $\pi \backslash_g \alpha_w$ to $[\pi \backslash_g \alpha_w] = \pi \backslash_g [\alpha_w]$, where $\pi \backslash_g \alpha$ is defined as the iterated division $f_n \backslash_g \cdots f_0 \backslash_{f_1 \cdots f_n g} \alpha$ translating $\alpha_w \cdot \pi$ to $[\alpha_w \cdot \pi] = [\alpha_w] \cdot \pi$, where $\alpha \cdot \pi$ is defined as $\alpha \cdot f_0 \cdots f_n$, and so on.

(2) As a derivation $[\alpha_w] : [S_{sa}] \Longrightarrow_f [T_{sa}]$ in the strictly alternating fragment of the unrestricted sequent calculus, by interpreting each instance of $L\pi^+$, $R\pi^+$, etc., as a single instance of $Lf^+$, $Rf^+$, etc., on the composite arrow $[\pi] = f_0 \cdots f_n$. This corresponds to translating $\pi \backslash_g \alpha_w$ to a single left division $[\pi \backslash_g \alpha_w] = [\pi] \backslash_g [\alpha_w]$, translating $\alpha_w \cdot \pi$ to a single right multiplication $[\alpha_w \cdot \pi] = [\alpha_w] \cdot [\pi]$, and so on.

When we remain ambiguous about whether $S$ denotes an arbitrary bifibrational formula or its alternating syntax, we can write that for any $\alpha_w : S \Longrightarrow_f T$, we have $[\alpha_w] : S \Longrightarrow_f T$ and $[\alpha_w] : [S] \Longrightarrow_f [T]$.

### 3.3.5. Completeness of weak focusing.
We will use the following properties of iterated divisions and iterated multiplications on unrestricted derivations.

**Lemma 3.6** (Iterated identity). $\pi \setminus (\mathrm{id}_S \cdot \pi) \sim \mathrm{id}_{\pi^+ S}$ and $(\bar{\pi} \cdot \mathrm{id}_T) / \bar{\pi} \sim \mathrm{id}_{\pi^- T}$ for all compatible formulas $S, T$ and sequences of arrows $\pi$.

**Lemma 3.7** (Iterated cut). $(\alpha \cdot \pi) \cdot (\pi \backslash_h \beta) \sim \alpha \cdot \beta$ and $(\alpha_g / \bar{\pi}) \cdot (\bar{\pi} \cdot \beta) \sim \alpha \cdot \beta$ for all compatible derivations $\alpha, \beta$ and sequences of arrows $\pi$.
Proof. Both straightforward by induction on $\pi$. $\square$

We can now give explicit derivations for the equivalences $\theta_S : S \equiv [S]$, by defining for every $S \sqsubseteq A$ a pair of (unrestricted) derivations

$$ \theta_S : S \underset{\mathrm{id}_A}{\Longrightarrow} [S] \qquad \theta_S^{-1} : [S] \underset{\mathrm{id}_A}{\Longrightarrow} S $$

as follows. (We omit the subscript arrow on the division signs below, which is always $\mathrm{id}_A$.)

$$ \theta_{\pi^+ N} = \pi \setminus (\theta_N.[\pi]) \qquad \theta_{\pi^+ N}^{-1} = [\pi] \setminus (\theta_N^{-1} \cdot \pi) $$

$$ \theta_{\pi^- P} = (\overline{[\pi]} \cdot \theta_P) / \bar{\pi} \qquad \theta_{\pi^- P}^{-1} = (\bar{\pi} \cdot \theta_P^{-1}) / \overline{[\pi]} $$

$$ \theta_X = \theta_X^{-1} = \mathrm{id}_X $$

By appealing to Lemmas 3.6 and 3.7, we have:

**Proposition 3.8.** $\theta_S$ and $\theta_S^{-1}$ are inverses up to permutation equivalence.

*Proof.* For example in the case $S = \pi^+ N$ we have:

$$ \begin{align*} \theta_{\pi^+ N} \cdot \theta_{\pi^+ N}^{-1} &= (\pi \setminus (\theta_N.[\pi])) \cdot ([\pi] \setminus (\theta_N^{-1} \cdot \pi)) \\ &\sim \pi \setminus (\theta_N \cdot \theta_N^{-1} \cdot \pi) &\qquad \text{definition of cut} \\ &\sim \pi \setminus (\mathrm{id}_N \cdot \pi) &\qquad \text{induction hypothesis} \\ &\sim \mathrm{id}_{\pi^+ N} &\qquad \text{Lemma 3.6} \end{align*} $$

$$ \begin{align*} \theta_{\pi^+ N}^{-1} \cdot \theta_{\pi^+ N} &= ([\pi] \setminus (\theta_N^{-1} \cdot \pi)) \cdot (\pi \setminus (\theta_N.[\pi])) \\ &\sim [\pi] \setminus (\theta_N^{-1} \cdot \theta_N.[\pi]) &\qquad \text{definition of cut and Lemma 3.7} \\ &\sim [\pi] \setminus (\mathrm{id}_N.[\pi]) &\qquad \text{induction hypothesis} \\ &\sim \mathrm{id}_{[\pi]^+ N} &\qquad \text{definition of identity} \end{align*} $$

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

On formulas we remarked that we have the relation $[S] = [[S]]$. There is a similar relation at the level of derivations.

**Proposition 3.9.** For any $\alpha_w : S \implies_f T$ we have $[\alpha_w] \sim [[\alpha_w]]$.

*Proof.* By induction on the weakly focused derivation $\alpha_w$. For example, in the case that $\alpha_w$ is of the form $\pi \setminus_g \alpha'_w : \pi^+ N \implies_g T$, we have

$$ \begin{align*} [[\pi \setminus_g \alpha'_w]] &= ([\pi] \setminus (\theta_N^{-1} \cdot \pi)) \cdot (\pi \setminus_g [\alpha'_w]) \cdot \theta_T && \text{by definition of $[-]$ and $[-]$} \\ &\sim [\pi] \setminus (\theta_N^{-1} \cdot [\alpha_w] \cdot \theta_T) && \text{definition of cut and Lemma 3.7} \\ &\sim [\pi] \setminus [\alpha_w] && \text{induction hypothesis} \\ &= [\pi \setminus_g \alpha_w] && \text{definition of $[-]$} \end{align*} $$

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

We remarked above that every bifibrational formula is of the form $[S_{sa}]$, and every strictly alternating formula is of the form $[S_{sa}]$, where $S_{sa}$ is a formula in alternating syntax. The situation for derivations is different: all strictly alternating derivations are of the form $[\alpha_w]$, but not all unrestricted derivations are of the form $[\alpha_w]$—it is really a more restricted
syntax. For example, the derivation on the left below is not in the image of [-], but it is
permutation equivalent to the derivation on the right, which is:

$$
\begin{array}{c}
\begin{array}{c}
S \underset{fghi}{\Longrightarrow} T \\
\hline
\frac{f^+ S \underset{ghi}{\Longrightarrow} T}{f^+ S \underset{gh}{\Longrightarrow} i^- T} \quad \mathbf{L} f^+ \\
\hline
\frac{g^+ f^+ S \underset{h}{\Longrightarrow} i^- T}{g^+ f^+ S \underset{h}{\Longrightarrow} i^- T} \quad \mathbf{L} g^+
\end{array}
\end{array}
$$

$$
\begin{array}{c}
\begin{array}{c}
S \underset{fghi}{\Longrightarrow} T \\
\hline
\frac{S \underset{fgh}{\Longrightarrow} i^- T}{f^+ S \underset{gh}{\Longrightarrow} i^- T} \quad \mathbf{L} f^+ \\
\hline
\frac{g^+ f^+ S \underset{h}{\Longrightarrow} i^- T}{g^+ f^+ S \underset{h}{\Longrightarrow} i^- T} \quad \mathbf{L} g^+
\end{array}
\end{array}
$$

**Proposition 3.10.** The mapping $[-]$ is a one-to-one correspondence between weakly focused derivations of $S_{sa} \implies_f T_{sa}$ and unrestricted derivations of strictly alternating sequents $[S_{sa}] \implies_f [T_{sa}]$.

*Proof.* We prove that for any judgment $S_{sa} \implies_f T_{sa}$, if $\alpha$ is an unrestricted derivation of $[S_{sa}] \implies_f [T_{sa}]$, then there exists a *unique* weakly focused derivation $\alpha_w$ such that $\alpha = [\alpha_w]$. The proof proceeds by induction on the product ordering of the two sides of the sequent $(S_{sa}, T_{sa})$ with respect to the subformula ordering. We will have more occasions to use this style of induction in the rest of this section, which we refer to as *induction on judgments*. The associated well-founded ordering on judgments is defined explicitly by

$$
(S' \underset{h'}{\Longrightarrow} T') < (S \underset{h}{\Longrightarrow} T)
$$

just in case $S'$ is a subformula of $S$, $T'$ is a subformula of $T$, and either $S'$ is a strict subformula of $S$ or $T'$ is a strict subformula of $T$. We now proceed to the proof.

If $\alpha$ is an axiom rule then it is already a weakly focused proof.

If $\alpha$ is of the form $f \backslash_g \alpha'$:

$$
\frac{\alpha' : S' \underset{fg}{\Longrightarrow} [T_{sa}]}{f \backslash_g \alpha' : f^+ S' \underset{g}{\Longrightarrow} [T_{sa}]}
$$

then from $f^+ S' = |S|_{sa}$ we can deduce that $S_{sa}$ must be of the form $\pi^+ N$, so $f$ is uniquely
determined to be $[\pi]$ and $S'$ is $[N]$. So in fact the derivation of $\alpha$ is of the form

$$
\frac{\alpha' : [N] \underset{\pi g}{\Longrightarrow} [T_{sa}]}{[\pi] \backslash_g \alpha' : [\pi]^+ [N] \underset{g}{\Longrightarrow} [T_{sa}]}
$$

By induction hypothesis, there exists a unique $\alpha'_w$ such that $\alpha' = [\alpha'_w]$, so $\alpha$ is necessarily equal to $[\pi] \backslash_g [\alpha'_w]$, and $\alpha_w := \pi \backslash_g \alpha'_w$ is uniquely determined.

The reasoning is symmetric when if $\alpha$ is of the form $\bar{f} \cdot \alpha'$.

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

**Corollary 3.11 (Completeness of weak focusing).** For any derivation $\alpha : S \implies_f T$, there is a weakly focused derivation $\alpha_w : S \implies_f T$ such that $\alpha \sim [\alpha_w]$.

*Proof.* Let $[\alpha] : [S] \implies_f [T]$ be the strictification of $\alpha$, and let $\alpha_w : S \implies_f T$ be the unique weakly focused derivation such that $[\alpha] = [\alpha_w]$, which exists by the previous proposition. In particular, $[\alpha]$ and $[[\alpha_w]]$ are equal as $sa\mathcal{B}if(p)$ morphisms, so by Theorem 3.2 we have that $\alpha$ and $[\alpha_w]$ are equal as $\mathcal{B}if(p)$ morphisms, that is, $\alpha \sim [\alpha_w]$.
$\square$

<figure><img src="image_38.png" /></figure>
### 3.3.6. Equivalence of weakly focused proofs.
There are two reasonable notions of equivalence on weakly focused proofs $\alpha_w, \beta_w$:

* One can consider the relation $[\alpha_w] \sim [\beta_w]$, which views $\alpha_w, \beta_w$ as unrestricted derivations and considers permutation equivalence between them. Such a proof of equivalence permutes inference rules one at a time, and in particular it may contain intermediate steps that are not weakly focused derivations.

* One can consider the relation $[\alpha_w] \sim [\beta_w]$, which views $\alpha_w$ and $\beta_w$ as derivations on strictly alternating formulas. Such proofs of equivalence respect the strictly-alternating structure in the sense that they cannot break sequences of pushes or sequence of pulls apart. They can be seen as permutation equivalences on “synthetic” connectives.

**Corollary 3.12.** *These two notions of equivalence coincide.*

*Proof.*

$$ [\alpha_w] \sim [\beta_w] \quad \text{Proposition 3.9} \quad [[\alpha_w]] \sim [[\beta_w]] \quad \text{Theorem 3.2} \quad [\alpha_w] \sim [\beta_w] \quad \Box $$

### 3.3.7. Presentation.
The results of this section can be reformulated as an alternative presentation of the arrows of Bif($p$) as triples $(S, \hat{\alpha}_w, T)$, where $\hat{\alpha}_w \in \text{saBif}(p)(S, T)$ is a permutation-equivalence class of weakly focused derivations $\alpha_w : S \Longrightarrow_f T$. Weak focusing removes some of the inessential non-determinism of the sequent calculus, but it is possible to go further and obtain a still more canonical presentation, as we will now examine.

## 3.4. Multifocusing.

### 3.4.1. Introduction.
The previous calculus was only “weakly” focused in the sense that it allows applying non-invertible rules to derive a judgment even where an invertible rule is applicable. It would be more canonical to enforce that invertible rules are applied eagerly. For instance, if we have a positive formula on the left then we can always apply an invertible left rule, and if we have a negative formula on the right then we can always apply an invertible right rule. In the case of a sequent of the form $\pi^+ N \Longrightarrow_f \rho^-$ $P$ with both a positive formula on the left and a negative formula, it seems we have a useless choice to make of whether to work on the left or right first:

$$ \frac{N \underset{\pi^+ N \underset{f \rho^-}{\Longrightarrow} \rho^- P}{\Longrightarrow} P}{\pi^+ N \underset{f \rho^-}{\Longrightarrow} P} \L_{\pi^+} \qquad \frac{N \underset{\pi^+ N \underset{f \rho^-}{\Longrightarrow} \rho^- P}{\Longrightarrow} P}{\pi^+ N \underset{f \rho^-}{\Longrightarrow} P} \R_{\rho^-} $$

The choice of whether to apply $\mathbb{R}\pi^-$ or $\mathbb{L}\rho^+$ first is irrelevant, since the two derivations above are permutation equivalent. However, a natural way of addressing this issue is to add a rule that can perform both left and right inversion at once. By combining such a bi-inversion rule with polarity-restricted instances of the left- and right-inversion rules,

$$ \frac{N \underset{\pi^+ N \underset{f \rho^-}{\Longrightarrow} P}{\Longrightarrow} P}{\pi^+ N \underset{f \rho^-}{\Longrightarrow} P} \L_{\pi^+} \qquad \frac{N \underset{\pi^+ N \underset{f \rho^-}{\Longrightarrow} \rho^- P}{\Longrightarrow} P}{\pi^+ N \underset{f \rho^-}{\Longrightarrow} P} \R_{\rho^-} \qquad (3.2) $$
$$ \alpha_m ::= \begin{array}{c} \delta \\ | \bar{\sigma} \cdot \alpha_m | \alpha_m \cdot \tau | \bar{\sigma} \cdot \alpha_m \cdot \tau \\ | \pi \backslash_g \alpha_m | \alpha_m \backslash_g \bar{\rho} | \pi \backslash \alpha_m \backslash \bar{\rho} \end{array} $$

$$ \frac{\delta : X \to Y \in \mathcal{D} \quad p(\delta) = f}{\delta : X \underset{f}{\Rightarrow} Y} $$

$$ \frac{\alpha_m : N \underset{\pi f}{\Rightarrow} P}{\pi \backslash f \alpha_m : \pi^+ N \underset{f}{\Rightarrow} P} L \pi^+ \frac{\alpha_m : N \underset{\pi f \rho}{\Rightarrow} P}{\pi \backslash \alpha_m / \bar{\rho} : \pi^+ N \underset{f}{\Rightarrow} \bar{\rho}^- P} L \pi^+ R \bar{\rho}^- $$

$$ \frac{\alpha_m : P \underset{f}{\Rightarrow} Q}{\bar{\sigma} \cdot \alpha_m : \sigma^- P \underset{\sigma f}{\Rightarrow} Q} L \sigma^- \frac{\alpha_m : P \underset{f}{\Rightarrow} N}{\bar{\sigma} \cdot \alpha_m \cdot \tau : \sigma^- P \underset{\sigma f \tau}{\Rightarrow} \tau^+ N} L \sigma^- R \tau^+ \frac{\alpha_m : N \underset{f}{\Rightarrow} M}{\alpha_m \cdot \tau : N \underset{f \tau}{\Rightarrow} \tau^+ M} R \tau^+ $$

<caption>Figure 4: Rules of the strongly multifocused calculus.</caption>

we can enforce that non-invertible rules are only used on polarized sequents of the form $N \Rightarrow_f P$, with a uniquely determined invertible rule applicable in all other cases. We say that such a system, with a polarity restriction on non-invertible phases, is *strongly focused*.

Once we arrive at a sequent of the form $N \Rightarrow_f P$ we have to make a potentially significant choice as to whether to try applying a non-invertible rule on the left or right first. However, here a similar phenomenon arises in considering permutable applications of non-invertible rules. Again it is natural to introduce a rule that allows to perform two non-invertible rules in parallel, written in the middle below:

$$ \frac{P \underset{\sigma^-}{\Rightarrow} f Q}{\sigma^- P \underset{\sigma f}{\Rightarrow} Q} L \sigma^- \frac{P \underset{\sigma^-}{\Rightarrow} f N}{\sigma^- P \underset{\sigma f \tau}{\Rightarrow} \tau^+ N} L \sigma^- R \tau^+ \frac{N \underset{\sigma f}{\Rightarrow} f M}{N \underset{\sigma f \tau}{\Rightarrow} \tau^+ M} R \tau^+ \quad (3.3) $$

The collection of six polarized rules (3.2) and (3.3), together with the ordinary axiom rule, together define a system that we call *strongly multifocused*.

Strong focusing and multi-focusing are standard notions from the literature [12, 51]. Going from a weakly-focused to a strongly-focused system (enforcing that invertible rules are applied eagerly) makes the system more canonical. On the other hand, introducing multifocusing (the bi-focusing rule $L\sigma^-R\tau^+$ in our case) does not automatically make the system more canonical, since it actually allows more proofs: every time a bi-focused rule is used, it is also possible to use two mono-focused rules in sequence. In Section 3.6 below, we will explain how to restrict this system by limiting the usage of mono-focused rules, resulting in a calculus that is canonical under an assumption on the base category.

In Figure 4 we recapitulate the rules of the strongly multifocused system while introducing a term syntax.

### 3.4.2. Neutral sequents, bipoles.
Following the focusing tradition, we call *neutral* a sequent of the form $N \Rightarrow_f P$. A proof of a (non-atomic) neutral sequent has to start with a focusing step, either on the left, right or both sides of the sequent.
Following the same tradition, we call *bipole* a two-step (open) derivation of a neutral sequent beginning with a focusing step followed by an inversion step. We use the notation $L$ for a bipole of $L^+ L^-$ rules, $R$ for a bipole of $R^- R^+$ rules, and $LR$ for a bi-focused bipole $(L^+ R^-) (L^- R^+)$. In order to avoid having to treat atomic formulas as a special case, we will expand the interpretation of the $L\pi^+, R\rho^-$, and $L\pi^+ R\rho^-$ rules by allowing $\pi$ (respectively, $\rho$) to be empty when the left (respectively right) side of the sequent is atomic. With that convention, every strongly focused proof of a neutral sequent decomposes as a sequence of $L / R / LR$ bipoles ended by an axiom.

### 3.4.3. Sequentialization equivalence of strongly multi-focused proofs.
The permutation equivalence that we introduced in Section 1.5 and extended to weakly focused proofs is not directly applicable for strongly focused proofs. Indeed, permutation equivalence breaks the polarity invariants that we described above. However, there is a natural notion of equivalence for strongly multifocused derivations that arises from considering both possible sequentializations of a $LR$ bipole:

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

Or equivalently in stack-and-string diagrammatic form:

<figure><img src="image_40.png" /></figure>
Or equivalently again in proof term syntax:

$$ \bar{\sigma}.(\pi \setminus_{f\tau} ((\beta_{\pi f}/\bar{\rho}).\tau)) \leftarrow_{\text{seq}_L^R} \bar{\sigma}.(\pi \setminus \beta/f/\bar{\rho}).\tau \longrightarrow_{\text{seq}_R^L} ((\bar{\sigma}.(\pi \setminus_{f\rho} \beta)).\sigma_f/\bar{\rho}).\tau \quad (3.4) $$

Recall that we allow $\pi$ and $\rho$ to be empty, $\pi = \epsilon$ or $\rho = \epsilon$ (in which case, e.g., $\epsilon \setminus \alpha = \alpha$).

Let us write ($\rightarrow_{\text{seq}}$) for this sequentialization order, and ($\sim_{\text{seq}}$) for the corresponding equivalence relation.

### 3.4.4. Relating the weak-monofocused and strong-multifocused systems.

The ($\rightarrow_{\text{seq}}$)-normal forms of this relation are the strongly monofocused proofs—in other words proofs that do not use the bi-focusing rule, although they can use bi-inversion. Such proofs can then be turned into derivations in the weakly focused calculus by selecting an ordering for each bi-inversion rule. We define $\text{Seq}(\alpha_m)$ as the set of weakly monofocused sequentializations of a strongly multifocused proof $\alpha_m$.

**Proposition 3.13.** If $\alpha_m \sim_{\text{seq}} \alpha'_m$ then for all $\alpha_w \in \text{Seq}(\alpha_m)$ and $\alpha'_w \in \text{Seq}(\alpha'_m)$ we have $\alpha_w \sim \alpha'_w$.

*Proof.* The idea of the proof is that for any non-deterministic choice in the sequentialization process, the two choices will sequentialize into permutation-equivalent derivations.

The first choice comes from the definition of the sequentialization order between multifocused proofs. For each $\alpha$ with two direct sequentializations $\alpha_1, \alpha_2$ as depicted in (3.4) above, we have that $\text{Seq}(\alpha) = \text{Seq}(\alpha_1) \oplus \text{Seq}(\alpha_2)$, and we prove that for any $\alpha_{1w} \in \text{Seq}(\alpha_1)$ and $\alpha_{2w} \in \text{Seq}(\alpha_2)$ we have $\alpha_{1w} \sim \alpha_{2w}$. Indeed, the two sequentializations sets are

$$ \text{Seq}(\alpha_1) = \{ \bar{\sigma}.(\pi \setminus ((\beta_w f/\bar{\rho}).\tau)) \mid \beta_w \in \text{Seq}(\beta) \} $$

$$ \text{Seq}(\alpha_2) = \{ ((\bar{\sigma}.(\pi \setminus_f \beta_w)) / \bar{\rho}).\tau \mid \beta_w \in \text{Seq}(\beta) \} $$

and for any $\beta_w \in \text{Seq}(\beta)$, we do have as expected:

$$ \begin{align*} & \bar{\sigma}.(\pi \setminus ((\beta_w f/\bar{\rho}).\tau)) \\ & \sim \bar{\sigma}.((\pi \setminus (\beta_w f/\bar{\rho})).\tau) \\ & \sim (\bar{\sigma}.(\pi \setminus (\beta_w f/\bar{\rho}))).\tau \\ & \sim (\bar{\sigma}.((\pi \setminus_f \beta_w) / \bar{\rho})).\tau \\ & \sim ((\bar{\sigma}.(\pi \setminus_f \beta_w)) / \bar{\rho}).\tau \end{align*} $$

The second choice is in the ordering of inversion rules when sequentializing bi-inversion rules, and the two choices are immediately permutation-equivalent. $\square$

**Corollary 3.14.** All elements of $\text{Seq}(\alpha_m)$ are permutation-equivalent: for any $\alpha_m$ we have $\alpha_m \sim_{\text{seq}} \alpha_m$, so $\alpha_w \in \text{Seq}(\alpha_m)$ and $\alpha'_w \in \text{Seq}(\alpha_m)$ imply $\alpha_w \sim \alpha'_w$.

Conversely, given a weakly focused derivation $\alpha_w : S \implies_h T$, let us write $S(\alpha_w)$ for the strengthening of $\alpha_w$, a uniquely-determined strongly (mono-)focused proof defined as follows, by induction on judgments:

$$ S(\alpha : \pi^+ N \implies_f \bar{\rho}^- P) := \pi \setminus S(\pi_N \cdot \alpha \cdot \bar{\rho}_P : N \implies_{\pi f \rho} P) / \bar{\rho} $$

$$ S((\bar{\sigma}.\alpha) : \sigma^- P \implies_{\sigma f} Q) := \bar{\sigma} \cdot S(\alpha : P \implies_f Q) $$

$$ S((\alpha.\tau) : N \implies_{f\tau} \tau^+ M) := S(\alpha : N \implies_f M).\tau $$

$$ S(\delta : X \implies_f Y) := \delta $$

In other words, to strengthen $\alpha_w$, whenever we encounter a judgment that admits invertible steps, we do them (both at the same time if applicable), and otherwise we imitate the non-invertible steps.
This strengthening transformation defines a mapping from weakly focused derivations to strongly focused derivations of the same judgment. We now establish that it sends permutation equivalent weakly focused derivations to sequentially equivalent strongly focused derivations.

**Proposition 3.15.** If $\alpha_w \sim \alpha'_w$ then $S(\alpha_w) \sim_{\text{seq}} S(\alpha'_w)$.

*Proof.* By induction on the underlying judgment derived by both derivations $\alpha_w \sim \alpha'_w$. There are two cases to consider, depending on whether or not the judgment is invertible.

* Case $\pi^+ N \implies_f \rho^- P$. (Recall we allow $\pi = \epsilon$ or $\rho = \epsilon$.) We have

$$S(\alpha_w) = \pi \setminus S(\pi_N \cdot \alpha_w \cdot \bar{\rho}_P) / \bar{\rho} \sim_{\text{seq}} \pi \setminus S(\pi_N \cdot \alpha'_w \cdot \bar{\rho}_P) / \bar{\rho} = S(\alpha'_w)$$

where the first and last steps are by definition and the middle step is by induction on $\pi_N \cdot \alpha_w \cdot \bar{\rho}_P \sim \pi_N \cdot \alpha'_w \cdot \bar{\rho}_P$ at the smaller judgment $N \implies_{\pi f \rho} P$.

* Case $N \implies_h P$. We consider the derivation of the permutation equivalence $\alpha_w \sim \alpha'_w$.

- Subcase $\alpha_w \sim \alpha'_w$ is derived by the generator (1.2), with $\alpha_w = (\bar{f} \cdot \beta) \cdot h$ and $\alpha'_w = \bar{f} \cdot (\beta \cdot h)$. In this case the two strengthenings are sequentializations of the same bi-focused derivation $\bar{f} \cdot S(\beta) \cdot h$.

- Subcase $\alpha_w \sim \alpha'_w$ is derived by a generator (1.3)-(1.5): impossible at the judgment $N \implies_h P$.

- Subcase $\alpha_w = \bar{f} \cdot \beta$ and $\alpha'_w = \bar{f} \cdot \beta'$ for some $\beta \sim \beta'$: $Q \implies_{fh} P$ where $N = f^- Q$. Then $S(\beta) \sim_{\text{seq}} S(\beta')$ by induction and so $S(\alpha_w) = \bar{f} \cdot S(\beta) \sim_{\text{seq}} \bar{f} \cdot S(\beta') = S(\alpha'_w)$.

- Subcase $\alpha_w = \beta \cdot g$ and $\alpha'_w = \beta' \cdot g$ for some $\beta \sim \beta'$: $N \implies_{hg} M$ where $P = g^+ M$: same as above.

□

The relation between permutation equivalence and sequentialization equivalence is captured by the following diagram:

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

where we have factored sequentialization $\text{Seq}(-)$ in two different nondeterministic / multivalued functions: $\text{FocSeq}(\alpha_m)$ is the sequentialization of the bi-focused rules of a multifocused proof, and $\text{InvSeq}(\alpha_m)$ is the sequentialization of the bi-invertible rules of a strongly mono-focused proof. This diagram expresses two equivalences of setoids (sets equipped with an equivalence relation), in the following sense:

(1) $S$ is a morphism of setoids, per Proposition 3.15. (This gives us completeness and relational completeness of strongly focused proof with respect to weakly focused proofs).

(2) $\text{InvSeq}$ and $\text{FocSeq}$ are nondeterministic morphisms of setoids, per Proposition 3.13.

(3) The equivalence on the right corresponds to the following statement:

$$\alpha_m \sim \text{FocSeq}(\alpha_m) \\ \forall \alpha'_m \in \text{FocSeq}(\alpha_m), \alpha'_m \sim_{\text{seq}} \alpha_m$$

It is immediate from the fact that $\text{FocSeq}(\alpha_m)$ is defined as the set of $(\to_{\text{seq}})$-normal forms of $\alpha_m$, and $(\sim_{\text{seq}})$ as the least congruence containing $(\to_{\text{seq}})$.
(4) The equivalence on the left corresponds to the following statements:

**Proposition 3.16.**

$$ \begin{array}{l} \forall \alpha_w, \quad \alpha_w \sim \mathrm{InvSeq}(S(\alpha_w)) \\ \forall \alpha_w, \forall \alpha'_w \in \mathrm{InvSeq}(S(\alpha_w)), \quad \alpha_w \sim \alpha'_w \end{array} $$

**Proposition 3.17.**

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

For each property, on the first line we wrote the statement with $InvSeq$ seen as a multi-valued function nondeterministically returning a weakly focused proof, and on the second line we wrote it with $InvSeq$ seen directly as a function into sets of weakly focused proofs. Both statements can be established by induction on derivations; we detail the proofs in Appendix A.2.

The intermediate system **StrongMono** is useful to describe the fine-grained properties of strengthening and sequentialization, but note that the equivalence relation ($\sim_{\mathrm{seq}}$) has no natural definition that is internal to **StrongMono**, since the source derivation $\alpha_m$ of a sequentialization step $\alpha_m \to_{\mathrm{seq}} \alpha'_m$ uses a bi-focused rule.

### 3.4.5. Horizontal composition (cut) of strongly multi-focused proofs.
Now that we have defined strengthening, sequentialization and their properties, we can easily define horizontal composition (cut) of strongly multifocused proofs modulo permutation equivalence: $\alpha_m \cdot \beta_m$ can be defined as $S(\alpha_w \cdot \beta_w)$ for some $\alpha_w \in \mathrm{Seq}(\alpha_m)$, $\beta_w \in \mathrm{Seq}(\beta_m)$. The choice of $\alpha_w$ and $\beta_w$ is irrelevant: they are all permutation equivalent, so the resulting strengthening is unique modulo sequentialization equivalence. This definition is easily seen to be associative (lifted from the associativity of composition of non-focused proofs) and unital—for identity derivations defined as the $S(id_A)$. Finally, we also directly get that $S(-)$ respects composition and preserves identity derivations.

We can thus define a category of strongly multifocused derivations quotiented by ($\sim_{\mathrm{seq}}$), with $S(-)$ a functor from $\mathcal{Bif}(p)$. But this category is just $\mathcal{Bif}(p)$ itself, given that our equivalence of setoids gives an equality of quotiented sets.

It is also possible to define cut directly on strongly multifocused derivations. We detail this construction in Appendix B.

### 3.5. Normal forms via rewriting.
In this section we introduce a strongly normalizing rewriting relation between multifocused proofs that, under a certain condition on the base category, is locally confluent and thus admits unique normal forms: all proofs in each sequentialization equivalence class eventually reduce to the same normal form.

An intuition is that these normal forms will be “maximally parallel”, in the sense that $L$ and $R$ bipoles should be combined into an $LR$ bipole whenever possible. We therefore begin by considering the *parallelization* order ($\to_{\mathrm{par}}$), which is just the opposite of the sequentialization order ($\alpha \to_{\mathrm{par}} \beta$ iff $\beta \to_{\mathrm{seq}} \alpha$). Diagrammatically it is defined by the pair of rules $\mathrm{par}_L^R$ and $\mathrm{par}_R^L$ shown below:
if both $fg = fh$ and $gk = hk$ then necessarily $g = h$. Equivalently, $\mathcal{C}$ is factorization
preordered just in case every commuting square has at most one diagonal filler:

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

Equivalently again, $\mathcal{C}$ is factorization preordered just in case the category of factorizations of every arrow is a preorder, where the category of factorizations of an arrow $w : A \to B$ has objects given by composable pairs of arrows $A \xrightarrow{u} X \xrightarrow{v} B$ such that $w = uv$, and morphisms $(A \xrightarrow{u} X \xrightarrow{v} B) \to (A \xrightarrow{s} Y \xrightarrow{t} B)$ given by arrows $h : X \to Y$ such that $uh = s$ and $ht = v$.

**Example 3.19.** Any category that has only monic arrows or only epic arrows is factorization preordered. In particular, every preorder category is factorization preordered, as is every free category.

Let us call “FP condition” the hypothesis that the base category $\mathcal{C}$ of the free bifibration $\Lambda_p : \mathcal{Bif}(p) \to \mathcal{C}$ is factorization preordered.

**Proposition 3.20.** *Under the FP condition, the parallelization rules $\mathrm{par}_L^\mathbb{R}$ and $\mathrm{par}_R^\mathbb{L}$ are deterministic, and the sequentialization rules $\mathrm{seq}_L^\mathbb{R}$ and $\mathrm{seq}_R^\mathbb{L}$ are co-deterministic.*

Determinism is a special case of confluence, ensuring that a single application of a rule does not induce a critical pair with itself. On the other hand, general confluence fails for the parallelization order, as one can exhibit a divergent critical pair from a stack of three bipoles. For example, there is a critical pair whose apex is a stack of bipoles $L \amalg R \amalg L'$,

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

as well as a symmetric critical pair whose apex is a stack of bipoles $R \amalg L \amalg R'$. Here we clarify
that the condition that $bf = b'g$ is necessary for the well-formedness of the stack in the middle
L R L which is exactly the critical pair (3.6) which is resolved by the rule gra<sub>L</sub>, and one with three bipoles LRLR involving the rules gra<sub>L</sub> on one side and par<sub>R</sub><sup>L</sup> on the other, which is resolved by applying par<sub>R</sub><sup>L</sup> on one side and gra<sub>R</sub> on the other (see Figure 5). ☐

**Lemma 3.22.** *par* ∪ *gra* is terminating: any valid rewriting sequence is finite.

*Proof.* We provide a non-negative measure for derivations that par ∪ gra decreases strictly.

We measure each derivation by summing the weight of all bipoles. If a bipole is at position *i* starting from the bottom, the root of the derivation, we define its weight as *i* if it is a L or R bipole, and 2 × *i* if it is a LR bipole: the weight of LR is the weight of L plus the weight of R.

Consider a *gra* rewrite (*gra*<sub>*L*</sub> for example), which is of the following shape annotated with vertical positions:

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

The starting positions of the sub-stacks $\alpha$ and $\beta$ do not matter in this rewrite as their weight is unchanged. The weight of the middle of the derivation decreases strictly from $2 \times (i+1) + i$ to $(i+1) + 2 \times i$.

Consider a *par* rewrite (*par*<sub>*R*</sub><sup>*L*</sup> for example), it is of the shape

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

The weight of $\alpha$ is unchanged by the rewrite. The combined weight of the L and R bipoles decreases from $i + (i+1)$ to $2 \times i$. The weight of $\beta$ also decreases strictly as all its bipoles are shifted one position down. ☐

From local confluence and termination, we derive our main canonicity theorem.

**Theorem 3.23.** Under the FP condition, any multifocused derivation $\alpha_m$ admits a unique normal form for par ∪ gra, which we write NF($\alpha_m$). Moreover, for any pair of derivations $\alpha_m$ and $\beta_m$ we have

$$ \alpha_m \sim_{\text{seq}} \beta_m \iff \text{NF}(\alpha_m) = \text{NF}(\beta_m). $$

**3.6. Maximal multifocusing.** We finally introduce a restriction of the multifocused sequent calculus that precisely captures the normal forms for par ∪ gra. Under the FP condition, proofs in this restricted calculus give canonical representatives for the arrows of Bif(*p*).

An intuition is that, when building the proof from the root to the axioms, we only need information about the last invertible rule that was applied to conclude a bipole. In the immediately following bipole, we can use this information to check that the non-invertible rule does not introduce a par or gra redex.

Suppose for example that the last invertible rule was $L\pi^+$ as part of a L bipole with intermediate base arrow *f*, and suppose that—assuming $\pi * f$ is of the form $g\tau$ for some $g$—we want to continue the proof by applying $R\tau^+$ as part of a R bipole, as depicted on the left:
<figure><img src="image_46.png" /></figure>

This creates a parL redex exactly when there is an arrow $h$ such that $g = \pi h$ and $f = h\tau$, that is when the square to the right has a diagonal filler, corresponding to a morphism $h : (\pi, f) \to (g, \tau)$ in the category of factorizations of the composite arrow $\pi f = g\tau$.

If instead we try to extend the $L$ bipole with a $LR$ bipole, we should check that we don't create a gra redex. Such an extension takes the shape on the left:

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

This forms a gra redex exactly when $f$ is of the form $h\tau$ for some $h$ such that $\pi h = \sigma g$, that is when the square to the right has a diagonal filler corresponding to a morphism $h : (\pi, f) \to (\sigma g, \tau)$ in the category of factorizations of the composite arrow $\pi f = \sigma g\tau$.

Notice that in both cases, in order to decide whether or not there is a redex we need to know the intermediate arrow $f$ of the $L$ bipole. By keeping track of the last rule applied as well as the intermediate arrow, we can thus rule out the creation of any par or gra redexes.

In Figure 6 we present a refinement of the multifocused sequent calculus that we call maximally multifocused, in which judgments $S \Longrightarrow_f^q T$ are annotated with a state $q$ that can be either a pre-inversion state $q = q_i$ or a pre-focus state $q = q_f$. The rules are best read operationally as goal transformers from conclusion to premise, following the conventions of proof search. The idea is that a pre-inversion state forces an inversion rule to be applied in the next step (recall that we allow $\pi$ and $\rho$ to be empty), while a pre-focus state forces one of the focusing rules or an atomic rule to be applied. After applying a focusing rule, the state transitions to a pre-inversion state of the form $L$, $R$, or $\perp_i$, indicating the start of a $L-$, $R-$, or $LR$-bipole respectively. The subsequent inversion rule supplements the state with additional information about the arrows involved, which is then used at the start of the next bipole to rule out any par or gra redexes: this is done with the side conditions for the focusing rules, which are indicated to the side in a smaller font in Figure 6.
$$
\begin{array}{l@{\hspace{1em}}c@{\hspace{1em}}l}
\text{pre-inversion states} & q_i & ::= \quad \bot_i | \mathbf{L} | \mathbf{R} \\
\text{pre-focus states} & q_f & ::= \quad \bot_f | \mathbf{L}[\pi, f] | \mathbf{R}[f, \rho]
\end{array}
\qquad \bot_i[\pi, f] = \bot_f = \bot_i[f, \rho]
$$

$$
\frac{\delta : X \to Y \in \mathcal{D} \quad p(\delta) = f}{X \underset{f}{\stackrel{q_f}{\rightleftharpoons}} Y} \delta
$$

$$
\frac{N \underset{\pi f}{\stackrel{q_i[\pi, f]}{\rightleftharpoons}} P}{\pi^+ N \underset{f}{\stackrel{q_i}{\rightleftharpoons}} P} L\pi^+
$$

$$
\frac{N \underset{\pi f \rho}{\overset{\bot_f}{\rightleftharpoons}} P}{\pi^+ N \underset{f}{\overset{\bot_i}{\rightleftharpoons}} \rho^- P} L\pi^+ R\rho^-
$$

$$
\frac{N \underset{f \rho}{\stackrel{q_i[f, \rho]}{\rightleftharpoons}} P}{N \underset{f}{\stackrel{q_i}{\rightleftharpoons}} \rho^- P} R\rho^-
$$

$$
q_f = \mathbf{R}[f, \rho] \Rightarrow (\sigma, g) \not\le (f, \rho) \quad \frac{P \underset{g}{\overset{\mathbf{L}}{\rightleftharpoons}} Q}{\sigma^- P \underset{\sigma g}{\overset{q_f}{\rightleftharpoons}} Q} L\sigma^-
$$

$$
q_f = \mathbf{L}[\pi, f] \Rightarrow (\pi, f) \not\le (g, \tau) \quad \frac{N \underset{g}{\overset{\mathbf{R}}{\rightleftharpoons}} M}{N \underset{g\tau}{\overset{q_f}{\rightleftharpoons}} \tau^+ M} R\tau^+
$$

$$
\begin{array}{l}
q_f = \mathbf{L}[\pi, f] \Rightarrow (\pi, f) \not\le (\sigma g, \tau) \\
q_f = \mathbf{R}[f, \rho] \Rightarrow (\sigma, g\tau) \not\le (f, \rho)
\end{array}
$$

$$
\frac{P \underset{\sigma^- P}{\overset{\bot_i}{\rightleftharpoons}} N}{\sigma^- P \underset{\sigma g \tau}{\overset{q_f}{\rightleftharpoons}} \tau^+ N} L\sigma^- R\tau^+
$$

where $(a, b) \le (c, d) := \exists e. c = ae \wedge b = ed.$

<caption>Figure 6: Maximally multifocused derivations (factorization preordered base category)</caption>

For example, suppose we are in a “left-locked” state $q_f = \mathbf{L}[\pi, f]$. That means that in the current stage of proof search, we just performed a left-focus rule to initiate a $\mathbf{L}$-bipole followed by a $\mathbf{L}\pi^+$ rule to terminate it. We now have the following choices are available:

• any left-focus rule can be applied freely;

• a right-focus rule $R\tau^+$ beginning a $\mathbb{R}$ bipole with intermediate arrow $g$ can only be applied if $(\pi, f) \not\le (g, \tau)$ in the factorization order;

• a bi-focus rule $L\sigma^- R\tau^+$ beginning a $\mathbb{L}\mathbb{R}$ bipole with intermediate arrow $g$ can only be applied if $(\pi, f) \not\le (\sigma g, \tau)$ in the factorization order.

Dual restrictions apply in a “right-locked” state $q_f = \mathbf{R}[f, \rho]$.

Our use of lock states is inspired by formulations of focusing and maximal multifocusing using tag annotations by Uustalu, Veltri, and Wan [53, 54].

By the preceding analysis we immediately have the following result.

**Proposition 3.24.** *Maximally multifocused proofs of unlocked judgments* $S \mathrel{\mathop{\Rightarrow}\nolimits}_f^{\bot_i} T$ *are in one-to-one correspondence with (par $\cup$ gra)-normal multifocused proofs of* $S \mathrel{\mathop{\Rightarrow}\nolimits}_f T$.

*Proof.* The side conditions on the rules $L\sigma^-$ and $R\tau^+$ ensure that they never create a **par** redex, while the side condition on the $L\sigma^- R\tau^+$ rule ensures that it never creates a **gra** redex. Conversely, given a multifocused proof with no **par** or **gra** redex, we can always annotate it
with states following the locking discipline of Figure 6 in a uniquely determined way, starting
from an unlocked state $q_i = \perp_i$. $\square$

Combining Proposition 3.24 with Theorem 3.23 then implies the following.

**Corollary 3.25.** *Under the FP condition, there is a one-to-one correspondence between arrows $\alpha : S \to T$ in $\mathcal{Bif}(p)$ such that $\Lambda_p(\alpha) = f$ and maximally multifocused proofs of $S \implies_f \perp_i T$.*

This correspondence means that if the base category $\mathcal{C}$ is factorization preordered then maximally multifocused proofs give an equation-free inductive definition of arrows of $\mathcal{Bif}(p)$. An important special case is when $\mathcal{C} = \mathcal{FG}$ is the free category over a graph $\mathcal{G}$. In that case, the factorization order reduces to a linear order (a path of length $n$ has $n+1$ linearly ordered factorizations) and the calculus can be simplified somewhat: states only need to keep track of the type of the last bipole and the intermediate arrow $f$ (but not $\pi$ or $\rho$), and the factorization order test can be replaced by a single prefix or suffix test (since for any two factorizations of a word $w = uv = u'v'$, $u$ is a prefix of $u'$ just in case $v'$ is a suffix of $w$).

On the other hand, in both the free case and general FP case, our definition of cut-elimination or horizontal composition of two multifocused proofs in Section 3.4.5 does not preserve maximality—to obtain a maximal multifocused proof one needs to renormalize the result of the composition. We leave open the question of whether there is a more direct definition of horizontal composition on maximal derivations.

**3.7. Decidability and enumeration.** In studying their free adjoint construction, Dawson, Paré, and Pronk [15] established the surprising result that, in general, equality of 2-cells in $\Pi_2(\mathcal{C})$ is undecidable—or more precisely that there is no decision procedure for determining whether two representatives of 2-cells (what they call “fences”) denote the same 2-cell. They gave two proofs of this result, first by exhibiting a very concrete reduction from the halting problem for 2-register machines, and second by giving a somewhat simpler and more abstract reduction from the undecidable problem of determining whether two vertices of an infinite (but locally finite) bipartite graph are connected by a path. Their latter proof translates cleanly to an analogous undecidability result for sequentialization equivalence.

**Definition 3.26.** We say that a category $\mathcal{C}$ has **locally finite factorizations** just in case every commuting square in $\mathcal{C}$ has at most finitely many diagonal fillers, or equivalently if the category of factorizations of every arrow is locally finite (i.e., has finite homsets).

By a *locally finite bipartite graph*, we mean a span of sets $V \stackrel{p_1}{\rightleftharpoons} E \stackrel{p_2}{\longrightarrow} W$ such that the fibers of $p_1$ and $p_2$ are finite. (Every edge $e \in E$ connects a vertex $v \in V$ to a vertex $w \in W$, where $v = p_1(e)$ and $w = p_2(e)$. So local finiteness says that every vertex of either class is involved in only finitely many edges, i.e., has finite degree.) To any locally finite bipartite graph $G$, we can associate a category $\mathcal{C}_G$ with locally finite factorizations, defined as the subcategory of $\mathcal{Set}$ generated by the five sets

$$0, 1, V, W, E$$

(where 0 and 1 are respectively the empty set and singleton set), the projection functions

$$V \stackrel{p_1}{\leftarrow} E \stackrel{p_2}{\longrightarrow} W$$
describing the incidence relation of $G$, the constant functions

$$1 \xrightarrow{v} V \qquad 1 \xrightarrow{w} W \qquad 1 \xrightarrow{e} E$$

associated to every vertex $v \in V$ or $w \in W$ or edge $e \in E$, and finally the unique functions from the empty set

$$0 \xrightarrow{a_X} X$$

for $X \in \{1, V, W, E\}$. To see that local finiteness of $G$ implies that $\mathbb{C}_G$ has locally finite factorizations, first note that the only non-degenerate commuting squares are of the form

$$\begin{tikzcd}
  0 \arrow[r, "a_E"] \arrow[d, "a_1"] & E \arrow[d, "p_1"] \\
  1 \arrow[r, "v"] & V
\end{tikzcd} \qquad \begin{tikzcd}
  0 \arrow[r, "a_E"] \arrow[d, "a_1"] & E \arrow[d, "p_2"] \\
  1 \arrow[r, "w"] & W
\end{tikzcd}$$

and then observe that diagonal fillers for these squares correspond to edges incident to the respective vertices:

$$\begin{tikzcd}
  0 \arrow[r, "a_E"] \arrow[d, "e^{\nrightarrow}", "1"'] & E \arrow[d, "p_1"] \\
  1 \arrow[r, "v"] & V
\end{tikzcd} \qquad \begin{tikzcd}
  0 \arrow[r, "a_E"] \arrow[d, "e^{\nrightarrow}", "1"'] & E \arrow[d, "p_2"] \\
  1 \arrow[r, "w"] & W
\end{tikzcd}$$

Now, to any vertex or edge $x$ of $G$ let us associate a stack $\alpha_x$ of the zigzag double category $\mathbb{Z}(\mathbb{C}_G)$, as follows:

$$\alpha_v := \begin{tikzcd}
  0 \arrow[r, "a_V"] \arrow[d, "a_1", "1 - v"'] & V \arrow[d, "L"] \\
  1 \arrow[r, "v"] & V
\end{tikzcd} \qquad \alpha_e := \begin{tikzcd}
  0 \arrow[r, "a_V"] \arrow[d, "a_1", "1 - e"'] & V \arrow[d, "L^- R^-"', "p_1"] \\
  1 \arrow[r, "e"] & E
\end{tikzcd} \qquad \alpha_w := \begin{tikzcd}
  0 \arrow[r, "a_V"] \arrow[d, "a_1", "1 - a_W"'] & V \arrow[d, "R"] \\
  0 \arrow[r, "a_W"] & W
\end{tikzcd}$$

Observe that $\alpha_e$ sequentializes to $\alpha_v$ and $\alpha_w$, that is, $\alpha_v \leftarrow_{\text{seq}} \alpha_e \rightarrow_{\text{seq}} \alpha_w$, just in case $v = p_1(e)$ and $w = p_2(e)$.

**Theorem 3.27** (cf. Theorems 2 and 3 of Dawson, Paré, and Pronk [15]). There is a category $\mathbb{C}$ with locally finite factorizations for which the following equivalent problems are both undecidable:

* given two stacks of double cells in $\mathbb{Z}(\mathbb{C})$, determine whether they vertically compose to the same double cell;

* given two proofs in the bifibrational calculus generated by $p = \text{id}_\mathbb{C}$, determine whether they are permutation equivalent.
**Proof.** We take $\mathcal{C} = \mathcal{C}_{G_M}$ where $G_M$ is a bipartite version of the configuration graph of some universal Turing machine $M$. Without loss of generality we will assume that $M$ is deterministic and has a unique halting configuration $\tau_{\text{halt}}$. Let us write $\text{Conf}_M$ for the configuration space of $M$, that is, the set of tuples $(q, u, v)$ of a state $q$ and finite strings $u$ and $v$ over the working alphabet denoting the contents of the tape to the left and right of the head. We define $G_M$ by taking $V = \text{Conf}_M \times \{0\}$ and $W = \text{Conf}_M \times \{1\}$ to be two disjoint copies of the configuration space, and $E \subseteq V \times W$ as the union

$$E = \{ ((\sigma, 0), (\tau, 1)) \mid \sigma \to \tau \text{ is a valid transition of } M \} \\ \cup \{ ((\sigma, 0), (\sigma, 1)) \mid \sigma \in \text{Conf}_M \}$$

By the preceding observation, it is clear that any directed chain of configurations

$$\sigma_1 \to \sigma_2 \to \sigma_3 \to \dots$$

induces a corresponding chain of sequentialization equivalences:

$$\alpha_{(\sigma_1, 0)} \sim_{\text{seq}} \alpha_{(\sigma_2, 1)} \sim_{\text{seq}} \alpha_{(\sigma_2, 0)} \sim_{\text{seq}} \alpha_{(\sigma_3, 1)} \sim_{\text{seq}} \alpha_{(\sigma_3, 0)} \sim_{\text{seq}} \dots$$

Conversely, the assumption that $M$ is deterministic and has a unique halting state ensures that any chain of sequentialization equivalences $\alpha_{(\sigma, 0)} \sim_{\text{seq}} \dots \sim_{\text{seq}} \alpha_{(\tau_{\text{halt}}, 1)}$ corresponds to a halting execution $\sigma \to^* \tau_{\text{halt}}$. We have thus reduced the halting problem for $M$ to deciding sequentialization equivalence $\alpha_{(\sigma, 0)} \sim_{\text{seq}} \alpha_{(\tau_{\text{halt}}, 1)}$, or equivalently permutation equivalence $\alpha_{(\sigma, 0)} \sim \alpha_{(\tau_{\text{halt}}, 1)}$. $\square$

Dawson, Paré, and Pronk proved decidability of (fence equivalence for) the $\Pi_2(\mathcal{C})$ construction separately in the cases that $\mathcal{C}$ is locally finite or factorization preordered. We now prove analogues of these two results for deciding equality of morphisms in $\mathcal{Bif}(p)$, or more precisely for deciding whether two proofs of the same judgment represent the same morphism. The first is already a consequence of the results of Section 1, while the second is a corollary of our normal form theorem.

**Theorem 3.28** (cf. Propositions 2 and 3 of Dawson, Paré, and Pronk [15]). Let $p: \mathcal{D} \to \mathcal{C}$ and suppose that $\mathcal{C}$ satisfies either of the following conditions:

(1) $\mathcal{C}$ is locally finite, or

(2) $\mathcal{C}$ is factorization preordered;

then for any two proofs $\alpha_1, \alpha_2: S \implies_f T$ of the bifibrational calculus generated by $p$, it is decidable whether $\alpha_1 \sim \alpha_2$.

**Proof.** (1) Two proofs are equivalent just in case there is some sequence of permutations transforming one to the other. Any such permutation leaves invariant the length of the proof, the choice of terminating axiom $\delta: X \to Y$ in $\mathcal{D}$, and the selection of left and right rules applied, merely changing the order of the rules and the intermediate base arrows that annotate the derivation. Since $\mathcal{C}$ is locally finite, there are therefore only finitely many proofs permutation equivalent to any given proof, and we can reduce $\alpha_1 \sim \alpha_2$ to a finite test $\alpha_2 \in [\alpha_1]$.

(2) This is a corollary of our normal theorem, Theorem 3.23, which states that each multifocused proof has a unique maximal normal form, under the FP condition. We can thus decide whether two proofs denote the same morphism of $\mathcal{Bif}(p)$ simply by computing their normal forms and checking that these are equal. $\square$
**Remark 3.29.** Technically, we need $\mathcal{C}$ to satisfy computable versions of either local finiteness or factorization preorder to get a decision procedure. For instance, we need to be able to effectively enumerate the finite homset $\mathcal{C}(A, B)$ between any pair of objects. Or, for any given square, we need to be able to decide whether that square is empty or else compute a filler. We also need the equality of morphisms in $\mathcal{C}$ and $\mathcal{D}$ to be decidable to check that two proofs are identical. We omit these precisions from the statement of the theorem, since it is clear from context that the conditions should be interpreted constructively.

Besides entailing decidability of the word problem, the normal form theorem has the equally important application of allowing us to *enumerate* homsets of free bifibrations without duplicates, assuming the FP condition. We are most interested in the situation that $\mathrm{Bif}(p)$ is relatively locally finite in the following sense.

We say that a category $\mathcal{D}$ equipped with a functor $p : \mathcal{D} \to \mathcal{C}$ is **relatively locally finite** (relative to $p$) if the *relative homsets* over $f$

$$ \mathcal{D}_f(X, Y) := \{ \delta \mid \delta : X \to Y, p(\delta) = f \} $$

are finite, for every arrow $f : A \to B$ of $\mathcal{C}$ and pair of objects $X$ and $Y$ of $\mathcal{D}$ lying above $A$ and $B$ respectively. (Thus a category $\mathcal{C}$ is locally finite iff the unique functor $!_C : \mathcal{C} \to 1$ is relatively locally finite.)

**Theorem 3.30.** Let $p : \mathcal{D} \to \mathcal{C}$ and suppose $\mathcal{C}$ satisfies the FP condition. If $\mathcal{D}$ is relatively locally finite (relative to $p$) and $\mathcal{C}$ has locally finite slices and coslices, then $\mathrm{Bif}(p)$ is relatively locally finite (relative to $\Lambda_p$). In particular, the fiber category $\mathrm{Bif}(p)_A$ of every object $A \in \mathcal{C}$ is locally finite.

*Proof.* Suppose given an arrow $f : A \to B$ of $\mathcal{C}$ and a pair of bifibrational formulas $S \sqsubseteq A$ and $T \sqsubseteq B$. By Corollary 3.25, we can enumerate canonical representatives of arrows $\alpha \in \mathrm{Bif}(p)_f(S, T)$ using the sequent calculus of Figure 6 to search for maximally multifocused proofs of $S \implies_f^\perp T$. There are only three potential sources of nondeterminism:

(1) the choice of whether to initiate a $\mathbb{L}$, $\mathbb{R}$, or $\mathbb{LR}$ bipole when proving a neutral sequent;

(2) the choice of an arrow $g$ in the premise of a left-/right-/bi-focus rule;

(3) the choice of an axiom $\delta : X \to Y \in \mathcal{D}$ to terminate the proof.

But each of these choice points are finite branching:

(1) at most three rules to try (some may be forbidden by the lock state $q_f$ or if one side of the sequent is atomic);

(2) finite by the assumption that $\mathcal{C}$ has locally finite slice and coslice categories (for example, to derive a sequent of the form $\sigma^- P \implies_h^q Q$ using the $\mathbb{L}\sigma^-$ rule, we must pick an arrow $g$ such that $h = \sigma g$; observe that such an arrow corresponds to a morphism $\sigma \to h$ in the coslice category $A/\mathcal{C}$, where $A = \mathrm{dom}\,\sigma = \mathrm{dom}\,h$);

(3) finite by the assumption that $\mathcal{D}$ is relatively locally finite.

We conclude that there are only finitely many maximally multifocused proofs of any given judgment, and hence that the relative homsets are finite. In particular, for every object $A \in \mathcal{C}$, the homset of the fiber category $\mathrm{Bif}(p)_A$, corresponding to the relative homset over $\mathrm{id}_A$, is finite. $\square$

**Corollary 3.31.** Under the assumptions of Theorem 3.30, logical equivalence of bifibrational formulas is decidable.
*Proof.* Recall that by definition, two formulas $S_1, S_2 \subset A$ are logically equivalent if there exist derivations $\alpha : S_1 \implies_{\mathrm{id}_A} S_2$ and $\beta : S_2 \implies_{\mathrm{id}_A} S_1$ whose compositions are permutation equivalent to identities (Defn. 1.19), or equivalently just in case they are isomorphic in the fiber category $\mathcal{Bif}(p)_A$ (Prop. 1.20). It suffices to enumerate canonical representatives of all such derivations $\alpha$ and $\beta$ using Theorem 3.30, compute their cuts $\alpha \cdot \beta$ and $\beta \cdot \alpha$, and decide whether $\alpha \cdot \beta \sim \mathrm{id}_{S_1}$ and $\beta \cdot \alpha \sim \mathrm{id}_{S_2}$ using Theorem 3.28. $\square$

As already remarked, free categories satisfy the FP condition because their factorization categories are linear orders. Moreover, although free categories $\mathcal{FG}$ are not locally finite unless the underlying graph $\mathcal{G}$ is acyclic, their slices and coslices are posetal and hence trivially locally finite. Thus the enumeration and decision procedures described above are applicable (and even become slightly simpler since the sequent calculus of Figure 6 can be simplified a bit, as remarked at the end of Section 3.6).

Finally, Theorem 3.30 can clearly be generalized to derive any infinite cardinality bound on the relative homsets of $\mathcal{Bif}(p)$, assuming the same bound on the relative homsets of $\mathcal{D}$ and the homsets of the slices and coslices of $\mathcal{C}$. We can also use the sequent calculus to effectively enumerate the (potentially infinite) relative homsets of $\mathcal{Bif}(p)$, given procedures for doing the same for $\mathcal{D}$ and for the slices and coslices of $\mathcal{C}$.

## 4. FREE $(\mathcal{P}, \mathcal{N})$-FIBRATIONS

As previously mentioned, Dawson, Paré, and Pronk's $\Pi_2(\mathcal{C})$ construction may be seen as a weaker version of the free groupoid construction, which turns a category into a groupoid by freely adding an inverse to every arrow. More often, one only wants to add formal inverses to a class of arrows $\mathcal{W}$, a process known as localization (see, e.g., Borceaux [10, Ch.5]), which freely builds a category $\mathcal{C}[\mathcal{W}^{-1}]$ equipped with a functor $\mathcal{C} \to \mathcal{C}[\mathcal{W}^{-1}]$ sending every arrow $f \in \mathcal{W}$ to an isomorphism. DPP [14, §4.1] discuss how to adapt their construction of $\Pi_2(\mathcal{C})$ to define a 2-category $\mathcal{C}[\mathcal{W}^*]$ in which every arrow $f \in \mathcal{W}$ is freely equipped with a right adjoint. In this section we quickly explain how our construction of the free bifibration on a functor $p : \mathcal{D} \to \mathcal{C}$ may be similarly adapted when the operations of pushing and pulling are restricted to certain classes of arrows of $\mathcal{C}$.

**Definition 4.1.** Let $\mathcal{P} \subset \mathcal{C}$ and $\mathcal{N} \subset \mathcal{C}$ be two subsets of arrows (not necessarily subcategories) of $\mathcal{C}$. We say that a functor $\pi : \mathcal{E} \to \mathcal{C}$ is a $(\mathcal{P}, \mathcal{N})$-fibration if it has $+-$cartesian liftings of all arrows in $\mathcal{P}$ and $-+\mathrm{cartesian liftings}$ of all arrows in $\mathcal{N}$.

As special cases, a $(\emptyset, \mathcal{C})$-fibration is a Grothendieck fibration in the ordinary sense, a $(\mathcal{C}, \emptyset)$-fibration is an opfibration, and a $(\mathcal{C}, \mathcal{C})$-fibration is a bifibration.

A case of particular interest is when $(\mathcal{P}, \mathcal{N})$ constitute a factorization system for the base category. Such $(\mathcal{P}, \mathcal{N})$-fibrations relative to a factorization system have been termed *ambifibrations* by Joachim Kock and André Joyal. One interesting property of ambifibrations, noted by Kock [30], is that they give rise to ternary factorization systems in which every arrow of the total category factors as a $+\mathrm{cartesian arrow}$, followed by an arrow lying over
an identity, followed by a $\overline{\text{--}}$cartesian arrow:

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

We will consider an example of a free ambifibration in Section 5.3.

Unless otherwise stated we do not assume anything about $\mathcal{P}$ and $\mathcal{N}$ in this section. We write $\Lambda_{p,\mathcal{P},\mathcal{N}} : \text{Bif}(p, \mathcal{P}, \mathcal{N}) \to \mathcal{C}$ for the free $(\mathcal{P}, \mathcal{N})$-fibration on a functor $p : \mathcal{D} \to \mathcal{C}$.

**Sequent calculus.** The presentation of the free bifibration that we gave via the sequent calculus in Section 1 adapts directly to a presentation of the free $(\mathcal{P}, \mathcal{N})$-bifibration. For this one simply has to restrict the formation rules on bifibrational formulas:

$$ \frac{S \sqsubseteq A \qquad f : A \to B \in \mathcal{P}}{f^+ S \sqsubseteq B} \qquad \frac{g : B \to C \in \mathcal{N} \qquad T \sqsubseteq C}{g^- T \sqsubseteq B} $$

Otherwise, everything remains the same: the definition of the inference rules, permutation equivalence, cut-elimination, et cetera. This presentation makes clear that $\text{Bif}(p, \mathcal{P}, \mathcal{N})$ is a full subcategory of $\text{Bif}(p)$.

**The zigzag double category.** In Section 2 we defined the double category of zigzags $\mathbb{Z}(\mathcal{C})$ by first constructing the free bifibration on the identity functor $\text{id}_\mathcal{C}$. We can similarly define a double category of restricted zigzags $\mathbb{Z}(\mathcal{C}, \mathcal{P}, \mathcal{N})$, whose vertical arrows are zigzags moving positively along arrows in $\mathcal{P}$ and negatively along arrows in $\mathcal{N}$. In particular, we can recover DPP's $\mathcal{C}[W^*]$ in this way as the vertical 2-category of $\mathbb{Z}(\mathcal{C}, \mathcal{C}, W)$.

**Weak focusing.** The syntax of weakly focused derivations given in Section 3.3 works just as well for $(\mathcal{P}, \mathcal{N})$-fibrations, although the proof of correctness based on the equivalence $\text{Bif}(p) \simeq \text{saBif}(p)$ has to be slightly adapted. The equivalence with strictly alternating formulas relied on the pseudofunctoriality laws $(g \circ f)^+ S \equiv g^+ f^+ S$ and $(f g)^- T \equiv f^- g^- T$, whereas $\mathcal{P}$ and $\mathcal{N}$ are not necessarily closed under composition. However, Theorem 3.2 can be directly adapted to prove the following.

**Proposition 4.2.** If $\mathcal{P}$ and $\mathcal{N}$ are closed under binary composition, then $\text{Bif}(p, \mathcal{P}, \mathcal{N}) \simeq \text{saBif}(p, \mathcal{P}, \mathcal{N})$.

The restrictions on $\mathcal{P}$ and $\mathcal{N}$ are not problematic, because we can always close them under finite compositions and obtain an equivalent free $(\mathcal{P}, \mathcal{N})$-fibration. Given a subset of arrows $W \subset \mathcal{C}$, let us write $W^*$ for the subcategory of $\mathcal{C}$ generated by adding identity arrows $\text{id}_A$ and $\text{id}_B$ for every $f : A \to B \in W$, and by closing under binary composition. The pseudofunctoriality laws immediately imply the following.

**Proposition 4.3.** $\text{Bif}(p, \mathcal{P}, \mathcal{N}) \simeq \text{Bif}(p, \mathcal{P}^*, \mathcal{N}^*)$.

**Corollary 4.4.** If $\mathcal{C} = \mathbb{FG}/\sim$ is freely generated by some graph $G$ modulo some equations, then $\text{Bif}(p) \simeq \text{Bif}(p, G, G)$.
**Maximal multifocusing.** Finally, the results of Sections 3.5–3.7 provided a strong notion of normal form for free bifibrations as well as decidability results in the case that the base category is factorization preordered (Definition 3.18). One benefit of considering free $(\mathcal{P}, \mathcal{N})$-fibrations is that we can relax this requirement to the a priori weaker condition that $\mathcal{C}$ is both $\mathcal{P}$-factorization preordered and $\mathcal{N}$-factorization preordered.

**Definition 4.5.** Let $\mathcal{W} \subset \mathcal{C}$ be a subset of arrows of a category $\mathcal{C}$. We say that $\mathcal{C}$ is $\mathcal{W}$-factorization preordered (or $\mathcal{W}$-FP) if for any diagram of the form

$$ \begin{tikzcd} \mathcal{W} \arrow[r, "f \in \mathcal{W}"] \arrow[d, "g"] & \mathcal{W} \arrow[d, "h"] \arrow[r, "k \in \mathcal{W}"] \arrow[d, "g = h"'] \arrow[r, "k \in \mathcal{W}"] \arrow[d, "h = k"] \arrow[r, "f \in \mathcal{W}"] \arrow[d, "g = h"'] \arrow[r, "k \in \mathcal{W}"] \arrow[d, "h = k"] \arrow[r, "f \in \mathcal{W}"] \arrow[d, "g = h"'] \arrow[r, "k \in \mathcal{W}"] \arrow[d, "h = k"] \end{tikzcd} $$

if both $fg = fh$ and $gk = hk$ then necessarily $g = h$. Equivalently, $\mathcal{C}$ is factorization preordered just in case every commuting square of the following form has at most one diagonal filler:

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

**Proposition 4.6.** Every category $\mathcal{C}$ is both $\mathcal{C}_{\text{epi}}$-FP and $\mathcal{C}_{\text{mono}}$-FP, where $\mathcal{C}_{\text{epi}}$ and $\mathcal{C}_{\text{mono}}$ consist respectively of the epic arrows and the monic arrows of $\mathcal{C}$.

The analysis of Sections 3.5–3.7 carries over and we obtain the following.

**Theorem 4.7.** If $\mathcal{C}$ is both $\mathcal{P}$-FP and $\mathcal{N}$-FP, then arrows of $\mathcal{Bif}(p, \mathcal{P}, \mathcal{N})$ are canonically represented by maximally multifocused derivations, and permutation equivalence is decidable. If moreover $\mathcal{D}$ is relatively locally finite and $\mathcal{C}$ has locally finite slices and coslices, then $\mathcal{Bif}(p, \mathcal{P}, \mathcal{N})$ is relatively locally finite and logical equivalence is decidable.

**Remark 4.8.** As mentioned, fibrations and opfibrations arise as particular cases of $(\mathcal{P}, \mathcal{N})$-fibration, taking $\mathcal{P} = \emptyset, \mathcal{N} = \mathcal{C}$ for fibrations and $\mathcal{P} = \mathcal{C}, \mathcal{N} = \emptyset$ for opfibrations. Even if $\mathcal{C}$ is not factorization preordered, strongly focused derivations do provide normal forms for the arrows of $\mathcal{Bif}(p, \emptyset, \mathcal{C})$ or $\mathcal{Bif}(p, \mathcal{C}, \emptyset)$, for the simple reason that there are no $\mathcal{L}\mathbb{R}$-bipoles and so sequentialization equivalence reduces to discrete equality. The usual constructions of the free fibration and free opfibration as comma categories may be recovered in this way if one restricts to strictly alternating formulas of depth 1, avoiding formulas of depth 0 so as to obtain a split fibration (cf. Remark 3.4).

# 5. THE COMBINATORICS OF FREE BIFIBRATIONS AND AMBIFIBRATIONS

We conclude with a deeper analysis of the specific examples of free bifibrations and ambifibrations that were mentioned in the Introduction. In all of these examples, some rich combinatorial structure emerges out of very simple generating data, and the exploration of this structure is facilitated by the bifibrational calculus.
**5.1. Reconstructing the simplex category.** Recall that we write $\Delta$ for the category of finite ordinals and order-preserving maps, which is sometimes referred to as the *augmented simplex category* to emphasize that it includes the empty ordinal $0$, but which we will simply call the simplex category. We write $\Delta_{\perp}$ for the category of non-empty finite ordinals and order-and-least-element preserving maps. We write $L : \Delta \to \Delta_{\perp}$ for the functor sending an ordinal $n$ to a non-empty ordinal $n'$ by adding a $\perp$ element, and an order-preserving map $\theta : m \to n$ to the order-and-least-element-preserving map $\theta' : m' \to n'$ defined by $\theta'(\perp) = \perp$ and $\theta'(x) = \theta(x)$ for $x > \perp$. This functor has a right adjoint given by the forgetful functor $R : \Delta_{\perp} \to \Delta$, which interprets $n'$ as $1+n$ and forgets that a map is $\perp$-preserving.

**Proposition 5.1.** Let $F : 2 \to \text{Adj}$ and $p_2 : 1 \to 2$ be the functors shown below:

$$ F0 = \Delta \qquad F1 = \Delta_{\perp} \qquad Ff = \Delta \xrightarrow[\substack{\leftarrow \\ R}]{L} \Delta_{\perp}. $$
$$ \begin{array}{ccc} 1 & \ast & \\ \searrow^{p_2} & & \searrow^{f} \\ 2 & & 1 \end{array} $$

Then the unique morphism of bifibrations $\text{Bif}(p_2) \to \int_2 F$ sending the atomic formula $\ast$ to the empty ordinal $0$ is an equivalence of categories. In particular, $\Delta$ is equivalent to $\text{Bif}(p_2)_0$.

**Proposition 5.1** is a corollary of Theorem 5.3 below, so we do not give a detailed proof here, but we sketch the correspondence. Under the equivalence, each ordinal $n$ in $\Delta$ is interpreted as the bifibrational formula

$$ \text{``n''} := \underbrace{f^- f^+ \dots f^- f^+}_{n \text{ times}} \ast \subset 0 $$

while each non-empty ordinal $n'$ in $\Delta_{\perp}$ is interpreted as the bifibrational formula

$$ \text{``n''} := f^+ \underbrace{f^- f^+ \dots f^- f^+}_{n \text{ times}} \ast \subset 1. $$

Conversely, since $\ast$ is the only atom and $f$ is the only non-identity arrow, every bifibrational formula on $p_2$ is equivalent to one of these two forms. To be precise, we note that pushing or pulling along an identity arrow $id_0$ or $id_1$ is also possible, but logically equivalent to doing nothing (Prop. 1.21)—hence why we only state an equivalence $\int_2 F \equiv \text{Bif}(p_2)$ rather than an isomorphism of categories. Clearly we obtain an isomorphism if we restrict to the full subcategory $\text{Bif}(p_2, f, f) \subset \text{Bif}(p_2)$.

Observe that ordinal formulas `n` and `n'` are strictly alternating. The sequent calculus of Figure 6 becomes particularly simple when restricted to such ordinal formulas: since there are no non-trivial factorizations in the base category, the bi-focusing and bi-inversion rules can be removed (they are impossible to apply), as can the lock conditions on the left- and right-focusing rules (they are always validated). Thus any morphism in $\text{Bif}(p_2)$ may be represented canonically as a strongly monofocused derivation, which in turn is essentially just a shuffle of $\mathbb{L}$ and $\mathbb{R}$ bipoles.

As an illustration, the three order-preserving maps $2 \to 2$ depicted on the left correspond to the following three derivations of $f^- f^+ f^- f^+ \ast \Rightarrow_{id_0} f^- f^+ f^- f^+ \ast$ depicted on the right (drawn as stacks with overlaid string diagrams):
<figure><img src="image_50.png" /></figure>

The graphical correspondence should be suggestive. In general, any morphism $\mathrm{[m]} \to \mathrm{[n]}$ in $\mathrm{Bif}(p_2)_0$ can be canonically represented as a derivation that opens (reading from the bottom) with a $\mathbb{R}^-$ rule, followed by an arbitrary shuffle of $m \mathbb{L}$ bipoles with $n-1 \mathbb{R}$ bipoles, followed by a closing $\mathbb{R}^+$ rule. Since there are $\binom{m+n-1}{m}$ such shuffles, we thus derive the well-known formula for the number of order-preserving maps.

**Corollary 5.2.** There are $\frac{(m+n-1)!}{m!(n-1)!}$ order-preserving maps $m \to n$.

**5.2. Categories of trees and walks.** A natural generalization of the previous example is obtained by considering the free bifibration generated by the functor $p_\omega$ illustrated below which maps the point to the initial object of $\omega$, the totally ordered set of natural numbers considered as a category.

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

As we observed in the introduction, up to isomorphism the objects of $\mathrm{Bif}(p_\omega)_0$ may be read as Dyck words, which are in bijection with rooted plane trees, that is, trees embedded in the plane with one vertex marked as the root, considered up to planar isotopy. We draw
such trees growing upwards from the root, as depicted on the left:

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

To encode a plane tree by a Dyck word, a canonical procedure is to traverse the tree (say) from right to left starting from the root, recording a +1 every time you move up towards a child, and a -1 every time you move down back to a parent. We represent the beginning of this traversal, visually, on the right. (We will use these same colors below to visualize the traversal order.)

The corresponding bifibrational formula may be read off directly:

$$f^{-} f^{-} f^{-} f^{+} f^{+} f^{-} f^{+} f^{+} f^{-} f^{-} f^{+} f^{+} *$$

Here to keep the notation simple we have elided the indices from the $f_i$'s, which are uniquely determined. Such a word may also be interpreted as a walk on the upper plane, starting at the x-axis (at the point marked * below), constantly moving up or down while moving leftwards and eventually terminating back at the x-axis:

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

Observe that all of the information about the walk is contained in its peaks and valleys, and a tree may also therefore be represented more concisely as a strictly alternating zigzag:

$$0 \rightarrow 3 \leftarrow 1 \rightarrow 2 \leftarrow 0 \rightarrow 1 \leftarrow 0 \rightarrow 2 \leftarrow 0$$

or again as a formula in strictly alternating syntax: $f^{-3} f^{+2} f^{-1} f^{+2} f^{-1} f^{+1} f^{-2} f^{+2} *$.

Next we recall how plane trees admit an alternative representation as functors. (This idea goes back at least to Joyal [26], but may be earlier folklore.) Define the height of a vertex as its distance from the root, and the height of a tree as the maximum height of any of its vertices. Let $[k] = k+1$ be the linear order $\{0 < \dots < k\}$ seen as a posetal category. It is clear from the definitions that any rooted plane tree of height $k$ may be represented by a functor $T : [k]^{op} \rightarrow \Delta$ such that $T(0) = 1$: each linearly ordered set $T(i)$ defines the vertices of height $i$, and the parents of the non-root vertices are specified by the functions $T(i+1) \rightarrow T(i)$, which must be order-preserving by the constraints of planarity. For instance, the height-3 tree given in the example above corresponds to the functor $T : [3] \rightarrow \Delta$ depicted
below.

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

This tree also has *width* 3, defined as the maximum number of vertices at any given height. More generally, a tree of unbounded height and width may be represented as a functor $T : \omega^{op} \to \Delta$ such that $T(0) = 1$. In other words, the only requirement is that $T$ sends the initial object of $\omega$ to the terminal object of $\Delta$. Finiteness is ensured if we moreover ask that there is some natural number $k$ such that $T(k+1) = 0$ (and hence $T(j) = 0$ for all $j > k$).

We define PTree as the full subcategory of $[\omega^{op}, \Delta]$ spanned by the finite rooted plane trees, that is, the category whose objects are functors $T : \omega^{op} \to \Delta$ such that $T(0) = 1$ and $T(k+1) = 0$ for some $k$, and all natural transformations between them. For example, below we depict two different morphisms of plane trees $S \to T$ between the same pair of trees, using different color lines to indicate the mappings $S(k) \to T(k)$ of the natural transformations at each height $k$.

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

Readers familiar with the “topos of trees” $[\omega^{op}, \text{Set}]$ may recognize that PTree is defined in essentially the same way, but replacing Set by $\Delta$ to reflect planarity, and taking a full subcategory of $[\omega^{op}, \Delta]$ in order to restrict to finite trees rather than potentially infinite forests. The combination of order-preservation and naturality imposes strong constraints on the shape of plane tree morphisms. The reader may check that there are exactly 11 morphisms $S \to T$ between the trees $S$ and $T$ shown above, including the two in (5.1).

We should note that PTree is strongly related to but different from a category of plane trees defined by Joyal [26]. Joyal considered a more liberal notion of morphism $S \to T$ between plane trees encoded in the same way as functors $S, T : \omega^{op} \to \Delta$. Instead of considering natural transformations in $[\omega^{op}, \Delta]$, he took more general natural transformations between the underlying functors in $[\omega^{op}, \text{Set}]$ so long as they respect the linear orders on the fibers of the maps $S(n+1) \to S(n)$. (In other words, respect the ordering of siblings, but not necessarily of cousins.) Every morphism in PTree is a morphism in Joyal’s category