It is well known how to derive the field operations from the construction of the real numbers as the Dedekind completion of the rational numbers and as the Cauchy completion of the rational numbers; see section 11.2.1 and 11.3.3 of [this textbook](https://hott.github.io/book/hott-online-1353-g16a4bfa.pdf) for an explicit definition of real numbers as a Dedekind completion or Cauchy completion. However, in constructive mathematics, none of the above definitions of the real numbers behave well, as many theorems in classical mathematics fail, such as the Heine-Borel theorem and the fundamental theorem of algebra.


Instead, one has to use the locale of real numbers, defined as the localic completion of the rational numbers. A locale $A$ is a frame $\mathcal{O}(A)$ whose elements are regarded as "opens"; a frame is a partially ordered set with finitary meets and infinitary joins where meets distribute over all joins, and a continuous function between two locales $f:A \to B$ is a frame homomorphism $f^\*:\mathcal{O}(B) \to \mathcal{O}(A)$, a function which preserves the frame structure.


Now let $\mathbb{R}$ be the symbol denoting the locale of real numbers. There is a function $B:\mathbb{Q} \times \mathbb{Q}^+ \to \mathcal{O}(\mathbb{R})$ to the frame of opens of the locale of real numbers, with the weak and strict orders defined as


* $B(x,\delta)\le B(y,\epsilon)$ if $\vert y - x \vert + \delta \le \epsilon$
* $B(x,\delta)\lt B(y,\epsilon)$ if $\vert y - x \vert + \delta \lt \epsilon$


respectively for $x, y \in \mathbb{Q}$ and $d, e \in \mathbb{Q}^+$.


The localic completion of the rational numbers is the locale presented by the following generators and constructors


1. If $\vert y - x \vert + \delta \le \epsilon$ then $B(x,\delta)\le B(y,\epsilon)$
2. $\top = \bigvee\_{x\in \mathbb{Q}} B(x,\epsilon)$ for any $\epsilon$
3. $B(x,\delta)\cap B(y,\epsilon) = \bigvee \{ B(z,\eta) \mid B(z,\eta) \le B(x,\delta) \, \text{and} \, B(z,\eta) \le B(y,\epsilon) \}$
4. $B(x,\delta) = \bigvee \{ B(y,\epsilon) \mid B(y,\epsilon) \lt B(x,\delta) \}$


However, I wasn't able to find anything on how the field operations are explicitly derived from the construction of the locale of real numbers, as most of the literature I looked at either focused solely on the topological properties of the locale of real numbers such as local compactness, or is about locale theory more generally. The fact that one is able to talk about the fundamental theorem of algebra and [Jordan's theorem](https://mathoverflow.net/questions/407492/what-is-the-status-of-jordans-theorem-in-constructive-mathematics-in-the-langua/407589#407589) in the locale of real numbers imply that the field operations are well-defined on the locale of real numbers. How would one go about explicitly defining the field operations on the locale of real numbers?



The field structure on the locale of real numbers
There are several (equivalent) way to go about it:


You can start form the fields operation on $\mathbb{Q}$ and use that they are "locally uniformly continuous" to extend them by continuity to the localic completion (for the inverse map, you'll have to stay away of $0$ of course).


Regarding the existence of such continuous extention: I don't remember the literature on constructive localic completion very well (I haven't worked on that topic in almost 10 years). You can look at [this paper](https://arxiv.org/abs/1411.0898) of mine where I do it for maps satisfying $d(f(x),f(y)) \leqslant d(x,y)$ (see sections 3.3, 3.4 and 3.6), which isn't quite what you need but should be enough given that you can restrict to a ball and replace the distance function by a multiple of it to arrive at something that satisfies this condition. But I'm sure there are more appropriate references available. (I'll see if I can remember something)


**Alternatively**, you can use the fact that these operations are well defined on Dedekind real numbers constructively and the methods explained [here](https://mathoverflow.net/questions/426682/locallic-maps-given-by-series/426692#426692) allow you to turn these into maps between the corresponding locales (using the fact that these constructions are geometric and the Yoneda lemma).


Here again, to talk about inverse you have to restrict to Dedekind real that are $>0$ or $< 0$ which in terms of classifying locales corresponds to the open subspace $\mathbb{R} - \{0\}$


