一句话：证明在Aczel解释下，构造集合论序数与HoTT类型论序数等价，并推广到所有集合。
构造集合论将序数定义为本原传递集合，而同伦类型论（HoTT）将序数定义为带有传递、良基且外延二元关系的类型。本文研究这两种定义之间的关系。作者采用 Aczel 构造集合论到类型论解释的 HoTT 精化，证明两种序数概念等价。随后，他们将类型论序数的概念推广到 Aczel 解释中的所有集合，而不仅限于序数，由此得到一类自然的有序结构；该类包含类型论序数，并实现了集合论的高阶归纳解释。所有结果均已在 Agda 证明助手中形式化。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2301-10696,
title = {Set-Theoretic and Type-Theoretic Ordinals Coincide},
author = {Tom de Jong and Nicolai Kraus and Fredrik Nordvall Forsberg and Chuangjie Xu},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175762}
}