Set-Theoretic and Type-Theoretic Ordinals Coincide

Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1

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…