Toward a minimalist foundation for constructive mathematics

The two main views in modern constructive mathematics usually associated with constructive type theory and topos theory are compatible with the classical view, but they are incompatible with each other, in a sense explained by some specific results which are briefly reviewed. This chapter argues in favour of a minimal foundational theory. On the one hand, this has to satisfy the proofs-as-programs paradigm, and thus be suitable for the implementation of mathematics on a computer. On the other hand, it has to be compatible with all the theories in which mathematics has been developed, like Zermelo-Fraenkel set theory, topos theory, and Martin-Löf's type theory. As a first step towards a foundational theory of this kind, the chapter formulates a specific intensional type theory, but it also warns that one should give up the expectation of an all-embracing foundation.