Peter LeFanu Lumsdaine: Projectivity in the free topos

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.