Is there a nice (topological) characterization of the locales such that the axiom of dependant choices holds in the internal logic of the topos of sheaves ? I would also be interested in the case of the axiom of countable choice if the characterization is simpler.
Note, that (if I'm correct) the internal axiom of dependant choice in the topos of sheaves over a locale $X$ is equivalent to the following 'external' property:
If: $$... \twoheadrightarrow U_n \twoheadrightarrow U_{n-1} \twoheadrightarrow \dots \twoheadrightarrow U_1 \twoheadrightarrow U_0$$ is an infinite sequence of sheaves over $X$ connected by epimorphisms, then the map from the projective limit $U_{\infty} \rightarrow U_0$ is also an epimorphisms of sheaves.
I've also put the tag general topology because if we restrict to spatial locales then we have a question of purely about point set topology and sheaves over (sober) topological space which is probably equally interesting: one what conditions on a (sober) topological space $X$ do we have the above property about sequence of sheaves ?
