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 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

- If $\vert y - x \vert + \delta \le \epsilon$ then $B(x,\delta)\le B(y,\epsilon)$
- $\top = \bigvee_{x\in \mathbb{Q}} B(x,\epsilon)$ for any $\epsilon$
- $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) \}$
- $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 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?

rationalnumbers? $\endgroup$