Abstract
I have had several interactions with Martin on the topic of sheaf models for type theory, in a constructive meta theory. In particular, we had several discussions in Princeton, 2012 and I started to write a suggestion for a sheaf model for choice sequences. As Martin found out with his former student Chuanghie Xu, this suggestion was too simple: Hofmann’s construction of universes in presheaf models cannot be simply generalised to sheaf models. I will try to present current research on this topic, with two possible examples.
Talk Details
Speaker: Thierry Coquand (University of Gothenburg, Sweden)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 13:30 (remote)
Key Topics
- Sheaf models
- Dependent type theory
- Constructive meta theory
- Choice sequences
- Presheaf models
- Universe constructions
- Hofmann’s construction
Collaboration History
This talk reflects long-term interactions between Coquand and Escardó on sheaf models, including discussions in Princeton in 2012. The work involves collaboration with Escardó’s former student Chuangjie Xu, who identified limitations in early approaches to generalizing presheaf model constructions.
Related Work
- Hofmann’s universe construction in presheaf models
- Choice sequences in constructive mathematics
- Maria Emilia Maietti - On the compatibility of dependent type theory with Brouwer’s intuitionistic principles