Set-Theoretic and Type-Theoretic Ordinals Coincide
(2023)
Presentation / Conference
KRAUS, N., de Jong, T., Nordvall Forsberg, F., & Xu, C. (2023, June). Set-Theoretic and Type-Theoretic Ordinals Coincide. Paper presented at Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, USA
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 (... Read More about Set-Theoretic and Type-Theoretic Ordinals Coincide.