Return to Answer

Maybe problem in non-localic constructive analysis (of the kind mentioned by Andrej Bauer in his comments) are closely related to the fact that topological space $\mathbb{R}$ is not (always) locally compact, so for example, not every map on it to $\mathbb{R}^n$ has to be bounded on $[0,1]$ or uniformly continuous on $[0,1]$.

Many problems in non-localic constructive analysis (of the kind mentioned by Andrej Bauer in his comments) are closely related to the fact that topological space $\mathbb{R}$ is not (always) locally compact, so for example, not every map on it to $\mathbb{R}^n$ has to be bounded on $[0,1]$ or uniformly continuous on $[0,1]$.

Finally, any map $S^1 \to \mathbb{R}^2$ is proper and uniformly continuous, in particular, any monomorphism $S^1 \to \mathbb{R}^2$ is automatically a closed embeddings (proper injections are closed embeddings). Now I'm completely convinced by the paper Andrej Bauer linked that the following is constructively valid:

The fact that we look at map of locale gives us all the boundeness and uniformity assumption they need, and because we look at the "open complement" of the closed curve, we get all the condition of "being at bounded distance from the curve". Finally, while all the proof in the paper explicitely refers to points, I believe they can all be interpreted as reffering to generalized elements : when they talk about taking a point in $U$, interpret this as working internally in the topos $Sh(U)$ and using the generic point of $U$ that you have there. Of course, in order to this, some additional work is requiered to show that many construction they do can be transfered from one topos to another (they are all "geometric") but I looked at it and so far I see no problem for doing this.

Finally, any map $S^1 \to \mathbb{R}^2$ is proper and uniformly continuous, in particular, any monomorphism $S^1 \to \mathbb{R}^2$ is automatically a closed embeddings (proper injections are closed embeddings). Now I'm completely convinced by the paper Andrej Bauer linked that the following is constructively* valid:

The fact that we look at map of locale gives us all the boundeness and uniformity assumption they need, and because we look at the "open complement" of the closed curve, we get all the condition of "being at bounded distance from the curve". Finally, while all the proof in the paper explicitely refers to points, I believe they can all be interpreted as reffering to generalized elements : when they talk about taking a point in $U$, interpret this as working internally in the topos $Sh(U)$ and using the generic point of $U$ that you have there. Of course, in order to this, some additional work is requiered to show that many construction they do can be transfered from one topos to another (they are all "geometric") but I looked at it and so far I see no problem for doing this.

*Note : regarding the type of foundation/constructivism, I'll go to my safe place and say this is valid in any elementary topos with a natural number object. In particular it is a theorem of intuitionistic ZF. Though I'm sure if some care is taken when talking about locales, this can be made into a completely predicative statement as well, so weaker systems like constructive set theory or some form of type theory should be ok too.

Let me first clarify some confusion in the comments to the original question. To be clear : I'm not at all saying the persons making them were confused, as far as I can tell all the comments were correct, my point is rather than the mixture of the "topological" and "localic" point of view created some confusion that I would like to clarify the distinction before we go any further.

Let me first clarify some confusion in the comments to the original question. To be clear : I'm not at all saying the persons making them were confused, as far as I can tell all the comments were correct, my point is rather than the mixture of the "topological" and "localic" point of view created some confusion (which I might very well be responsible for), and I would like to clarify the distinction before we go any further.