A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

这是一份关于论文《具有显式宇宙多态性的类型理论的广义代数理论》（A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism）的详细技术总结。

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

在类型理论（Type Theory）的研究中，特别是涉及**宇宙多态性（Universe Polymorphism）**时，传统的基于语法和推理规则（Grammar and Inference Rules）的表述方式存在局限性：

• 语法细节的干扰：传统的表述包含大量的语法选择、变量命名约定以及繁琐的“记账”规则（如等式规则），这些细节掩盖了类型理论的高层数学结构。
• 初始性猜想（Initiality Conjecture）的挑战：Voevodsky 提出的初始性猜想旨在证明特定类型的推理规则系统生成的项模型（Term Model）是其对应模型范畴中的初始对象。然而，由于语法表述的细微差别（如显式替换与隐式替换），直接证明这一猜想非常困难且容易出错。
• 缺乏统一的抽象框架：目前缺乏一种统一的、基于范畴逻辑的方法来形式化不同类型的系统（如带有外部宇宙塔的类型理论与带有显式宇宙多态性的类型理论），以便能够生成通用的元理论结果。

本文旨在解决上述问题，通过**广义代数理论（Generalized Algebraic Theories, GATs）和带族范畴（Categories with Families, CwFs）**来重新表述 Martin-Löf 类型理论（MLTT）的两个变体，从而在抽象层面刻画其结构，并为初始性猜想提供严谨的代数基础。

2. 方法论 (Methodology)

作者采用了一种基于范畴逻辑和**广义代数理论（GATs）**的自顶向下方法：

• 广义代数理论 (GATs)：由 Cartmell 提出，是对多排序代数理论的推广，允许排序符号（sort symbols）和算子符号（operator symbols）具有依赖类型。GATs 能够以方程和算子的形式精确描述类型理论的规则，而无需具体的语法细节。
• 带族范畴 (CwFs)：作为类型理论的标准语义模型，CwFs 包含上下文范畴、类型族和项族。
• 核心策略：
  1. 将类型理论表述为 GAT。
  2. 利用 GAT 的通用性质，构造其初始模型（Initial Model）。
  3. 证明该初始模型同构于具体的语法项模型（无论是基于显式替换还是隐式替换）。
  4. 通过这种抽象，将具体的语法系统视为 GAT 的特定实例，从而分离出“语法实现”与“数学本质”。

3. 主要贡献与理论构建 (Key Contributions)

论文构建了两个具体的 GAT，分别对应两种不同的宇宙处理方式：

A. 带有外部宇宙塔的类型理论 ($\Sigma_{tower}$)

• 对应理论：Martin-Löf 类型理论，带有由外部自然数 $l \in \mathbb{N}$ 索引的宇宙塔 $U_l$。
• GAT 结构 ($\Sigma_{tower}$)：
  • 这是一个无穷 GAT（infinitary gat），因为宇宙塔是无限延伸的。
  • 基于 CwF，增加了小类型构造子（$\Pi, \Sigma, N_0, \dots$）的算子符号。
  • 增加了宇宙相关的算子：
    • 宇宙类型 $(U_l)_\Gamma$。
    • 解码映射 $T_l(a)$。
    • 宇宙编码的 $\Pi$ 类型构造子 $\Pi_{l,l'}$。
    • 宇宙包含映射 $(U^m_l)_\Gamma$（将 $U_l$ 的元素提升到 $U_m$）。
  • 方程：定义了解码方程（如 $T_{l \vee l'}(\Pi_{l,l'}(a,b)) = \Pi(T_l(a), T_{l'}(b))$）以及算子与替换的交换律。
• 模型构造：虽然 $\Sigma_{tower}$ 是无穷的，但作者通过将其视为有限子理论 $\Sigma_n$（截断到 $n$ 个宇宙）的并集，利用 GAT 初始模型的通用构造方法，证明了其初始模型 $T_{\Sigma_{tower}}$ 的存在性。

B. 带有显式宇宙多态性的类型理论 ($\Sigma_{up}$)

• 对应理论：Martin-Löf 类型理论，带有显式的宇宙层级判断（$l \text{ level}$）和内部索引的宇宙。
• 核心创新：引入了层级索引的 CwF（Level-indexed CwF）。
  • 基础结构：首先定义了一个单一类型 CwF (ucwf) 来表示层级（Levels），包含层级上下文、层级替换和层级项。
  • 层级索引：主 CwF 是一个从层级 ucwf 到 CwF 的预层（Presheaf）。即 $P: C^{op} \to CwF$，其中 $C$ 是层级上下文范畴。
  • 新排序符号：引入了层级等式排序（Level Equality Sort） leqn(l, l')。这是为了解决 GAT 中不能直接在假设中使用等式约束的问题。通过引入 leqn 和自反性算子 r(l)，可以将层级不等式（如 $l < m$）形式化为存在性证明。
• GAT 结构 ($\Sigma_{up}$)：
  • 这是一个有限 GAT（finitary gat）。
  • 包含层级索引的宇宙 $U_l$（其中 $l$ 是层级项）。
  • 包含层级索引的乘积（Level-indexed products）$[\alpha]A$，用于实现真正的宇宙多态性（即类型可以量化宇宙层级）。
  • 定义了层级替换与类型构造子、宇宙算子的交换律。

4. 结果 (Results)

1. 初始性证明：
   • 证明了 $\Sigma_{tower}$ 和 $\Sigma_{up}$ 的初始模型 $T_{\Sigma}$ 在各自的模型范畴（$CwF_{\Sigma}$）中是初始对象。
   • 展示了如何将这些 GAT 的初始模型“外部化”（Externalization），得到具体的项模型（如 $T_{tower}$ 和 $T_{up}$），这些模型分别对应于带有外部宇宙塔和显式宇宙多态性的具体类型理论。
2. 语法与代数的对应：
   • 详细描述了如何从基于隐式替换的语法（如 Agda 或标准 MLTT 语法）构建 CwF 模型，并证明其满足 GAT 的方程。
   • 对比了基于显式替换（Explicit Substitution）的通用构造与基于隐式替换（Implicit Substitution）的具体构造，表明两者在初始性上是等价的。
3. 层级等式的处理：
   • 成功地将层级等式（Level Equality）作为 GAT 中的一个排序符号处理，解决了在 GAT 框架下表达宇宙层级约束（如 $l < m$）的难题。证明了在初始模型中，层级等式排序的元素对应于通过代数推理（$\vee$ 和 $+$ 运算）得到的等式证明。

5. 意义与影响 (Significance)

• 对 Voevodsky 初始性猜想项目的贡献：
  • 本文提供了一种统一的框架来定义依赖类型理论。通过将类型理论视为 GAT，初始性不再依赖于特定的语法细节，而是 GAT 的内在属性。
  • 这为证明“项模型是初始对象”提供了更稳健的数学基础，有助于解决 Voevodsky 提出的关于一般化推理规则系统的初始性问题。
• 抽象与统一：
  • 通过 GAT 和 CwF，作者剥离了类型理论中繁琐的语法细节，突出了其核心的范畴结构。
  • 这种方法不仅适用于 MLTT，还可以推广到简单类型逻辑、谓词逻辑（通过索引 CwF）以及立方类型理论（Cubical Type Theory）。
• 与相关工作的联系：
  • 文章讨论了 GAT 与**逻辑框架（Logical Frameworks，如 LF, Dedukti）以及商归纳 - 归纳类型（QIITs）**的关系。
  • 指出 GAT 提供了一种不同于逻辑框架的编码方式（基于依赖类型而非 $\Pi$ 类型），并强调了 QIITs 作为 GAT 在依赖类型理论中的数据类型实现，两者在概念上紧密相关。
• 未来方向：
  • 为处理带有等式约束的宇宙多态性（Equational Constraints on Universe Levels）铺平了道路。
  • 为在证明助手（如 Agda）中形式化初始性证明提供了清晰的蓝图。

总结：
这篇文章通过将具有宇宙多态性的类型理论形式化为广义代数理论（GATs），成功地在抽象层面统一了两种不同的宇宙处理方式。它不仅为 Voevodsky 的初始性猜想提供了强有力的理论支持，还展示了如何利用范畴逻辑（CwFs）来消除语法细节的干扰，从而获得类型理论更本质、更通用的数学刻画。