I am looking for statements¹ that, when interpreted in the internal language of a topos, are valid in all spatial toposes (i.e., the topos of sheaves of any topological space) that are not valid in all Grothendieck toposes. Is there somewhere I could find various examples of such things, to get a feel of what they look like and how they are proved?
Essentially the only example I know is: “the unit interval $[0,1]$ is compact” or its variation, “Cantor space $2^{\mathbb{N}}$ is compact”: these statements hold in any spatial topos but not in any Grothendieck topos. For proofs of these fact, see theorem 3.2 and §4, as well as the postscript, in: Fourman & Hyland, “Sheaf models for analysis”, p. 280–301 in Fourman, Mulvey & Scott (eds.), Applications of Sheaves (Durham 1977) (Springer LNM 753, 1979).
While I'm at it, I'm also interested in the threefold separation:
Examples of statements valid in all spatial toposes that are not valid in all localic toposes.
Examples of statements valid in all localic toposes that are not valid in all Grothendieck toposes.
Examples of statements valid in all Grothendieck toposes that are not valid in all elementary topoi² with natural numbers object.
— provided these do exist, which I'm not at all sure of (except for the above-mentioned examples for the first point).
Let's say, to be more precise: statements in higher-order logic whose types are constructed by finite applications of finite products, finite coproducts and internal hom (function types) over the basic types $0$, $1$, $\Omega$ (type of truth values) and $N$ (type of natural numbers).
(Here following the convention that the plural of “Grothendieck topos” is “Grothendieck toposes” but that of “elementary topos” is “elementary topoi”.)