以 Cubical Agda 正式化同伦类型论中的实数
计算机科学中的逻辑
2026-04-29 v1
摘要
在构造数学中，实数一直似乎需要以各种形式妥协。经典的完备性证明需要可数选择，Bishop 的集合型构造在每个定义和定理上引入持续的bookkeeping开销，Dedekind 切割则迫使在前束类型论中进行笨拙的宇宙级跟踪。同伦类型论 (HoTT) 书中提出了一种替代方法，将 Cauchy 实数构建为更高归纳-归纳类型族，从而避免了上述所有妥协。我们在 Cubical Agda 中实现了 HoTT 书中的实数，Cubical Agda 是一个其对更高归纳类型的本机支持允许该构建直接表达。代码在没有后设或孔的情况下通过类型检查，为在构造分析中进一步的机器辅助工作提供了基础。
引用
@article{arxiv.2604.24782,
title = {Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda},
author = {Jackson Brough},
journal= {arXiv preprint arXiv:2604.24782},
year = {2026}
}