💻 computer science

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

本文通过 M-类型和终极余代数，在同伦类型论中构建了满足斯科特（Scott）和阿塞尔（Aczel）反基础公理的非良基实质集合模型，并将这些公理扩展至单价实质集合论中的高阶类型层级，并提供了 M-类型恒等类型的刻画，所有结果均在 Agda 中进行了形式化。

原作者： Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

发布于 2026-07-01

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心图景：构建一个“旋转”集合的宇宙

想象你正在构建一个由物体（集合）组成的宇宙。在传统的数学方法中（称为“良基”集合论），每个物体都是由更小的物体构建而成的，而这些小物体又是由更小的物体构建的，一直向下追溯到虚无。这就像一座金字塔：你不能让一个方块悬浮在半空中；它必须支撑在下方的某个东西之上。

但如果你想构建一个允许物体“支撑自身”的宇宙呢？如果你想要一个盒子包含了它自己？或者一个由盒子组成的链条：盒子 A 在盒子 B 内部，盒子 B 在盒子 C 内部，而盒子 C 又在盒子 A 内部？在传统数学中，这是被禁止的，因为它会产生无限循环。在这篇论文中，作者们探索了如何使用一种被称为同伦类型论 (Homotopy Type Theory, HoTT) 的现代框架，来构建一个允许这些循环的数学宇宙。

这篇论文主要做了两件事：

它构建了一个允许循环的集合模型，遵循了一位名叫 Scott 的数学家所设定的规则。
它构建了另一个允许循环的集合模型，遵循了一位名叫 Aczel 的数学家所设定的规则。

工具箱：树、余代数与“展开”

为了理解他们的模型，请想象一棵树。

良基树（旧的方法）就像是族谱。它们有根、有枝干，最终会有叶子。它们是停止生长的。
非良基树（新的方法）可以像分形或镜子迷宫一样。一个分支可能会绕回到根部，再次成为根。或者一个分支可能会分裂成两个看起来与整棵树完全相同的分支。

作者们使用一个叫做余代数 (Coalgebras) 的概念来描述这些树。把余代数想象成一台“机器”，它告诉你如何观察一个节点并看到接下来的内容。

如果机器说“停止”，你就得到了一个叶子。
如果机器说“去往这些子节点”，你就有了分支。
如果机器说“去往一个实际上就是你自己的子节点”，你就有了循环。

论文提出了一个问题：什么样的“终极”机器才能描述所有可能的循环？

两种模型：Scott 对比 Aczel

作者们构建了两种不同的“终极机器”（数学模型）来处理这些循环。它们对应于两种不同的处理循环世界中“相等性”的哲学。

1. “镜像”模型 (Scott 的反基础公理)

类比： 想象一个镜子迷宫。如果你站在镜子前，你会看到一个倒影。如果这个倒影又在另一面镜子里，你就会看到倒影的倒影。
规则： 在这个模型中，两个物体被认为是“相等”的，如果它们的展开模式 (unfolding patterns) 看上去是一样的。如果你不断地打开一个集合的层级（就像剥洋葱或展开一棵树），如果分支的模式与另一个集合完全一致，那么它们就是同一个。
结果： 作者构建了一种特定类型的树结构（称为 $V^0_\infty$ ），它充当了这个模型。它是一个“不动点”，这意味着如果你对这个宇宙应用规则，你会得到同样的宇宙。
关键发现： 这个模型并不是严格意义上的“最终”或“终极”机器。它是一个“第三种选择”——它既不是起点（初始对象），也不是绝对的终点（终极对象）。它处于中间位置。它满足 Scott 的规则，这些规则对于如何识别循环更加严格。

2. “通用”模型 (Aczel 的反基础公理)

类比： 想象一本包含所有可能讲述的故事的“大师级目录”，其中甚至包括那些讲述自身的故事。
规则： 在这个模型中，任何图（由点和线组成的图像）都可以转化为一个集合。如果你有一个代表循环的图像，就会有一个唯一的集合与之完美匹配。
结果： 作者构建了一个用于此目的的“终极余代数 (Terminal Coalgebra)”。然而，为了构建这个特定的机器，他们必须使用一种特殊的、带有一定争议性的数学工具，称为命题缩减 (Propositional Resizing)。
- 什么是命题缩减？ 想象你有一个巨大的书籍库（命题）。这个工具允许你将整个图书馆缩小到可以放在一个书架上，且不会丢失任何故事。这是一个强大的捷径，使得这种构建成为可能。
关键发现： 这个模型满足 Aczel 的规则。它是“终极”对象，意味着它是这种规则下所能实现的、最完整的循环集合宇宙。

“同一性”谜题：是什么让两个事物变得相同？

论文的一个重要部分是解决一个棘手的谜题：我们如何知道两棵循环树实际上是同一个？

在标准数学中，如果两个东西看起来一样，它们就是相等的。但在一个有循环的世界里，情况会变得很奇怪。

作者发现，这两个循环树之间的“相等性”可以用另一种类型的树（一种“索引 M-类型/indexed M-type”）来描述。
隐喻： 想象你正在比较两个无限的分形。要证明它们是相同的，你不能只看整体图像；你必须比较每一个分支、每一个子分支、每一个子之子分支。论文提供了一个精确的配方（一种“特征化”方法），说明如何进行这种比较。他们证明了这些复杂循环的“相等性”本身就是一个有结构的、无限的对象。

成就总结

Scott 模型： 他们构建了一个允许循环的集合宇宙，其中相等性由“展开”树的形状决定。这是一个不动点，但不是绝对的“终极”对象。
Aczel 模型： 他们构建了一个允许循环的“终极”集合宇宙，其中任何图都可以转化为一个集合。这需要一个特殊的数学假设（命题缩减）。
“相等性”配方： 他们弄清楚了如何精确定义这些无限循环结构的“相同性”，证明了相等性本身就是另一种树结构。
形式化： 他们不仅仅是在纸上书写；他们在名为 Agda 的计算机程序中构建了这一切，该程序会检查每一个逻辑步骤以确保没有错误。

为什么这很重要？

这篇论文并不声称解决了现实世界的工程问题或医疗问题。相反，它解决了一个数学的基础性谜题。它表明，我们可以使用现代的同伦类型论语言，构建一个允许“圆圈”和“循环”存在的、一致且逻辑严密的宇宙。它弥合了经典集合论（禁止循环）与现代计算机科学逻辑（需要处理如流和转换系统等复杂循环数据结构）之间的鸿沟。

简而言之：他们构建了两个不同的“宇宙”，其中事物可以包含自身，证明了它们按照特定规则运行，并展示了如何准确判断两个这样的自包含事物是否真的相同。

技术摘要：同伦类型论中的终端余代数与非良基集合

问题陈述
本文解决了在同伦类型论（HoTT）中建模非良基实质集合（non-wellfounded material sets）的挑战。虽然通过高阶归纳类型（其中相等性为恒等类型）已成功在 HoTT 中建立了良基集合模型，但建模非良基集合（即可能包含自身或形成无限成员链的集合）在历史上一直依赖于集合论（setoids，其中相等性是一个独立的二元关系），而非恒等类型。作者旨在构造 HoTT 中的非良基集合模型，使相等性严格解释为恒等类型，从而将普遍余代数（universal coalgebra）和非良基集合论中的经典概念整合到 HoTT 所支持的高维结构中。具体而言，本文寻求构造受限幂集演算的终端余代数以模拟 Aczel 的反基础公理（AFA），并构造用于模拟 Scott 反基础公理（SAFA）的替代不动点。

方法论
作者采用了单价实质集合论（Univalent Material Set Theory）以及对宇宙类型上的 wild endofunctors 的余代数理论框架。其方法论涉及三种主要的底层技术途径：

迭代集合的对偶化： 作者通过对迭代集合（ $V^n$ ）的构造进行对偶化，构造了一个类型层级 $V^n_\infty$ 。虽然 $V^n$ 是受限幂集演算 $P^n$ 的初始代数，但 $V^n_\infty$ 被构造为 M-类型（即无限制幂集演算 $P^\infty$ 的终端余代数）的一个特定子类型。该子类型通过一个余归纳谓词（coinductive predicate）来定义，该谓词确保每个节点处的分支映射都被截断到特定层级。
恒等类型的特征化： 一个关键的技术步骤是特征化 M-类型的恒等类型。作者证明了 M-类型中两个元素之间的恒等类型等价于一个索引 M-类型（具体而言，是源自“展开”关系的索引多项式演算的终端余代数）。这种特征化对于证明所构造模型的局部小性（local smallness）至关重要。
适配 Aczel–Mendler 构造： 为了构造 $P^0$ $P^{0}$ 的真正终端余代数（以模拟 AFA），作者将经典的 Aczel–Mendler 定理适配到了类型论中。这种适配需要：
- 定义“基于 U 的”演算（即在大型类型上的值是小型类型之值的余极限的演算）。
- 利用关系提升（relation lifting）和“前同余”（precongruences）的概念来对弱终端余代数进行商运算。
- 假设命题重缩放（propositional resizing），以确保生成的商类型是局部小的，并且该构造对于集合值演算（如 $P^0$ ）成立。

主要贡献与结果

Scott 反基础公理（SAFA）的模型： 作者构造了一个类型 $V^0_\infty$ ，它是受限幂集演算 $P^0$ 的不动点，但既不是初始代数也不是终端余代数。他们证明了该类型在诱导的成员关系下满足 Scott 反基础公理。在该模型中，相等性是恒等类型，且该模型是“简单”的（任何到它的同态都是相等的），但并非终端的。
向高阶类型的推广： 该构造被推广到对于任何截断层级 $n$ 的层级 $V^n_\infty$ 。这些模型对于所有 $k \le n$ 均满足广义的 $k$ -SAFA 公理。论文展示了这些模型在适当的截断层级下满足标准集合论公理（空集、分离公理、并集等），前提是这些模型是局部小的。
M-类型恒等类型的特征化： 论文提供了 M-类型恒等类型作为索引 M-类型的完整特征化（定理 2.15）。这一结果被用于证明所构造的模型是局部小的，这是将其作为 HoTT 中有效实质集合论模型的必要条件。
Aczel 反基础公理（AFA）的模型： 在假设命题重缩放公理的情况下，作者构造了 $P^0$ （以及更广泛的基于 $U$ 的演算）的终端余代数。该终端余代数作为 Aczel AFA 的模型，其中每个图都有唯一的装饰（decoration）。
$V^0_\infty$ 的非终端性： 论文明确展示了 $V^0_\infty$ 不是 $P^0$ 的终端余代数。它提供了一个反例，显示从特定图到 $V^0_\infty$ 可以存在不同的余代数同态，从而将其与通过 Aczel–Mendler 方法构造的终端余代数区分开来。

意义与主张
本文声称提供了首个在 HoTT 中其中相等性为恒等类型的非良基实质集合模型，超越了过去的基于集合论（setoid）的模型。

AFA 与 SAFA 的区别： 该工作澄清了在 HoFF 背景下 Aczel 的与 Scott 的反基础公理之间的关系。它表明，虽然终端余代数（需要命题重缩放）验证了 AFA，但余迭代不动点（无需命题重缩放即可构造）验证了 SAFA。作者指出，在未截断（ $\infty$ ）的情况下，AFA 和 SAFA 是重合的，但在较低的截断层级处它们会发生分歧。
构造性： SAFA 模型（ $V^n_\infty$ ）的构造是完全构造性的，不依赖于命题重缩放等非构造性公理。
形式化： 所有主要结果都使用 Agda 证明助手进行了形式化，同时利用了标准 Agda 和 Cubical Agda（用于第 6 节），以确保复杂的同伦论证的正确性。
开放问题： 作者谦虚地指出，在没有命题重缩放的情况下， $P^0$ 的终端余代数的存在性仍然是一个开放问题。他们并未声称解决了是否可能进行此类构造，或者其存在性是否意味着经典原理，而是将其强调为未来工作的主要动力。

总而言之，本文成功地将非良基集合理论扩展到了同伦类型论的高维设置中，为不同的反基础公理提供了不同的模型，并建立了关于 M-类型和余代数结构的必要技术基础。