The internal languages of univalent categories

技术摘要：单价范畴的内部语言

问题陈述
范畴逻辑中的内部语言定理建立了语法（类型论）与语义（范畴模型）之间的等价关系。Clairambault 和 Dybjer [CD14] 的一项开创性结果修正了 Seely 最初的定理 [See84]，建立了局部笛卡尔封闭范畴（LCCCs）的二范畴与支持外延恒等类型、$\Sigma$-类型和 $\Pi$-类型的民主范畴与族（CwFs）的二范畴之间的双等价关系。

然而，该结果是在集合论基础上制定的。在单价基础（同伦类型论）中，标准的 CwF notion 面临一个根本性的障碍：单价公理意味着集合的类型本身不是一个集合（它是一个 1-类型）。因此，CwF 中“上下文中的类型集合构成一个集合”的要求被违反了，因为集合的单价范畴并不满足这一点。此外，“选定”结构（例如分裂纤维化）与“存在”结构（例如同构意义下的极限）之间的区别在集合论基础中产生了相干性问题，这需要选择公理或严格化程序。在单价基础中，由于同构蕴含恒等，这些区别消失了，但现有的 CwF 框架并不能直接适用。

方法论
本文开发了一个在单价基础内进行范畴语义的新框架，利用单价范畴和理解范畴（comprehension categories）而非 CwF。

1. 单价范畴： 作者研究的是对象恒等类型与同构（伴随等价）等价的范畴。这允许将伴随等价视为恒等，从而简化了关于结构保持（例如指数）的证明，并消除了对选择极限所需的选择公理的需求。
2. 理解范畴： 为了在不需要类型构成集合的情况下建模依赖类型，本文采用了理解范畴（基于纤维化和显示范畴）。理解范畴由一个上下文的基范畴、一个类型的显示范畴、一个提供替换的切分（cleaving）以及一个理解函子组成。作者将注意力限制在单价全理解范畴上，其中基范畴和显示范畴都是单价的。
3. 显示二范畴： 构建模型的二范畴高度依赖于显示二范畴 [AFM+21]。这种模块化方法允许作者通过在更简单的基二范畴之上叠加属性（例如有限极限、$\Pi$-类型、宇宙）来构建复杂的二范畴（如 LCCCs 或带有宇宙的拓扑斯）。这种模块化促进了证明所构建的二范畴本身是单价的。
4. 局部属性： 为了将从具有有限极限的范畴到更复杂结构（如拓扑斯）的结果进行扩展，本文改编了 Maietti 关于局部属性 [Mai05] 的概念。局部属性是关于切片下封闭的范畴的条件。作者在显示二范畴框架内将其形式化，以将双等价关系从基情况（有限极限）扩展到各种类别的拓扑斯。
5. 重索引与宇宙： 对于宇宙的处理，本文采用了显示二范畴的重索引。这种技术允许将来自基范畴的双等价关系转移到其上的显示范畴，从而能够定义在特定类型构造器（如 $\Sigma$、$\Pi$、自然数）下封闭的宇宙，而无需严格的稳定性法则，而是基于同构的稳定性（这在单价范畴中变为恒等）。

主要贡献
本文做出了四个主要贡献：

1. Clairambault-Dybjer 的单价模拟： 作者构建了具有有限极限的单价范畴的二范畴与单价全民主有限极限（DFL）理解范畴的二范畴之间的双等价关系。这确立了具有有限极限的单价范畴的内部语言是带有单位、二元积和 $\Sigma$-类型的外延 Martin-Löf 类型论。
2. 向局部笛卡尔封闭范畴的扩展： 该双等价关系被扩展到支持 $\Pi$-类型的单价局部笛卡尔封闭范畴和 DFL 理解范畴。这证实了单价 LCCC 的内部语言是带有 $\Pi$-类型的外延 Martin-Löf 类型论。
3. 向拓扑斯和宇宙的扩展： 通过局部属性，该方法被推广到各类拓扑斯（前拓扑斯、$\Pi$-前拓扑斯、初等拓扑斯以及带有自然数对象的拓扑斯）。此外，作者在这些范畴中定义了在类型构造器（自然数、子对象分类器、命题重缩放、$\Sigma$-类型和 $\Pi$-类型）下封闭的宇宙，建立了对于带有宇宙的初等拓扑斯的双等价关系。
4. 形式化： 所有构造和证明都在 Rocq 证明助手中利用 UniMath 库进行了形式化，确保了正确性，并为该理论提供了机器检查的参考。

结果
本文证明了对于各类单价范畴，存在与其对应的单价理解范畴类的双等价关系。具体而言：

• 有限极限： 具有有限极限的单价范畴 $\simeq$ DFL 理解范畴（单位、积、等化器、$\Sigma$）。
• LCCC： 单价 LCCC $\simeq$ 具有 $\Pi$-类型的 DFL 理解范畴。
• 拓扑斯： 单价初等拓扑斯（带/不带 NNO）$\simeq$ 具有相应局部属性（如子对象分类器、不交和、商）的 DFL 理解范畴。
• 宇宙： 带有特定类型构造器封闭宇宙的单价初等拓扑斯 $\simeq$ 满足相应封闭条件的宇宙对象的 DFL 理解范畴。

本文表明，在单价基础中，这些范畴结构的内部语言是外延 Martin-Löf 类型论。使用单价范畴通过移除对分裂纤维化的需求和选择公理，简化了理论；在单价基础中，由于同构即恒等，解决了一直困扰集合论模型的相干性问题（即替换必须严格成立的问题）。

意义与主张
本文声称其发展提供了对依赖类型论语义的新视角。通过利用单价范畴，作者避免了在集合论基础中为了确保健全性而必须使用的分裂纤维化和选择公理的技术开销。单价基础中固有的结构恒等原则允许更自然地处理对象在等价意义下而非严格相等意义下被识别的范畴结构。

作者明确指出，本文并非构建语法或初始模型，而是专注于范畴侧的内部语言定理（模型之间的等价关系）。作者指出，虽然理解范畴适用于单价基础，但其他结构如 CwF 则不然，因为 CwF 对类型存在集合限制。本文的意义在于建立了一个稳健的、经机器检查的单价范畴结构与类型论之间的对应关系，证明了单价基础可以在不具备早期集合论表述中所发现的缺陷的情况下，自然地支持这些内部语言定理。