Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, *The Countable Reals*) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a topos that makes Dedekind reals countable.

However, mainstream constructive $p$-adic implementation, such as Cauchy $p$-adic and HoTT $p$-adic, or just base-$p$ expansion $p$-adic, are uncountable.

I would like to know:

- Is there exists a $p$-adic implementation that is not sequence-avoiding?
- Is there a topos in infinite-time Turing machines where the $p$-adic is countable?
- If so, how many metrically complete can be hold in this topos? Can $\mathbb{Q}_p,\mathbb{C}_p,\Omega_p$ be countable?