Synthetic mathematics, logic-affine computation and efficient proof systems / Mathématiques synthétiques, calcul logique affine et systèmes de preuve efficients

Collection Synthetic mathematics, logic-affine computation and efficient proof systems / Mathématiques synthétiques, calcul logique affine et systèmes de preuve efficients

Organisateur(s) Blechschmidt, Ingo ; Cohen, Liron ; Coquand, Thierry ; Negri, Sara ; Schuster, Peter

Date(s) 08/09/2025 - 12/09/2025

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

00:00:00 / 00:00:00

1 5

Towards synthetic locale theory

De Ulrik Buchholtz

In synthetic mathematics, we often pick a particular topos (say, a classifying topos for a nice theory), and work in the internal language of its (higher) sheaves. But to reap the full benefits of a synthetic statement we need to externalize and connect the internal with the external world. In my talk, I'll explore approaches to giving a synthetic account of (iterated) internalization. One is ongoing work by David Jaz Myers and Mitchell Riley on “theory type theory”, and another is “geometric type theory” as advocated by Steven Vickers. Both of these require radical new type theories, which in the long term is surely the right way to go. Here, we propose a simpler account, where we use type theory as is to build a “synthetic mathematics for synthetic mathematics”, inspired by Blechschmidt's duality axiom as arising from (large) sheaves on the category of small locales and small maps. This can be seen as a next step in a sequence of synthetic theories exploring more and more structure on locales, based on what kind of observations are axiomatized.

Informations sur la vidéo

Date de captation 09/09/2025
Date de publication 02/10/2025
Institut CIRM
Licence CC BY NC ND
Langue Anglais
Audience Chercheurs, Doctorants
Réalisateur(s) Luca Recanzone
Format MP4

Données de citation

DOI 10.24350/CIRM.V.20387703
Citer cette vidéo Buchholtz, Ulrik (09/09/2025). Towards synthetic locale theory. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20387703
URL https://dx.doi.org/10.24350/CIRM.V.20387703

Domaine(s)

Bibliographie

BLECHSCHMIDT, Ingo , A general Nullstellensatz for generalized spaces, Rough draft, 2023 - https://rawgit.com/iblech/internal-methods/master/paper-qcoh.pdf
JAZ MYERS, David., Liberating synthetic quasi-coherence from forcing, 2025. Blog post for the Topos Institute. - https://topos.institute/blog/2025-07-13-liberating-synthetic-quasi-coherence-from-forcing/
VICKERS, Steven. Arithmetic universes and classifying toposes. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 2017, vol. 58, no 3 & 4, p. 213-248. - https://cahierstgdc.com/wp-content/uploads/2018/01/Vickers-58-34.pdf

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

53:36

publiée le 2 octobre 2025

Towards synthetic locale theory

De Ulrik Buchholtz

29:32

publiée le 2 octobre 2025

Towards the effective 2-topos

De Jacopo Emmenegger

51:49

publiée le 2 octobre 2025

Synthetic perspectives on the Yoneda lemma

De Emily Riehl

53:50

publiée le 2 octobre 2025

Synthesising random variables

De Alex Simpson

44:15

publiée le 2 octobre 2025

Towards an internal construction of meaning

De Sophie d'Espalungue

Copyright Carmin.tv 2025

Donner son avis