同伦类型论中序数构造性概念的联系

在经典集合论中，引入序数有多种等价方式。然而，在构造性设定中，不同概念发生分裂，各自具有不同的优缺点。我们考虑同伦类型论中三种不同的序数概念，并展示它们彼此间的关系：基于康托尔正规形的记号系统、精炼的布劳威尔树概念（由零、后继和可数极限归纳生成），以及良基广延序。对于康托尔正规形，多数性质是可判定的，而对于良基广延传递序，多数不可判定。布劳威尔树的表述通常是部分可判定的。我们证明这三种概念均具有序数预期的性质：它们的序关系虽在每种情况下定义不同，但都是广延且良基的，且通常的算术运算在每种情况下均可定义。我们通过构造从康托尔正规形到布劳威尔树、以及从后者到良基广延序的保结构嵌入来连接这些概念。我们已在立方 Agda 中形式化了大部分结果。