Consider a simple case of set-valued sheaves on some topological space $X$, $\operatorname{Sh}(X)$. All of these are Grothendieck toposes but clearly not all of them are equivalent.
Is there an overview of what properties of $\operatorname{Sh}(X)$ are induced by the properties of $X$? The properties I am interested in are the logical principles that hold in the internal logic. Of course the properties must necessarily be the properties of the locale of opens $\mathcal{O}(X)$.
Sketches of an Elephant has a list of some properties induced by the properties of $\mathcal{O}(X)$, but most of these are about the existence of geometric morphisms, which of course in some cases allow one to define some modalities in the internal language, but I would also like to know if there are some formulas of ordinary higher-order logic that are valid.
For example, suppose $X$ is compact. Is there a useful or interesting logical principle that holds in $\operatorname{Sh}(X)$ but does not hold in sheaves over non-compact spaces? Perhaps some form of choice?
I asked this question on math.stackexchange.com but did not receive an answer so I hope it's OK to ask here.
