For which Sheaf topoi is Brouwer's fan theorem true?

Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable product of spaces, it can be viewed as a countable choice axiom in its own right. However, general elementary topoi satisfy very few choice principles and the effective topos famously does not satisfy the fan theorem.

The fan theorem is a well known foundational result in constructive analysis, and continuous functions on the set of reals are allowed to have very pathological behaviours if it is not assumed, which is a symptom of the fact that the locale of real numbers cannot be proven to be spatial.

For which sheaf topoi is the fan theorem true?

(I am also interested in results on other related theorems like the bar theorem and especially the principle of open induction on the Dedekind reals, which are slightly stronger. I mostly care about sheaves on compact Hausdorff spaces and about smooth sets)

• It's not enough to have dependent choice. DC holds in the effective topos, but the Fan theorem does not, but the "Kleene tree" argument.
– aws
Nov 24 at 17:58
• @aws Thank you. I'll just shorten that paragraph. Nov 24 at 18:25