A [locale](http://ncatlab.org/nlab/show/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.



Detecting positive endomaps of the formal reals
I think the answer is no. Work in a recursive context; eg the effective topos.
Consider a (uniformly continuous) function $f:R\to R$ such that $f(x)>0$ for all $x$, but we don't have a positive infimum. This is standard (use the Kleene tree).
Now consider the embedding of pointwise spaces into locales; the work by Palmgren [A constructive and functorial embedding of locally compact metric spaces into locales](http://www.sciencedirect.com/science/article/pii/S0166864107001113). Then you have a function as requested, but if it factors through the positive formal reals, then we have a positive infimum. The result is proved [here](http://www2.math.uu.se/research/pub/Palmgren16.pdf) and recalled in the introduction of [this paper](http://logicandanalysis.org/index.php/jla/article/view/39/21)


