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.
Keywords : Searchable type; compact type; totally separated type; ordinal; topological topos; HoTT; univalent foundations
Codes MSC : 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
|
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 arXiv category : Logic Domaine : Computer Science ; Logic and Foundations ; Topology Format : MP4 (.mp4) - HD Durée : 00:58:27 Audience : Researchers ; Graduate Students ; 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 Congrès : 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
