If $X$ is a metric space, we can construct a version of its Cauchy completion as a locale, by taking as basic opens formal symbols $B_\delta(x)$ representing open balls, and imposing relations ensuring that the points are Cauchy filters. (We can equivalently regard $X$ as a Lawvere metric space and build a locale whose points are “Cauchy profunctors”.) This is the localic completion of $X$.
Consider the collection of “formal balls” $B(x,\delta)$, where $x\in X$ and $\delta\in\mathbb{Q}^+$ (technically this is just another notation for the ordered pair $(x,\delta)\in X\times \mathbb{Q}^+$). We say:
The localic completion of $X$ is the locale presented by generators $B(x,\delta)$ and relations:
Vickers combines conditions (3) and (4) into:
On the other hand, condition (3) makes sense for any poset of generators replacing $\{B(x,\delta)\}$, and simply says that we regard the generators as a base rather than a subbase. Since the elements of a formal topology automatically form a base, Palmgren (who works with formal topologies) can omit condition (3).
When interpreted as a geometric theory, conditions (1)–(4) say that the localic completion of $X$ is the classifying locale for Cauchy filters in $X$ that are additionally rounded (condition (4)).
When $X$ is the rational numbers $\mathbb{Q}$, this yields the locale of real numbers, which is in many respects better-behaved constructively than either its space of points (the Dedekind real numbers) or the completion of $\mathbb{Q}$ by Cauchy sequences (the Cauchy real numbers). Thus, the localic completion provides a “good” notion of completion for arbitrary metric spaces which generalizes the good localic real numbers.
By localically completing $\mathbb{Q}$ under a different metric, we obtain a “locale of p-adic numbers”; see this MO question.
We can allow $X$ to be a pseudometric space, a Lawvere metric space, or even a “metric locale?”. See the references.
Steve Vickers, “Localic Completion Of Generalized Metric Spaces II: Powerlocales”, pdf
Simon Henry, Localic Metric spaces and the localic Gelfand duality, arXiv
Erik Palmgren, A constructive and functorial embedding of locally compact metric spaces into locales