English
Compact ordinals in HoTT/UF
Multi angle
Auteurs : Escardó, Martin (Auteur de la conférence)
CIRM (Editeur )
03B15 - Higher-order logic and type-theory
03F65 - Other constructive mathematics, See also {26E40, 46S30, 47S30}
54D30 - Compactness
CIRM (Editeur )
Loading the player...
|
Résumé :
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.
Mots-Clés : Searchable type; compact type; totally separated type; ordinal; topological topos; HoTT; univalent foundations
Codes MSC : Mots-Clés : 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
|
Informations sur la Vidéo
Réalisateur : Hennenfent, GuillaumeLangue : Anglais Date de Publication : 15/05/2023 Date de Captation : 04/05/2023 Sous Collection : Research talks Catégorie arXiv : Logic Domaine(s) : Informatique ; Logique et Fondements ; Topologie Format : MP4 (.mp4) - HD Durée : 00:58:27 Audience : Chercheurs ; Etudiants Science Cycle 2 ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2023-05-04_Escardo.mp4 
|
Informations sur la Rencontre
Nom de la Rencontre : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométriqueOrganisateurs de la Rencontre : Coquand, Thierry ; Negri, Sara ; Rathjen, Michael ; Schuster, Peter Dates : 01/05/2023 - 05/05/2023 Année de la rencontre : 2023 URL de la Rencontre : https://conferences.cirm-math.fr/2319.html
Données de citation
DOI : 10.24350/CIRM.V.20040503Citer cette vidéo: 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 |
Voir Aussi
- [Multi angle] Recursive inequalities in applied proof theory / Auteur de la conférence Powell, Thomas.
- [Multi angle] On a decomposition of WKL!! / Auteur de la conférence Nemoto, Takako.
- [Multi angle] From axioms to synthetic inference rules via focusing / Auteur de la conférence Miller, Dale.
- [Multi angle] New modal operators for constructive mathematics / Auteur de la conférence Blechschmidt, Ingo.
Bibliographie
Imagette Video
