Compact ordinals in HoTT/UF
Appears in collection : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique
We discuss compact ordinals in HoTT/UF. In terms of computation, they are defined by an exhaustive searchability condition, which, in logic, corresponds to a form of choice, and, in topology, corresponds to compactness in the case of totally separated types. We use Johnstone's topological topos as a guiding tool.
