![[1245] Model theory, differential algebra and functional transcendence](/media/cache/video_light/uploads/video/SeminaireBourbaki.jpg)
publiée le 9 décembre 2025
[1245] Model theory, differential algebra and functional transcendence
De Amador Martin-Pizarro
Compact ordinals in HoTT/UF
Apparaît dans la 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.
