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 toposesbig 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$?
