显示类型理论与半单纯类型的共归纳定义：迈向高阶范畴的无穷相干结构

《Mathematical Structures in Computer Science》：Displayed type theory and semi-simplicial types

本文推荐Kolomatskaia和Shulman的研究，他们针对同伦类型理论无法定义无穷相干结构（如半单纯类型SST）的难题，提出了显示类型理论dTT。该理论通过引入离散和单纯两种模态，并利用显示原语和共归纳定义，首次在类型论内部完整定义了半单纯类型SST，其语义可解释于任意(∞,1)-topos。这项工作为在类型论中合成地处理高阶范畴理论等复杂结构奠定了基础。

　　

在同伦类型理论（Homotopy Type Theory, HoTT）的广阔图景中，一个长期存在的挑战如同顽固的礁石，阻碍着研究者驶向更高阶数学结构的深海：即如何在其框架内定义“无穷相干”的结构。诸如A_∞-空间或(∞,1)-范畴等复杂对象，在经典同伦论中可借助点集层面的严格等式轻松构建，但在重视“等价”而非“严格相等”的HoTT中，所有定义无穷结构的尝试似乎都陷入了某种循环：描述一致性需要无限结构，而定义该结构本身又需要无限的一致性条件。

在众多备受关注的无穷结构中，半单纯类型（Semi-Simplicial Types, SST）因其在编码其他无穷相干结构方面的潜力而成为焦点。一个半单纯类型可以直观地理解为一个无限维的几何对象：它包含点的类型（0-单形）、点之间线的类型（1-单形）、三个点及其边界线所围成三角形的类型（2-单形），如此递推至任意维度的单形。传统的思路是试图将这种无限层级的依赖关系编码为一个巨大的记录类型，但直接在HoTT内部实现这一点异常困难，仿佛试图抓住自己的影子。

为了突破这一瓶颈，研究者们曾提出多种增强型类型理论。双层次类型理论（Two-Level Type Theory, 2LTT）引入了非同伦不变的“外层次”和严格的“外相等”类型，但实际操作繁琐。单纯类型理论（Simplicial Type Theory, STT）则改变了视角，将类型本身视为单纯对象并公理化其性质，但其能力受限于公理系统的表达范围。

在此背景下，Astra Kolomatskaia和Michael Shulman在《Mathematical Structures in Computer Science》上发表了他们的研究成果，提出了第三条路径：显示类型理论（Displayed Type Theory, dTT）。dTT的核心思想巧妙而深刻：它部分内化了“一元参数化”的思想。参数化通常作为一个元定理出现，断言每个类型都配备有某种关系（例如“可计算性见证”），并且每个函数都保持这些关系。dTT通过引入一个称为“显示”（display）的原语操作^d，将这种关系内化为类型理论本身的一部分。对于一个类型A，其显示A^d可以理解为依赖于A中元素的“关系”或“见证”的类型。特别地，dTT包含了离散（dm）和单纯（sm）两种模式，通过模态（modality）来控制和区分在不同模式下工作的类型和项。

dTT最引人注目的成就在于，它使得半单纯类型SST的一个优雅的共归纳（coinductive）定义成为可能。这个定义直击几何本质：一个半单纯类型A由一个0-单形的类型Z A，以及对于每个0-单形x: Z A，一个在A上“显示”的半单纯类型S A x（称为A在x上的切片）共同构成。这个定义巧妙地利用了“(n+1)-单形是n-单形的锥”这一几何事实。通过共归纳原理，可以从一个“状态空间”Υ和指定的“头”函数（提供0-单形）与“尾”函数（提供高维单形的生成方式）来构造SST的元素。

为了从语义上支撑dTT及其对SST的定义，研究者构建了一个模型。该模型从一个满足特定条件的普通依赖类型理论模型??（离散模式）出发，通过考虑??上的Reedy纤维化增强半单纯图（即单纯模式的对象），构造出了dTT的模型。在这个模型中，SST被解释为半单纯对象的分类器，从而确保了其定义的普遍性和正确性。

本研究的关键技术方法主要包括：1) 构建多模态类型理论框架，明确区分离散模式与单纯模式，并定义模态之间的转换关系（如△, ◇, □）；2) 引入显示操作^d及其相关结构（如décalage），并精确规定其在各种类型构造子（如Π类型、宇宙）上的计算规则；3) 定义并处理“望远镜”（telescopes）和“元抽象”（meta-abstractions）等复杂上下文结构，以严谨表述依赖关系；4) 利用共归纳原理定义“显示的共归纳类型”（displayed coinductive type），并以SST作为其核心实例。

SST的共归纳定义

研究的核心是给出SST的共归纳定义。具体地，类型SST由两个析构器（destructor）刻画：

• •
  Z : SST → Type_?，用于提取一个半单纯类型的0-单形类型。
• •
  S : (A : SST) → Z A → SST^dA，对于半单纯类型A及其一个0-单形x: Z A，给出一个在A上“显示”的半单纯类型S A x。
  这个定义是共归纳的，意味着SST是满足上述性质的最大类型。通过迭代应用S和Z，可以逐层恢复出半单纯类型的所有单形层次。例如，A₁x₀₁x₁₀可以定义为 Z^d(S A x₀₁) x₁₀，即1-单形的类型。这种定义方式使得SST的元素在语义上对应于Reedy纤维化的增强半单纯对象。

显示结构及其应用

dTT的显示操作^d会自动为任何可定义的结构生成其“显示”版本。例如，对于范畴的记录类型定义应用显示操作，会得到“显示范畴”的记录类型，其对象和态射都依赖于底范畴的相应结构。这为模块化地构造复杂范畴和证明其性质提供了便利。研究展示了如何利用dTT定义一些基本的半单纯类型操作，如奇异半单纯类型（由拓扑空间生成）、范畴的脉（nerve）、拓扑奇异复形以及点化的半单纯类型和半单纯类型之间的态射。这些例子表明，基于dTT和SST的共归纳定义，可以进行实际的数学工作。

语义模型构建

为了确保dTT的合理性，研究者在范畴论层面构建了其语义模型。关键步骤是通过一个ω-极限过程来构造显示的共归纳类型的终端余代数。这个过程涉及构建一个塔序列，其中每一层通过一个拉回构造来逼近最终的共归纳类型。研究者证明了在适当的条件下（如涉及的映射是Quillen预纤维化），该序列的极限即为所需的终端余代数。这一构造为dTT中的共归纳定义，特别是SST，提供了坚实的数学基础。

结论与意义

Kolomatskaia和Shulman的这项工作在类型理论领域取得了重要进展。它所提出的显示类型理论dTT，通过巧妙地部分内化参数化并利用模态控制，成功地在类型论内部定义了半单纯类型SST这一关键的无穷相干结构。这不仅解决了HoTT中的一个长期难题，更重要的是，它为在类型论中“合成地”处理高阶范畴论、同伦代数等需要无穷相干性的数学领域开辟了一条新的道路。由于dTT的语义可以建立在任意的(∞,1)-topos之上，这使得其结果具有很高的普遍性。此外，文中发展的显示共归纳类型、望远镜技术以及对模态和参数化的处理方式，本身也是对类型理论本身的重要发展。未来，随着基于dTT的证明辅助工具的实现及其在更高阶数学结构中的应用探索，这一工作有望对形式化数学和同伦论的基础产生深远影响。