In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders. Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but almost all properties are undecidable. Brouwer trees take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences. Our three approaches are connected by canonical order-preserving functions from the "more decidable" to the "less decidable" notions. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardo and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.

翻译：在构造性设定下，没有任何一种具体的序数形式能同时具备所有可能令人感兴趣的性质；例如，能够计算序列的极限与判定外延相等性在构造意义上是不兼容的。以同伦类型论作为基础框架，我们发展了一个序论理论的抽象框架，并建立了一系列理想性质与构造。随后，我们研究并比较了同伦类型论中三种具体的序数实现：首先，一种基于康托尔范式（二叉树）的记法系统；其次，一种布劳威尔树的改进版本（无穷分支树）；第三，外延良基序。我们的三种表述均具备序数所期望的核心性质，例如配备了外延且良基的序关系，以及允许基本算术运算，但它们在额外可实现的功能上有所差异。例如，对于有限序数集合，康托尔范式具有可判定性质，但无法计算无穷集合的上确界。相比之下，外延良基序适用于无穷集合，但几乎所有性质都不可判定。布劳威尔树则处于中间的最佳平衡点，它结合了受限形式的可判定性与处理无穷递增序列的能力。这三种方法通过从"更可判定"到"更不可判定"概念的典范保序函数相互关联。我们已使用立方Agda形式化了关于康托尔范式与布劳威尔树的结果，而外延良基序则由Escardo及其合作者进行了深入研究和形式化。最后，我们将实现的计算效率与Berger报告的结果进行了比较。