The free bifibration on a functor

TL;DR

This paper develops a proof-theoretic construction of the free bifibration generated by a functor, connecting it to double categories, fibrations, and proof focusing, with applications to combinatorial categories.

Contribution

It introduces a novel proof-theoretic approach to constructing free bifibrations and extends to ambifibrations, providing normal forms, canonicity, and examples in combinatorics.

Findings

Constructed the free bifibration using a sequent calculus approach.

Established normal forms and a canonicity result for the construction.

Provided examples including categories of plane trees and forests as free fibrations.

Abstract

We consider the problem of constructing the free bifibration generated by a functor of categories $p : D \to C$. This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Par\'e, 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 : Bifib(p)\to C$ in which objects of $Bifib(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_ $\mathbb{Z}(C)$, which is also the free double category with companions and conjoints (or fibrant double category) on $C$. The approach adapts smoothly to the more general task of building $(P,N)$-fibrations, where one only asks for pushforwards along arrows in $P$ and pullbacks along arrows in $N$ for some subsets of arrows; this encompasses Kock and Joyal's notion of _ambifibration_ when $(P,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 $P$ and $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 for bicartesian squares.