The combinatorics of free bifibrations
Bryce Clarke & Gabriel Scherer & Noam Zeilberger(CLA talk abstract, November 7, 2023)

A functor p : D Ñ C between two categories is a bifibration when, roughly speaking, objects of D may
be pushed and pulled along arrows of C. Formally, for any arrow f : A Ñ B in C and any object S in Dsuch that ppSq “ A, there should be an object f˚ S and an arrow fS : S Ñ f˚ S of D such that ppfS q “ f ,DfSSf˚ SpCfAB

which are universal in the sense that for any arrow g : B Ñ C in C and arrow α : S Ñ T in D such thatppαq “ f g, there is a unique arrow β : f˚ S Ñ T such that α “ fS β.
αSfSSTf˚ SβT“Af

Bg

CAf

Bg

CDually, for any arrow g : B Ñ C in C and object T in D such that ppT q “ C, there should be an object g ˚ TgT q “ g,and an arrow gsT : g ˚ T Ñ T of D such that ppsgsTg˚ TTgBCagain universal in the sense that for any arrow f : A Ñ B in C and arrow α : S Ñ T in D such thatgT .
ppαq “ f g, there is a unique arrow β : S Ñ g ˚ T such that α “ βsα

SβSTg˚ TgsT

T“Af

Bg

CAf

Bg

C

An immediate consequence of the definition is that if p : D Ñ C is a bifibration then the operations ofpushing or pulling along an arrow f : A Ñ B of C extend to a pair of adjoint functors
f˚DAKfDB˚

where DA and DB are the fiber categories of A and B relative to the functor p, defined as the subcategoriesof D spanned by the arrows living over the identities idA and idB in C, and indeed any bifibration over C may
be equivalently described by a pseudofunctor C Ñ Adj into the category of small categories and adjunctions.
1

The categorical notion of bifibration was originally introduced by Grothendieck, together with the weaker
notion of fibration where one only has the ability to pull objects of the category above along arrows of thecategory below. One reason for the special interest of bifibrations from the perspective of logic and computerscience is that the operations of pushing forward or pulling back along an arrow may be seen as generalizationsof existential and universal quantification (cf. [MZ16]), and hence by alternating these operations one can insome sense define objects of arbitrary quantifier complexity. The pushforward and pullback operations may
also be seen as generalizations of strongest postconditions and weakest preconditions in specification logics.
Although most functors are not bifibrations, any functor p : D Ñ C generates a free bifibration, in thesense that there is a bifibration p̃ : BFibppq Ñ C and a functor ηp : D Ñ BFibppq such that p “ p̃ ˝ ηp .
Moreover, the free bifibration is universal in the sense that if q : E Ñ C is any bifibration equipped witha functor θ : D Ñ E such that p “ q ˝ θ, then there is an essentially unique morphism of bifibrations
θ̃ : BFibppq Ñ E such that θ “ θ̃ ˝ ηp . Whereas the free fibration over a functor has a well-known and very
simple concrete description, the free bifibration has been relatively little studied, and describing it explicitly
is far more subtle. The problem of building the free bifibration over a functor p : D Ñ C is closely related
to the problem, studied by Dawson, Paré, and Pronk [DPP03a, DPP03b], of extending C to a 2-categoryΠ2 C by freely adjoining right adjoints (cf. [SS86]). However, as far as we are aware there is only one direct
construction of the free bifibration over a functor in the literature, by Lamarche [Lam10, Lam14],
In our work, we have developed a number of alternative descriptions of the free bifibration over anarbitrary functor p : D Ñ C. One description is proof-theoretic, viewing the objects of BFibppq as formulas
in a primitive logic containing unary connectives f˚ and f ˚ for every morphism f of C, with the objects ofD serving as atomic formulas. The morphisms of BFibppq are then defined as equivalence classes of proofs
in a simple cut-free sequent calculus containing only four logical rules
S ùñ Tg

Lff˚ S ùñ TS ùñ f˚ Tg

S ùñ TS ùñ TS ùñ Tfg

gRf

˚f S ùñ Tgfgf

Lfs

S ùñ f ˚ TRfs

gfgwhere proofs are considered modulo four permutation relations, including the relations
S ùñ T

fhRg

S ùñ g˚ Tf hg

f˚ S ùñ g˚ TLfhLfT„ f˚ S ùñhf˚ S ùñ g˚ TS ùñ g˚ ThRg

hg

Rg

f ˚ S ùñ g˚ Thg

hg

S ùñ TS ùñ TS ùñ T

fhLfs

f hg

S ˚ ùñ T„Lfs

fhf ˚ S ùñ g˚ TRg

f hg

as well as their symmetric versions with pushforward and pullback swapped. The cut rule is admissible,
thereby defining composition of morphisms in BFibppq. This sequent calculus is closely related to an alternative description of the free bifibration using double category theory. The double category of zigzags ZC
has objects and horizontal arrows given by the objects and arrows of C, vertical arrows given by zigzags (=signed sequences of arrows) in C, and double cells of zigzag morphisms generated by vertical pastings of thefour generating cells below (ignore the colored arcs for now)
¨fg

¨

¨

Lff

¨gg

¨Rf
¨¨gf

¨f

¨¨

Lfsf

¨g

¨fg

gf

¨Rfs
¨¨gf

¨

modulo four permutation relations. Composition of zigzag morphisms can be defined inductively by analysisof the intermediate zigzag, thereby defining horizontal composition for the double category. The connection
with bifibrations is that ZC is the free bifibration over the identity functor idC : C Ñ C, while conversely,
any free bifibration may be reconstructed by pulling back the source functor src : ZC Ñ C of the double
category along an arbitrary functor p : D Ñ C. Finally, zigzag morphisms in ZC also have a natural graphical2interpretation (at least in the case where C is a free category) as certain planar arc diagrams considered up
to isotopy (see colored arcs above).
A challenge in understanding free bifibrations is getting a handle on the equivalence classes of zigzag
morphisms induced by the permutation relations. Indeed, by a reduction of [DPP03b], this equivalence relation is in general undecidable! One way we have attacked the problem is via the proof-theoretic techniqueof focusing, developing a (for now conjectured) canonical form whereby permutation equivalence classes ofderivations in the above sequent calculus are represented by focused derivations modulo a more elementary
notion of “observational” equivalence. In many cases (namely when C is factorization preordered ) the observational equivalence relation on focused derivations is just equality, although in general it is undecidable.
Another way we have attacked the problem is by considering examples, and here is where it appears that
free bifibrations give rise to a number of categories of great combinatorial interest. A basic example is thefree bifibration over the functor p “ p˚ ÞÑ 0q : 1 Ñ 2 sending the unique object of 1 to the initial object of
the walking arrow category 2 “ 0 Ñ 1. In this case, objects in the fiber over 0 are isomorphic to even-length
sequences of alternating pushes and pulls f ˚ f˚ ¨ ¨ ¨ f ˚ f˚ 0 along the unique arrow f : 0 Ñ 1, while objects
in the fiber over 1 correspond to odd-length sequences f˚ f ˚ f˚ ¨ ¨ ¨ f ˚ f˚ 0. When we consider morphisms,it turns out that the fiber category BFibppq0 is equivalent to the (augmented) simplex category ∆ of finite
ordinals and order-preserving maps, under an interpretation reading the length 2n sequence f ˚ f˚ ¨ ¨ ¨ f ˚ f˚ 0
as the ordinal n “ t 0 ă 1 ă ¨ ¨ ¨ ă n ´ 1 u. Similarly, the fiber BFibppq1 is equivalent to the category ∆Kof finite non-empty ordinals and order-and-least-element-preserving maps.` In particular,from the sequent
˘forthenumber of maps
calculus for free bifibrations we can easily derive the well-known formula n`m´1mm Ñ n in ∆. It is also worth mentioning that in this case the total category of the free bifibration isequivalent BFibppq – Υ to the category of schedules Υ introduced by Harmer, Hyland, and Melliès [HHM07]
in their study of the categorical combinatorics of game semantics.
An even richer structure emerges considering the free bifibration over the functor p “ p˚ ÞÑ 0q : 1 Ñ Nsending the unique object of 1 to the initial object of the natural numbers considered as a posetal category
under the natural order. In this case, objects in the fiber of 0 are isomorphic to sequences of rising and falling
steps in N that start at 0 and end at 0. In other words, they correspond to Dyck paths! By the standard
bijection between Dyck paths and rooted planar trees, the fiber BFibppq0 may therefore be interpreted as acategory of trees, giving rise to an interesting notion of morphism of planar trees. Indeed, it turns out that
BFibppq0 is equivalent to a category of finite rooted planar trees that was defined in an entirely different
manner by Joyal [Joy97] and Batanin [Bat98], namely as the full subcategory of the functor category rNop , ∆sconsisting of those functors T : Nop Ñ ∆ such that T p0q “ 1 and such that T phq “ 0 for some h. Under
the Joyal-Batanin representation of planar trees, the ordinal T pnq counts the number of nodes of height nfrom the root, while the monotone functions T pn ` 1q Ñ T pnq map the nodes of height n ` 1 to their parent
nodes of height n (these functions are necessarily order-preserving by planarity). It turns out that naturaltransformations between such functors are in one-to-one correspondence with equivalence classes of zigzag
morphisms between the corresponding Dyck paths. In particular, we can enumerate natural transformations
between trees by enumerating focused derivations in the sequent calculus for the free bifibration. Finally, it
appears that we get some interesting combinatorics by fixing a tree T and considering the sequencesinrT sn “ #t α : T 1 Ñ T | |T 1 | “ n uoutrT sn “ #t α : T Ñ T 1 | |T 1 | “ n ucounting all of the morphisms into T or out of T and out of/into a tree of a given size.

References[Bat98]Michael Batanin. Monoidal globular categories as a natural environment for the theory of weakn-categories. Advances in Mathematics, 136:39–103, 1998.

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

3

[DPP03b] Robert Dawson, Robert Paré, and Dorette Pronk. Undecidability of the free adjoint construction.
Applied Categorical Structures, 11:403–419, 2003. doi:10.1023/A:1025712521140.
[HHM07] Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent
strategies. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July
2007, Wroclaw, Poland, Proceedings, pages 379–388. IEEE Computer Society, 2007. doi:10.
1109/LICS.2007.14.
[Joy97]

André Joyal. Disks, duality, and θ-categories. Unpublished, 1997. URL: https://ncatlab.org/nlab/files/JoyalThetaCategories.pdf.

[Lam10]François Lamarche. Path functors in Cat. Unpublished, 2010. URL: https://hal.inria.fr/hal-00831430.

[Lam14]

François Lamarche. Modeling Martin-Löf type theory in categories. Journal of Applied Logic,
12:28–44, 2014. doi:10.1016/j.jal.2013.08.003.

[MZ16]

Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of Lawvere’s presheaf
hyperdoctrine. In Proceedings of the 31st Annual IEEE Conference on Logic in Computer Science,
pages 555–564, July 2016.

[SS86]

Stephen Schanuel and Ross Street. The free adjunction. Cahiers de topologie et géométrie
différentielle catégoriques, 27(1):81–83, 1986.

4