Polynomial Universes in Homotopy Type Theory

1. 研究背景与问题 (Problem)

核心问题：依赖类型理论的范畴语义中的“严格性”难题
依赖类型理论（Dependent Type Theory, DTT）的范畴语义通常面临一个根本性的困难：类型理论中的语法操作（如替换 substitution）是严格结合且严格满足 Beck-Chevalley 条件的。然而，在传统的范畴语义（如预层范畴 $Set^{C^{op}}$）中，这些操作通常通过拉回（pullback）来实现，而拉回在一般范畴中仅满足同构意义下的结合律（associative up to isomorphism），而非严格相等。

现有方案的局限性
Awodey 和 Newstead 提出的“自然模型”（Natural Models）通过引入“类型宇宙”（Type Universe）的概念，将类型视为展示映射（display maps），从而在某种程度上解决了严格性问题。然而，为了处理自然模型中需要“同构意义下相等”而非“严格相等”的高阶结构（higher coherences），他们被迫构建了一个复杂的**三范畴（tricategory）**多项式函子。这种从普通范畴向高阶范畴的跃迁使得理论变得极其复杂，且难以形式化。

本文试图解决的问题
如何在普通的多项式函子范畴内，完全公理化地描述依赖类型理论的范畴语义，同时自然地处理所有必要的高阶相干性（higher coherences），而无需引入额外的复杂高阶范畴结构？

2. 方法论 (Methodology)

本文采用了一种基于**同伦类型论（Homotopy Type Theory, HoTT）**的合成方法（synthetic approach）。

1. 工作语言转换：
   作者将工作背景从传统的 1-拓扑斯（如 $Set^{C^{op}}$）转移到了 HoTT 的语境下，具体是在 $\infty$-预层范畴 $\infty\text{Grpd}^{C^{op}}$ 内部工作。在 HoTT 中，所有结构天然地具有高阶同伦性质。

2. 多项式函子（Polynomial Functors）的重新定义：
   在 HoTT 内部，多项式函子 $P$ 被定义为形如 $P(y) = \sum_{x:A} y^{B[x]}$ 的自函子，其中 $A$ 是类型，$B$ 是依赖类型族。这对应于自然模型中的宇宙 $U$ 和展示映射 $u: U^\bullet \to U$。

3. 引入“多项式宇宙”（Polynomial Universes）：
   作者定义了一个关键概念：多项式宇宙。一个多项式函子 $u$ 被称为“单值的”（univalent），如果它是范畴 $\text{Poly}^{\text{Cart}}$（由多项式函子和笛卡尔透镜组成的范畴）中的次终端对象（subterminal object）。

   • 这意味着：对于任何多项式 $p$，从 $p$ 到 $u$ 的笛卡尔透镜（Cartesian lenses）构成的类型是一个“纯命题”（mere proposition），即任意两个这样的透镜都是相等的。
   • 这一性质直接对应于 HoTT 中的单值公理（Univalence Axiom）。

4. 利用单值性推导高阶相干性：
   这是本文方法论的核心创新。作者指出，一旦 $u$ 是单值的（univalent），那么任何以 $u$ 为终点的笛卡尔透镜之间的所有路径（即所有高阶相干性）都自动相等。因此，不需要显式地指定无穷多的相干数据，单值性公理隐式地保证了所有高阶幺半群（$\infty$-monad）和分配律（distributive laws）的相干性。

3. 关键贡献 (Key Contributions)

A. 在普通范畴内公理化依赖类型语义

论文证明了依赖类型理论的所有结构（包括 $\Sigma$ 类型、$\Pi$ 类型、单位类型等）都可以在普通的多项式函子范畴（$\text{Poly}$）中通过定义特定的透镜（lenses）来公理化，而无需像 Awodey-Newstead 那样构建复杂的三范畴。

B. 定义“多项式宇宙”与单值性

提出了“多项式宇宙”的概念，即满足单值性条件的多项式函子。

• $\Sigma$ 类型（依赖和）：对应于 $u$ 上存在一个笛卡尔透镜 $\mu: u \triangleright u \to u$（其中 $\triangleright$ 是多项式函子的复合）。
• $\Pi$ 类型（依赖积）：对应于 $u$ 上存在一个笛卡尔透镜 $\pi: u \Uparrow u \to u$（其中 $\Uparrow$ 是作者定义的新算子，用于处理依赖函数）。

C. 揭示 $\Pi$ 类型与分配律的深层联系

论文建立了一个深刻的对应关系：

• 一个多项式宇宙 $u$ 对 $\Pi$ 类型封闭，等价于 $u$（视为幺半群）存在一个自分配律（distributive law over itself）。
• 具体来说，$\Pi$ 类型的存在性导出了 $u \triangleright u \to u \triangleright u$ 的分配律，这对应于依赖积对依赖和的分配律：$\Pi x:A. \Sigma y:B[x]. C[x,y] \simeq \Sigma f: \Pi x:A. B[x]. \Pi x:A. C[x, f(x)]$。

D. 形式化验证

所有主要结果（包括定理 4.1 和 4.2）都在 Agda 证明助手（基于 HoTT）中完成了形式化。这证明了该理论不仅数学上严谨，而且在计算机辅助证明中是可行的。

4. 主要结果 (Results)

1. 定理 4.1（$\Sigma$ 类型的相干性）：
   如果 $u$ 是一个多项式宇宙，且存在笛卡尔透镜 $\eta: y \to u$（单位）和 $\mu: u \triangleright u \to u$（乘法），那么 $u$ 自动构成一个 $\infty$-幺半群（$\infty$-monad）。

   • 机制：由于 $u$ 的单值性，所有满足幺半群公理（结合律、单位律）的笛卡尔路径都是相等的，因此无需显式验证高阶相干图。

2. 定理 4.2（$\Pi$ 类型的分配律）：
   如果 $u$ 是一个多项式宇宙，且存在笛卡尔透镜 $\pi: u \Uparrow u \to u$，那么 $u$ 上存在一个自分配律 $\aleph: u \triangleright u \to u \triangleright u$。

   • 机制：作者引入了“跳跃结构”（jump structure）和“分配器”（distributor）的概念，将 $\Uparrow$ 算子的性质转化为分配律的公理。同样，利用 $u$ 的单值性，证明了分配律所需的所有高阶相干图自动交换。

3. 具体实例分析：

   • 部分性单子（Partiality Monad）：当宇宙 $U$ 为命题类型（Prop）时，对应的多项式函子即为部分性单子。
   • 列表单子与 Rezk 完备化：
     • 普通的列表单子（List）不是单值的，因此不满足 $\Pi$ 类型的分配律。
     • 通过 Rezk 完备化（Rezk Completion），可以将列表单子提升为单值多项式宇宙（对应于有限集 Bishop finite sets）。
     • 结果：Rezk(List) 拥有自分配律，其代数结构对应于交换幺半群（commutative monoid）。
     • 推论：Rezk(List) $\triangleright$ Rezk(List) 构成一个新的单子，作者推测其对应于交换环（commutative ring）的高阶范畴类比。

5. 意义与影响 (Significance)

1. 理论简化：
   本文极大地简化了自然模型（Natural Models）的理论框架。它消除了对复杂高阶范畴（如三范畴）的依赖，将依赖类型理论的语义完全封装在 HoTT 语境下的普通多项式函子范畴中。

2. 统一视角：
   通过单值性公理，将类型理论中的“严格性”要求与 HoTT 中的“同伦”性质统一起来。单值性不仅是一个公理，更是解决类型理论语义中“严格性 vs. 弱相等”矛盾的关键机制。

3. 代数结构的发现：
   揭示了依赖类型构造子（特别是 $\Pi$ 类型）与高阶代数结构（如分配律、交换环）之间的深刻联系。特别是关于 Rezk(List) 作为“自由交换环单子”的猜想，为高阶范畴代数提供了新的研究方向。

4. 形式化可行性：
   论文展示了 HoTT 作为形式化依赖类型理论语义的理想环境。通过 Agda 的形式化，证明了这些复杂的数学结构可以在计算机中精确构建和验证，为未来的类型理论实现和证明助手开发提供了理论基础。

总结：
这篇论文通过引入“多项式宇宙”和利用 HoTT 的单值性，成功地在普通范畴框架内解决了依赖类型理论语义中的高阶相干性问题。它不仅简化了现有理论，还揭示了类型构造子与高阶代数结构之间令人惊讶的对应关系，是类型理论与范畴论交叉领域的重要进展。