Set-theoretic and type-theoretic ordinals coincide

Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

Research output: Contribution to conferencePaperpeer-review

18 Downloads (Pure)


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 typetheoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
Original languageEnglish
Number of pages13
Publication statusE-pub ahead of print - 29 Jun 2023
EventThirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science - Boston, United States
Duration: 26 Jun 202329 Jun 2023
Conference number: 38


ConferenceThirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS
Country/TerritoryUnited States
Internet address


  • set-theoretic
  • type-theoretic
  • ordinals
  • homotopy type theory (HoTT)
  • Aczel's interpretation


Dive into the research topics of 'Set-theoretic and type-theoretic ordinals coincide'. Together they form a unique fingerprint.

Cite this