Set-Theoretic and Type-Theoretic Ordinals Coincide

TL;DR

This paper proves the equivalence of set-theoretic and type-theoretic definitions of ordinals within homotopy type theory, and extends the concept to encompass all sets in Aczel's interpretation, formalized in Agda.

Contribution

It establishes the equivalence of set-theoretic and type-theoretic ordinals in HoTT and generalizes the notion to include all sets in Aczel's interpretation.

Findings

Set-theoretic and type-theoretic ordinals coincide in HoTT.

A generalized class of ordered structures includes all sets in Aczel's interpretation.

Formalization of results in Agda.

Abstract

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.