Peter LeFanu Lumsdaine: Projectivity in the free topos
Tid: On 2018-05-23 kl 10.00 - 11.45
Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University 
Medverkande: Peter LeFanu Lumsdaine, Stockholm University
Abstract:
I will discuss some classic results on projectivity in the free topos — in proof-theoretic terms, existence properties for intuitionistic higher-order logic (IHOL). In particular, I will look at:
- Freyd’s “gluing” proof that the terminal object is projective in the free topos, i.e. the existence property for IHOL;
- Makkai’s “lost” proof that the natural numbers object is projective in the free topos, i.e. the “rule of countable choice” for IHOL.
This talk is largely expository, including results of Freyd and Makkai together with ongoing work of Forssell, Lumsdaine, and Swan.