In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.
Constructing Initial Algebras Using Inflationary Iteration
经典集合论中的Adámek的一个老定理通过序数上的超限迭代构造了充分共连续的内函子的初始代数。我们证明了一个新的版本，工程建设性的逻辑，使用“通货膨胀”迭代的大小概念，抽象的极限序数只是他们的传递性，定向和良好的基础属性。借用泰勒的建设性的序数处理，我们表明，存在的大小与上界的任何给定的签名的指数。由此可以得出结论，只要人们承认由于Streicher、Moerdijk、van den Berg和Palmgren而产生的弱选择形式（WISC），就有丰富的一类内函子可以应用新定理，并且已知它在许多种拓扑的内部构造性逻辑中成立。
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
