A locale is a sort of "formal topological space", which "may not have enough points to separate its open sets". For instance, there is a "locale of all real numbers that are both rational and irrational", which of course has no points at all (since there are no such numbers), but as a locale it is a nontrivial structure.

Locales are often better-behaved than topological spaces in constructive mathematics (i.e. in the absence of the law of excluded middle). For instance, there is a "locale of formal real numbers" $R_f$ whose sublocale $[0,1]_f$ is always compact, despite that the Heine-Borel theorem for the *space* $[0,1]$ may fail constructively. Classically, $R_f$ has enough points, but constructively it may not — though unlike the example above it of course has *lots* of points, indeed its points are dense in it. (See for instance P.T. Johnstone's book *Stone spaces*, or section D4.7 in *Sketches of an Elephant*.)

My question is: suppose $f:R_f \to R_f$ is a continuous map of locales, such that $f(x)>0$ for all points $x$ of $R_f$ (i.e. for all actual real numbers $x$); does it follow (constructively) that $f$ factors through the "locale of formal *positive* real numbers"?

The latter means the open sublocale of $R_f$ defined by the open subset $(0,\infty)$. Note that denseness of the points of $R_f$ is insufficient to answer "yes", since a function can be positive on a dense subset but zero at some other points.