Abstract
I’ll give an update on joint work with Johannes Schipp von Branitz and Mark Damuni Williams on devising a type theory for reasoning synthetically about synthetic mathematics. Synthetic mathematics using type theory leverages the interpretation of types as sheaves over a suitable (higher) topos, using principles that are only valid in that interpretation. This works one topos at a time. Recent work by Ingo Blechschmidt and others point the way towards systematically deriving these principles, and we build on this to propose a synthetic mathematics for synthetic mathematics, allowing a single theory to relate the synthetic mathematics of several toposes (including the base), beginning with the case of localic toposes. This touches on several aspects of Martín’s work: constructive topology and domain theory, topos semantics, and constructive type theory.
Talk Details
Speaker: Ulrik Buchholtz (University of Nottingham, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 14:10
Slides: Available
Key Topics
- Synthetic mathematics
- Higher toposes
- Sheaf semantics
- Localic toposes
- Constructive topology
- Domain theory
- Type theory foundations
- Topos semantics
Collaborators
- Johannes Schipp von Branitz
- Mark Damuni Williams
Related Work
- Ingo Blechschmidt’s work on systematic derivation of synthetic principles
- Thierry Coquand - Sheaf models of dependent type theory
- Steve Vickers - Escardó-Simpson interval objects and point-free trigonometry
Connection to Escardó’s Work
This research touches on several key areas of Martín Escardó’s contributions: constructive topology and domain theory, topos semantics, and constructive type theory, demonstrating the breadth and continuing influence of his work across foundational mathematics.