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.
The big point that need clarification is whether we talk about the "Topological space $\mathbb{R}$" which is constructed by starting from the set of (for exemple) Dedekind (continuous) real numbers, putting a topology on them and looking at the associated locales, or about the "formal locale $\mathbb{R}$" which is constructed as the classifying topos (or rather classifying locale) for Dedekind real number.
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]$.
On the other hand, the formal locale $\mathbb{R}$ is always locally compact. So if $I = [0,1]$ denote the closed sublocale $[0,1]$, any map $I \to \mathbb{R}^n$ (where I'm using the formal locale on both side) is automatically bounded and uniformly continuous.
In fact, the two definitions coincide if and only if the topological space $\mathbb{R}$ is locally compact and a map between the topological $\mathbb{R}^n$ (or open subsets of them) extend into a map between the localic version if and only if it is uniformly continuous on closed bunded subsets. So this really caputres the difference.
As the question explicitely refers to "the language of locales" I will be (from now on) only refering to the localic version when talking about $\mathbb{R}^n$ and its subspace.
Once we know that all the locale under consideration are (locally) compact and Haussdorf (By Hausdorff I mean with a closed diagonal), one can decude that all the important maps are proper from the fact that any map from a compact locale to a Hausdorff locale is proper.
In particular (and that is another difference between the topological and localic point of view), the map $I \to S^1$ that sends $t$ to $(\cos(2\pi t),sin(2 \pi t) )$ is a proper morphism, it is also a surjection (its image is a closed sublocale that contains a dense set of point), hence it is an effective descent morphisms and hence the equalizer of its Kernel pair. Its kernel pair is exactly $\Delta \coprod \{(0,1) , (1,0) \}$ (where $\Delta$ denote the diagonal), and so $S^1$ can be obtained by gluing the end point of $I$. For any locale $X$, a map $S^1 \to X$ is the same as a map $f: I \to X$ such that $f(0)=f(1)$. Note that - as observed in the comments - this is in contrast with what happen with topological spaces, where the map $I \to S^1$ fail to even be surjective on points constructively.
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:
Theorem : Let $j:S^1 \to \mathbb{R}^2$ be any monomorphisms of locales (between the formale locales). Then $j$ is a closed embeddings and it's open complement $U$ can be written uniquely as a union of two opens $U = U_b \cup U_u$ with $U_b \cap U_u = \emptyset$, $U_b$ and $U_u$ inhabited and connected (and path connected) with $U_b$ bounded and $U_u$ unbounded. Moreover the image of $j$ is included in the closure of both $U_u$ and $U_b$.
I guess a complete proof of this would require writing a (short?) paper, and I couldn't find a simple enough Barr covering argument to get something like this (at least a cheap version of it) for free (at least not without doing substancial work first to, for example, to define the index of a curve at a point, but at this point, we can as well do the full proof). But I claim that the same methods as in the paper linked by Andrej Bauer The constructive Jordan Curves theorem can be applied to prove the theorem :
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.
