James E Hanson

@jdw The answer to your first question should be yes since it's already the case that the join of (-∞,0) and [0,∞) in the lattice of sublocales of R is R. Regarding your followup question, it should be fairly easy to define this bump function constructively (on R as a locale and thereby on R as a topological space) since it's computable. More generally, you can constructively show that for any functions f : (-∞,0] → R and g : [0,∞) → R with the same limit at 0, there is a function h : R → R such that h(x) = f(x) for x ≤ 0 and h(x) = g(x) for x ≥ 0.

@jdw That's right. One way to think about it is that constructively it's consistent for R to 'not have enough points'. When this happens, if you take the join of the one-point sublocales of [0,∞), you get a proper sublocale of [0,∞). That said it's also not always going to be compatible with infinitary joins of open sublocales. If you have a singular cover of R, then there's a open proper sublocale of R that contains all of the points of R.