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$.
The construction can also be generalized in various ways.
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?”. We can also allow $X$ to be a certain sort of uniform space, with uniformity induced by a family of upper real number valued pseudometrics. 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, Continuity on the real line and in formal spaces. (2003). Revised version of U.U.D.M. Report 2003:32. link
(2007), 1854–1880.
Erik Palmgren, Resolution of the uniform lower bound problem in constructive analysis, link
Bas Spitters, Locatedness and overt sublocales, doi:10.1016/j.apal.2010.07.002 APAL
Thierry Coquand, Erik Palmgren, Bas Spitters, Metric complements of overt closed sets, Mathematical Logic Quarterly, 57(4), 373-378, 2011. link
Tatsuji Kawai, A point-free characterisation of Bishop locally compact metric spaces, link
Tatsuji Kawai. Localic completion of uniform spaces. Log. Methods Comput. Sci. 13 2017), no. 3, Paper No. 22, 39pp. arxiv