Français
Compact ordinals in HoTT/UF
Multi angle
Authors : Escardó, Martin (Author of the conference)
CIRM (Publisher )
03B15 - Higher-order logic and type-theory
03F65 - Other constructive mathematics, See also {26E40, 46S30, 47S30}
54D30 - Compactness
CIRM (Publisher )
Loading the player...
|
Abstract :
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.
Keywords : Searchable type; compact type; totally separated type; ordinal; topological topos; HoTT; univalent foundations
MSC Codes : Keywords : Searchable type; compact type; totally separated type; ordinal; topological topos; HoTT; univalent foundations
03B15 - Higher-order logic and type-theory
03F65 - Other constructive mathematics, See also {26E40, 46S30, 47S30}
54D30 - Compactness
|
Information on the Video
Film maker : Hennenfent, GuillaumeLanguage : English Available date : 15/05/2023 Conference Date : 04/05/2023 Subseries : Research talks arXiv category : Logic Mathematical Area(s) : Computer Science ; Logic and Foundations ; Topology Format : MP4 (.mp4) - HD Video Time : 00:58:27 Targeted Audience : Researchers ; Graduate Students ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2023-05-04_Escardo.mp4 
|
Information on the Event
Event Title : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométriqueEvent Organizers : Coquand, Thierry ; Negri, Sara ; Rathjen, Michael ; Schuster, Peter Dates : 01/05/2023 - 05/05/2023 Event Year : 2023 Event URL : https://conferences.cirm-math.fr/2319.html
Citation Data
DOI : 10.24350/CIRM.V.20040503Cite this video as: Escardó, Martin (2023). Compact ordinals in HoTT/UF. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.20040503 URI : http://dx.doi.org/10.24350/CIRM.V.20040503 |
See Also
- [Multi angle] Recursive inequalities in applied proof theory / Author of the conference Powell, Thomas.
- [Multi angle] On a decomposition of WKL!! / Author of the conference Nemoto, Takako.
- [Multi angle] From axioms to synthetic inference rules via focusing / Author of the conference Miller, Dale.
- [Multi angle] New modal operators for constructive mathematics / Author of the conference Blechschmidt, Ingo.
Bibliography
Imagette Video
