Compact ordinals in HoTT/UF | Vidéo | Carmin.tv

00:00:00 / 00:00:00

Compact ordinals in HoTT/UF

By Martin Escardó

Appears in 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.

Information about the video

Date of recording 04/05/2023
Date of publication 15/05/2023
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Guillaume Hennenfent
Format MP4

Citation data

DOI 10.24350/CIRM.V.20040503
Cite this video 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

Domain(s)

Logic

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

Copyright Carmin.tv 2025

Give feedback