The free bifibration on a functor

A bifibration is a functor $p:𝒟\to 𝒞$ which is both a fibration and an opfibration; intuitively, objects in the domain $𝒟$ can be pushed or pulled along arrows of the codomain $𝒞$. Fibrations, opfibrations, and bifibrations play an important role throughout category theory and computer science, particularly in categorical logic. While the construction of the free (op)fibration via comma categories is well-known, the problem of building free bifibrations has remained relatively unexplored until now, with the only explicit construction appearing in unpublished work of Lamarche [3] – although the problem is also closely related to a problem considered by Dawson, Paré, and Pronk, of “freely adjoining adjoints” to a category [2].

In this work, we develop a novel proof-theoretic construction of the free bifibration ${\mathrm{\Lambda }}_p:ℬ\mathrm{if}(p)\to 𝒞$ in which objects of $ℬ\mathrm{if}(p)$ are formulas of a primitive “bifibrational logic”, and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence (see middle of figure below, with the free bifibration generated from the data of the functor $p$ on the left). Remarkably, instantiating the construction to the identity functor generates a zigzag double category $\mathbb{Z}(𝒞)$, which coincides with the free double category with companions and conjoints (or fibrant double category) on $𝒞$. This, in turn, suggests a natural string diagram calculus for morphisms in the domain of a free bifibration (see right side of figure).

The approach adapts smoothly to the more general task of freely adding pushforwards and pullbacks relative to some restricted classes of arrows $𝒫$ and $𝒩$, recovering so-called ambifibrations as a special case when $(𝒫,𝒩)$ form a factorization system. Ideas from proof theory guide us through a series of progressively stronger normal forms, deriving a canonicity result under assumption that the base category is factorization preordered relative to $𝒫$ and $𝒩$. Finally, we identify a number of surprising and interesting examples. These include a category of plane trees generated as a free bifibration over $\omega$, and a category of increasing forests generated as a free ambifibration over $\mathrm{\Delta }$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition for bicartesian squares.