# Detecting positive endomaps of the formal reals

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.

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. 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 and recalled in the introduction of this paper
• How do you extend the map $f$ from reals to the locale of reals? Or this something that Erik does? – Andrej Bauer Jul 30 '15 at 21:40