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é, 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 $Λ_p : Bif(p)\to C$ in which objects of $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_ $\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, which 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 $ω$, and a category of increasing forests generated as a free ambifibration over $Δ$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition.

翻译：我们考虑由范畴函子$p : D \to C$生成自由双纤维化的构造问题。该问题先前由Lamarche考虑，并与Dawson、Paré和Pronk研究的"自由伴随函子"问题密切相关。我们为该问题发展了一种证明论方法，首先构造自由双纤维化$Λ_p : Bif(p)\to C$，其中$Bif(p)$的对象是原始"双纤维化逻辑"的公式，箭头是在无切割相继式演算中模置换等价关系的推导。我们证明，将构造实例化为恒等函子会生成一个_之字形双范畴_$\mathbb{Z}(C)$，它同时也是$C$上具有伴随与共伴随（或纤维化双范畴）的自由双范畴。该方法可平滑地推广到构建$(P,N)$-纤维化这一更一般的任务，其中仅要求沿$P$中箭头的推出和沿$N$中箭头的拉回（针对某些箭头子集），当$(P,N)$构成因子分解系统时，这包含了Kock与Joyal提出的_双性纤维化_概念。我们基于证明论中的_聚焦_思想，建立了一系列逐步增强的正规形式，并在基范畴相对于$P$和$N$为因子分解预序的假设下获得了典范性结果。该典范性结果使我们能够判定字问题并无重复地枚举相对态射集。最后，我们描述了若干组合性质的例子，包括作为$ω$上自由双纤维化生成的平面树范畴，以及作为$Δ$上自由双性纤维化生成的递增森林范畴，后者通过Beck-Chevalley条件将其纤维的非交叉划分格包含为商。