The Synthetic Sierpinski Cone

以下是 Bakke、Sterling、Williams 和 Ye 所著论文《合成西尔平斯基锥》（"The Synthetic Sierpi´nski Cone"）的详细技术总结。

1. 问题陈述

本文探讨了合成数学（特别是同伦类型论，HoTT）中几何构造与偏映射的逻辑分类之间关系的一个基本张力。

• 经典重合性：在经典范畴论和域理论中，通过在空间 $X$ 下方粘合一个通用闭点而构造的西尔平斯基锥（$X_\perp$）等价于偏映射分类器（$L^\circ(X)$）。后者用于分类定义在开子空间上的偏映射。这种等价性是这些领域中逻辑与几何对偶性的基石。
• 合成障碍：在基于具有通用区间 $I$ 的 HoTT 的合成设定中，断言对于所有类型 $X$ 都有 $X_\perp \simeq L^\circ(X)$ 会导致理论的退化。具体而言，如果这种等价性普遍成立，它将迫使区间 $I$ 变为“余离散”（平凡），从而消除开子空间与闭子空间之间的区别，并使所有合成空间变得平凡。
• 核心问题：能否识别出一个非平凡的类型子宇宙，在其中西尔平斯基锥确实能够分类偏映射？这与合成高阶范畴论中现有的完备性概念（特别是Segal 完备性）有何关联？

2. 方法论

作者在单值基础（HoTT）框架内开展工作，不假设关于区间 $I$ 的强公理（例如它是严格线性序），也不全局使用模态算子，除非特定论证需要。他们利用了：

• 分配格：他们将理论参数化于一个有界分配格 $\Sigma$（代表“区间”$I$），而不是固定特定的模型。
• 定位理论：他们采用可及反射定位理论（遵循 Rijke 等人）来定义“完备”类型的子宇宙。
• 正交性：他们通过相对于特定类映射（角包含、锥等）的正交性来定义完备性。
• 映射柱：他们将西尔平斯基锥推广到开映射柱（或开显示柱），以处理类型的依赖族。
• 模态算子（有限使用）：他们简要使用了“全局点”模态算子（$\flat$）来分析全局点的指数性，而不会使内部逻辑坍缩。

3. 主要贡献与定义

A. 完备性层级

本文建立了类型完备性条件的严格层级，改进了 Pugh 和 Sterling 的工作：

1. Segal 完备：相对于内角包含 $\Lambda^2_1 \hookrightarrow \Delta^2$ 正交。这是合成 $\infty$-范畴的标准条件。
2. 基于 Segal 完备：相对于族包含 $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$ 正交。这是一个更强的条件。
3. 小西尔平斯基完备：相对于“小”比较映射 $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$ 正交。
4. 西尔平斯基完备：相对于所有 $X$ 的完整比较映射族 $\sigma_X: X_\perp \to L^\circ(X)$ 正交。

B. 主要等价性

作者证明了小西尔平斯基完备性等价于西尔平斯基完备性。

• 意义：Pugh 和 Sterling 此前仅证明了该等价性适用于 0-截断类型（集合）。本文将其扩展到未截断类型（高阶群胚/$\infty$-范畴），证明了相对于小的“小”映射检查正交性足以保证相对于所有映射的正交性。

C. Segal 完备性与基于 Segal 完备性的分离

本文解决了 Ulrik Buchholtz 的一个猜想，证明了在非平凡上下文中，Segal 完备性并不蕴含基于 Segal 完备性。

• 他们表明，如果每个 Segal 完备类型也是基于 Segal 完备的，那么区间 $I$ 将变为商初始（坍缩为双元素集），这与如单纯空间等标准模型的性质相矛盾。
• 这确立了“基于 Segal"条件严格更强，且对于西尔平斯基锥作为偏映射分类器发挥作用是必要的。

D. 映射柱与偏映射分类器

作者将西尔平斯基锥的结果扩展到开映射柱（$M^\circ_Y(f)$）。

• 他们证明，对于西尔平斯基完备类型，函数 $f: X \to Y$ 的开映射柱等价于相对偏映射分类器 $L^\circ_Y(f)$。
• 这为西尔平斯基完备类型子宇宙内的映射柱提供了一种新的“右向”泛性质。

4. 主要结果

1. 定理 64 与推论 66：一个类型是西尔平斯基完备的，当且仅当它是小西尔平斯基完备的。因此，西尔平斯基完备类型构成了一个可及反射子宇宙。
2. 推论 48/49/50：在标准模型（单纯空间、戴德金立方空间）中，基于 Segal 完备性严格强于 Segal 完备性。
3. 定理 75 与推论 77：西尔平斯基完备类型的子宇宙在形成相对开偏映射分类器下是封闭的。在该子宇宙内，开映射柱 $M^\circ_Y(f)$ 分类了配备纤维 $\text{fib}_f(y)$ 的开偏元素的点 $y:Y$。
4. 指数性：本文分析了全局点的指数性。结果表明，虽然全局点包含在经典意义上具有指数性，但在内部除非区间是平凡的，否则它们不是 $L_{Segal}$-指数性的。这突显了合成数学中内部性质与外部性质的区别。

5. 意义与应用

• 指称语义：在合成域理论中，偏性通常通过偏映射分类器单子 $L^\circ$ 建模。结果阐明，若要按情况定义依赖输入是否定义的惰性函数，其陪域必须是西尔平斯基完备的。这意味着任何支持此类惰性函数的合成域都必须满足 Segal 条件（路径传递性），且更严格地，必须满足基于 Segal 条件。
• 合成高阶范畴论：这项工作阐明了由初始对象生成的自由余完备性的结构。在合成 $\infty$-范畴中，西尔平斯基锥 $C_\perp$ 并不自动成为一个 $\infty$-范畴。然而，在西尔平斯基完备 $\infty$-范畴的反射子宇宙内，反射 $R(C_\perp)$ 等价于偏映射分类器 $L^\circ(C)$。这为这些特定上下文中的自由余完备性提供了一种可计算描述。
• 领域统一：本文成功统一了合成拓扑、域理论和高阶范畴论的概念。它表明，几何西尔平斯基锥与逻辑偏映射分类器之间的“重合”并非普遍定律，而是特定且行为良好的类型子宇宙的属性。
• 机械化：作者指出，他们的主要结果已在 Agda 证明助手中进行机械化，确保了类型论论证的严格正确性。

总之，本文通过识别几何构造（锥/柱）与逻辑分类（偏映射）对齐的精确条件（西尔平斯基完备性），解决了合成数学中的一个关键歧义，同时证明了这些条件严格强于合成 $\infty$-范畴的标准要求。