Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Collection Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Organisateur(s) Coquand, Thierry ; Negri, Sara ; Rathjen, Michael ; Schuster, Peter

Date(s) 01/05/2023 - 05/05/2023

URL associée https://conferences.cirm-math.fr/2319.html

00:00:00 / 00:00:00

4 5

Compact ordinals in HoTT/UF

De Martin Escardó

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.

Informations sur la vidéo

Date de captation 04/05/2023
Date de publication 15/05/2023
Institut CIRM
Licence CC BY NC ND
Langue Anglais
Audience Chercheurs, Doctorants
Réalisateur(s) Guillaume Hennenfent
Format MP4

Données de citation

DOI 10.24350/CIRM.V.20040503
Citer cette vidéo Escardó, Martin (04/05/2023). Compact ordinals in HoTT/UF. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20040503
URL https://dx.doi.org/10.24350/CIRM.V.20040503

Domaine(s)

Logique

Codes MSC

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow

Toutes les vidéos de la collection

52:12

publiée le 15 mai 2023

On a decomposition of WKL!!

De Takako Nemoto

55:38

publiée le 15 mai 2023

New modal operators for constructive mathematics

De Ingo Blechschmidt

58:06

publiée le 15 mai 2023

Recursive inequalities in applied proof theory

De Thomas Powell

58:27

publiée le 15 mai 2023

Compact ordinals in HoTT/UF

De Martin Escardó

46:40

publiée le 15 mai 2023

From axioms to synthetic inference rules via focusing

De Dale Miller

Copyright Carmin.tv 2024

Donner son avis