Could not include topos theory - contents
There are several conditions on a topos that are necessary and sufficient to be boolean: * Every subobject has a complement (the general definition of boolean category). * Every subobject lattice is a Boolean algebra. * The subobject classifier is an internal Boolean algebra. * The maps are a coproduct cone (so in particular, , but this alone is not sufficient).
The internal logic of a boolean topos with natural numbers object can serve as foundations for “ordinary” mathematics, except for that which relies on the axiom of choice. If you add the axiom of choice, then you get (an internal version of) ETCS; conversely, if you use an arbitrary topos, then you get constructive mathematics. (For some high-powered work, you may also need to add a version of the axiom of replacement or an axiom of Grothendieck universes.)
Every cartesian closed boolean pretopos is in fact a topos. This is why ‘generalised predicativism’ (with function types but not power types) is necessarily a feature of constructive mathematics only.
Matthew Jackson, A sheaf-theoretic approach to measure theory, 2006 (pdf)