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.
