Abstract:
It may be argued that the language of mathematics, say type
theory, is about the category of sets, although the definite
article here
requires some justification. As possible worlds of mathematics we may
admit all models of type theory, by which we mean all local
toposes.
For an intuitionist, there is a distinguished local topos, namely the
so-called free topos, which may be constructed as the
Tarski-Lindenbaum
category of intuitionistic type theory. However, for a classical mathematician,
to pick a distinguished classical local topos (namely a topos whose
terminal object is a generator) may be as difficult as to define truth
in classical type theory, which Tarski has shown to be impossible.