函子上的自由双纤维化 The free bifibration on a functor|functor|函子|序列|构造|纤维化

https://arxiv.org/pdf/2511.07314

函子上的自由双纤维化

The free bifibration on a functor

摘要

引言

序列演算

打开网易新闻查看精彩图片

在一般的序列演算中，可以定义一个推导为一个有限的根树，其边被标记为序列，其节点被标记为推理规则的有效实例。此外，可以区分开放和封闭的推导，其中开放推导的前提对应于树的开放边。封闭推导的另一个名称是证明。双纤维化序列演算的一个特殊性质是，每个推理规则最多有一个前提，因此推导是完全线性的（即，它们只是列表而不是适当的树），并且推导仅在由一个唯一的初始公理终止时才是封闭的。

1.6. 切割。从逻辑的角度来看，切割是任何逻辑中预期的规则，它确保推理序列可以按预期进行链式连接。Gentzen 发明序列演算背后的惊人洞察是切割规则在某种意义上是逻辑上多余的。证明这一点的原始方法是直接在推理系统中包含切割规则，然后展示切割消除：任何封闭的证明都可以在不使用切割规则的情况下重写。我们采用一种替代但几乎等效的方法，首先定义一个无切割的系统，然后展示切割规则是可接受的。回想一下，如果给定其前提的封闭推导，则推理规则是可接受的，那么其结论也有一个封闭推导。

该定义在推导的原始语法上表现出一些非确定性，因为可能会出现两个可交换的切割规则都适用的情况。我们认为它在排列等价（~）的意义上是定义良好的：每当上述几种情况中的几种适用时，从该定义中可以定义的所有推导都是排列等价的。

请注意，这只发生在左侧推导以左规则开始，右侧推导以右规则开始的情况下。有四对这样的关键对（可以以两种不同方式组合的推导形状），对应于生成器的所有四种排列。两对是彼此对称的，所以我们只需要检查三对。

1.9. 相关工作。有一个著名的构造，最初由 Gray [16] 提出，关于函子上的自由纤维化（或其对偶，自由 opfibration）作为逗号范畴。标准构造实际上定义了一个 split (op)fibration，在这个意义上，伪函子性法则 (1.10)–(1.12) 崩溃为严格等式，尽管一个人可以表示非 split 纤维化和 opfibrations 作为相应伪单子的伪代数（参见 Anders Kock [25] 的描述，以及 Emmenegger、Mesiti、Rosolini 和 Streicher 关于纤维化替代构造的最近工作 [15]）。相反，我们的构造产生了一个非 split 双纤维化，但可以通过限制为严格交替公式（见下文第 3.3 节，特别是备注 3.4）恢复接近 split 双纤维化的东西。值得一提的是，由于一个函子在既是纤维化又是 opfibration 的情况下才是双纤维化，自由双纤维化单子范畴在形式上是自由纤维化和自由 opfibration 单子范畴的余积——但这种表征并没有在显式构造中提供太多帮助。