We are talking about ordinary reals in constructive mathematics.

Let represent each real number by infinite converging series: $$r = [\;(a_0,b_0),(a_1,b_1),...,(a_i,b_i),...\;]$$ $$where\quad a_i \leq a_{i+1} \; and \; b_{i+1} \leq b_i \quad and \quad if\;a_i=a_{i+1} \;and\; b_i=b_{i+1} \;then\; a_i=b_i$$

And interval $(a_i,b_i)$ converges: for any given rational $e$ there is index $j$ such that $b_k - a_k < e$ for all $k \geq j$.

There are only one way to construct such a number: to build an algorithm that produces $ (a_{i+1},b_{i+1}) $ from (a,b) (or some nearly equivalent).

Let model algorithms by lambda terms (we are able to do so because lambda calculus is Turing complete).

It is easy to show that each lambda term may be represented by unique natural number (this is simple serialization/deserialization process, well known for every programmer).

So there is a one-to-one correspondence between real numbers and subset of natural numbers.

This imply that constructive reals and naturals are equipotent sets.

Correct?