Strict stability of extension types

技术摘要：扩展类型的严格稳定性

问题陈述
本文解决了 Riehl 和 Shulman 引入的同伦类型论（HoTT）系统中，在合成开发 $(\infty, 1)$-范畴过程中存在的一个基础性空白。虽然该系统的语义已使用单纯形同伦论和 Segal 空间模型进行了初步勾勒，但原始表述并未证明扩展类型（extension types）在替换（substitution）下的严格稳定性（strict stability）。在类型论模型中，“严格稳定性”要求类型构造器（如扩展类型）的解释与拉回（即替换）严格交换，而非仅仅在同构或同伦意义下交换。若缺乏这一性质，该系统将无法在 $\infty$-topos 的内部语言中得到完全解释，从而无法支持某些内部范畴论（例如 Martini–Wolf 的范畴论）所要求的严格相等性。

方法论
作者采用了由 Voevodsky 最初描述、后由 Lumsdaine 和 Warren 对局部全集（local universes）进行推广的分裂方法（splitting method）。该方法涉及以下技术步骤：

1. 全集范畴（Universe Categories）： 本研究置于一个全集范畴内（一个配备了全集对象 $U$ 和通用纤维化 $\pi: \tilde{U} \to U$ 的范畴 $\mathcal{C}$）。作者假设存在一个“分裂”，即全集纤维化的全局拉回方阵的选择。这确保了重索引（即替换）被建模为对象和态射的严格相等，而非仅仅是同构。
2. 生成上下文（Generic Contexts）： 遵循 Awodey 关于自然模型的研究风格，本文定义了用于扩展类型构造与引入的生成上下文（分类对象）：
   • $U_{\text{Ext}@j}$ 被定义为分类一对类型族 $A$ 以及在形状包含 $j: \phi \hookrightarrow \psi$ 之上的偏截面 $a$ 的对象。
   • $U_{\lambda@j}$ 被定义为分类三元组 $\langle A, a, b \rangle$ 的对象，其中 $b$ 是 $a$ 的全扩展。
3. 严格拉回构造： 作者将扩展类型构造器 $\text{Ext}@j$ 和引入映射 $\lambda@j$ 构建为这些生成上下文与全集之间的态射。通过利用全集纤维化的分裂，本文证明了由这些映射构成的方阵是一个严格拉回（而非仅是弱拉回）。
4. 纤维性假设（Fibrancy Assumptions）： 为了在保持对标准模型（$\infty$-topos 中的单纯对象）适用性的同时简化技术设置，作者假设“形状”（单纯上下文）是纤维的。这确保了 Leibniz 伴随张量（Leibniz cotensors）是纤维化，从而允许扩展类型被建模为普通的 1-范畴拉回。

主要贡献与结果
其主要贡献是定理 3.8，该定理确立了扩展类型的严格稳定性。该定理证明，对于一个类型论模型 $\mathcal{E}$ 及其关联的单纯模型 $s\mathcal{E}$，一个固定的标准类型构造器的分裂，能够产生一个满足以下对于任何上下文态射 $\sigma: \Delta \to \Gamma$ 均成立的严格相等性的扩展类型解释：

1. 构造稳定性： $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. 引入稳定性： $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. 消去稳定性： $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

论文进一步详细阐述了在这一严格稳定框架内 $\beta$- 与 $\eta$- 计算规则是如何被满足的，这依赖于由分裂定义的拉回方阵的普遍性质。

意义与主张
本文声称该结果解决了 Riehl–Shulman 系统中关于扩展类型严格性的开放问题。其实际意义在于，该系统现在拥有了在 $\infty$-topos 的单纯对象中的鲁棒语义。这使得使用该系统来证明关于 Martini–Wolf 意义下的内部 $\infty$-范畴的定理成为可能，因为严格稳定性确保了类型论操作与内部范畴论所要求的范畴拉回完美对齐。

作者指出，尽管为了技术简化而假设了单一全集和纤维化形状，但该推理过程被认为可以推广到全集层级以及更复杂的纤维结构，而不会遇到本质性的障碍。这项工作搭建了单纯式 HoTT 的合成语法与 $\infty$-topos 严谨语义之间的桥梁。