https://arxiv.org/pdf/2511.07314

函子上的自由雙纖維化

The free bifibration on a functor

摘要

引言

1. 序列演算

   
   

在一般的序列演算中，可以定義一個(gè)推導(dǎo)為一個(gè)有限的根樹(shù)，其邊被標(biāo)記為序列，其節(jié)點(diǎn)被標(biāo)記為推理規(guī)則的有效實(shí)例。此外，可以區(qū)分開(kāi)放和封閉的推導(dǎo)，其中開(kāi)放推導(dǎo)的前提對(duì)應(yīng)于樹(shù)的開(kāi)放邊。封閉推導(dǎo)的另一個(gè)名稱是證明。雙纖維化序列演算的一個(gè)特殊性質(zhì)是，每個(gè)推理規(guī)則最多有一個(gè)前提，因此推導(dǎo)是完全線性的（即，它們只是列表而不是適當(dāng)?shù)臉?shù)），并且推導(dǎo)僅在由一個(gè)唯一的初始公理終止時(shí)才是封閉的。

1.6. 切割。從邏輯的角度來(lái)看，切割是任何邏輯中預(yù)期的規(guī)則，它確保推理序列可以按預(yù)期進(jìn)行鏈?zhǔn)竭B接。Gentzen 發(fā)明序列演算背后的驚人洞察是切割規(guī)則在某種意義上是邏輯上多余的。證明這一點(diǎn)的原始方法是直接在推理系統(tǒng)中包含切割規(guī)則，然后展示切割消除：任何封閉的證明都可以在不使用切割規(guī)則的情況下重寫(xiě)。我們采用一種替代但幾乎等效的方法，首先定義一個(gè)無(wú)切割的系統(tǒng)，然后展示切割規(guī)則是可接受的?；叵胍幌?，如果給定其前提的封閉推導(dǎo)，則推理規(guī)則是可接受的，那么其結(jié)論也有一個(gè)封閉推導(dǎo)。

該定義在推導(dǎo)的原始語(yǔ)法上表現(xiàn)出一些非確定性，因?yàn)榭赡軙?huì)出現(xiàn)兩個(gè)可交換的切割規(guī)則都適用的情況。我們認(rèn)為它在排列等價(jià)（~）的意義上是定義良好的：每當(dāng)上述幾種情況中的幾種適用時(shí)，從該定義中可以定義的所有推導(dǎo)都是排列等價(jià)的。

請(qǐng)注意，這只發(fā)生在左側(cè)推導(dǎo)以左規(guī)則開(kāi)始，右側(cè)推導(dǎo)以右規(guī)則開(kāi)始的情況下。有四對(duì)這樣的關(guān)鍵對(duì)（可以以兩種不同方式組合的推導(dǎo)形狀），對(duì)應(yīng)于生成器的所有四種排列。兩對(duì)是彼此對(duì)稱的，所以我們只需要檢查三對(duì)。

1.9. 相關(guān)工作。有一個(gè)著名的構(gòu)造，最初由 Gray [16] 提出，關(guān)于函子上的自由纖維化（或其對(duì)偶，自由 opfibration）作為逗號(hào)范疇。標(biāo)準(zhǔn)構(gòu)造實(shí)際上定義了一個(gè) split (op)fibration，在這個(gè)意義上，偽函子性法則 (1.10)–(1.12) 崩潰為嚴(yán)格等式，盡管一個(gè)人可以表示非 split 纖維化和 opfibrations 作為相應(yīng)偽單子的偽代數(shù)（參見(jiàn) Anders Kock [25] 的描述，以及 Emmenegger、Mesiti、Rosolini 和 Streicher 關(guān)于纖維化替代構(gòu)造的最近工作 [15]）。相反，我們的構(gòu)造產(chǎn)生了一個(gè)非 split 雙纖維化，但可以通過(guò)限制為嚴(yán)格交替公式（見(jiàn)下文第 3.3 節(jié)，特別是備注 3.4）恢復(fù)接近 split 雙纖維化的東西。值得一提的是，由于一個(gè)函子在既是纖維化又是 opfibration 的情況下才是雙纖維化，自由雙纖維化單子范疇在形式上是自由纖維化和自由 opfibration 單子范疇的余積——但這種表征并沒(méi)有在顯式構(gòu)造中提供太多幫助。

原文鏈接：https://arxiv.org/pdf/2511.07314