  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.
