![[1241] Théorie de l’homotopie motivique et groupes d’homotopie stables, d’après Morel–Voevodsky, Isaksen–Wang–Xu, ...](/media/cache/video_light/uploads/video/Bourbaki.png)
published on June 19, 2025
[1241] Théorie de l’homotopie motivique et groupes d’homotopie stables, d’après Morel–Voevodsky, Isaksen–Wang–Xu, ...
By Frédéric Déglise
Towards synthetic locale theory
Appears in collection : Synthetic mathematics, logic-affine computation and efficient proof systems / Mathématiques synthétiques, calcul logique affine et systèmes de preuve efficients
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.
