The real numbers can be defined in two ways (well, more than two, but let's stick to these for now): as the Cauchy completion of the metric space $\mathbb{Q}$ with its usual absolute value, or as the Dedekind completion of the ordered set $\mathbb{Q}$ with its usual ordering.
When these two constructions are performed internally in a topos, they generally yield different results, and often it is the Dedekind construction that gives a more useful answer. In particular, for any topological space $X$, the Dedekind real number object in $\mathrm{Sh}(X)$ is the sheaf of continuous $\mathbb{R}$-valued functions on $X$, where $\mathbb{R}$ has its usual topology. (And this generalizes to some big toposes too.) Roughly, this is because the definition of "a Dedekind real number" is constructively equivalent to "a point of the locale of formal real numbers", where the latter locale can be defined constructively, and classically turns out to be equivalent to the usual topological space $\mathbb{R}$.
However, the Cauchy definition of $\mathbb{R}$ has other generalizations: we can complete with respect to a non-Archimedean absolute value instead, obtaining the $p$-adic numbers $\mathbb{Q}_p$. We can do this internally in a topos too, but as with $\mathbb{R}$, in general we will not get the "right" answer. My question is, is there any way to construct "the $p$-adic numbers" constructively which, when interpreted in $\mathrm{Sh}(X)$, will yield the sheaf of continuous $\mathbb{Q}_p$-valued functions on $X$, where $\mathbb{Q}_p$ has its usual topology? In particular, is there a "locale of formal $p$-adic numbers" that can be defined constructively and that classically is equivalent to the usual topological space $\mathbb{Q}_p$?
Best Answer
Yes there is: the formal locale of p-adic integer is simply defined as the projective limit of the $\mathbb{Z}/p^k\mathbb{Z}$ (as a pro-finite locale). So internally in any topos a continuous function with values in $\mathbb{Z}_p$ corresponds to an element of the projective limit of the $\mathbb{Z}/p^k\mathbb{Z}$ (as a set this time)
You can then define the locale $\mathbb{Q}_p$ as $\bigcup \frac{1}{p^k} \mathbb{Z}_p$ (this is a sequence of spaces where each space is open in the next so everything goes well...) and internally, the ring of continuous functions with values in $\mathbb{Q}_p$ is just $\mathbb{Z}_p [1/p]$ for the previously defined $\mathbb{Z}_p$.
It turns out that, in this precise case, this coincides with the sequential completion (easy to see from the projective limit description...).
This is a strange coincidence, but you can relate this to the fact that on a locally connected space the sequential completion corresponds to locally constant functions, but on a locally connected space, continuous functions with values in $\mathbb{Z}_p$ or $\mathbb{Q}_p$ are locally constant functions anyway because of the total disconnectedness.
There is in fact way more to it:
Steve Vickers has show how to define more generally the localic completion of a metric set (a set with a distance), and at least when the distance is symmetric this locale is essentially the Classifying space for the theory of regular Cauchy filter. Moreover it appears that this completion is stable under pullback along geometric morphism (this is not completely trivial, I prove it in my paper linked below) and because of this you will trivially have that if your metric set is the pullback of a metric set in the base topos then the points of its localic completion will be exactly the continuous function with values in the localic completion computed in the base topos.
So a general consequence to remember is that (constructively) "completion by Cauchy filters always give you the correct set of points" so in any case if you have any valuation on a fields (note that over a non boolean topos even if the fields is $\mathbb{Q}$ it might not be equivalent to $|\_ |_p$ for some $p$) the "correct" completion (the one corresponding to the Dedekind completion) is the Cauchy filter completion. For metric space there is also a notion of "Cauchy approximation" which gives the same completion and is a bit more 'sequential': they are decreasing sequences of open ball whose diameter goes to zero at a controlled speed.
References for localic completion:
Vickers wrote several paper on the subject, the more relevant is I think "Localic completion of quasimetric spaces" and after that there is two other on the non-symmetric case "Localic completion of generalized metric spaces" I & II. His presentation is rather different from what I add in mind, so I will look if there is something older more simple.
This paper of mine where I define the completion of a symmetric metric locale and study all the geometricity properties (stability under pull-back) in section 3.3 . It is exactly what you need but because it deals with metric locales instead of metric sets there is some annoying additional complication...