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 : 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 $ω$, 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 for bicartesian squares.

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