In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.

翻译：在构造型集合论中，序数是指具有传递性的集合。 在同伦类型论（HoTT）中，序数是具有传递性、良基、扩张性的二元关系的类型。 如果我们使用（HoTT对构造型集合论的）阿兹尔解释，我们将证明两个定义是等价的。 随后，我们推广了类型论序数的概念，以捕捉所有阿兹尔解释中的集合，而不仅仅是序数。 这导致了一个自然的有序结构类，其中包含了类型论序数，并实现了集合论的高阶归纳解释。 我们所有的结果都在Agda中进行了形式化。