We have a well defined map from decimal expansions to Cauchy real numbers, so by taking the image factorisation of this map, we can always quotient out the set of decimal expansions to get a subobject of the Cauchy reals. This subobject is $\neg \neg$-dense, i.e. every Cauchy real does not lack a decimal expansion, corresponding to the fact that every computable real number has a computable decimal expansion. However, it is still the case in general in constructive mathematics that not every Cauchy real has to have a decimal expansion, corresponding to the fact that there is no uniformly computable way to find decimal expansions of computable Cauchy sequences.

In the presence of countable choice, the Dedekind and Cauchy reals are the same, and the following are equivalent (if I recall correctly weak countable choice is sufficient for these equivalences, but lets stick to countable choice for simplicity):

- Every real number has a decimal expansion.
- Decimal expansions are closed under addition.
- The lesser limited principle of omniscience (LLPO): for every binary sequence $\alpha$ with at most one $i$ such that $\alpha(i) = 1$, either $\alpha(2i) = 0$ for all $i$, or $\alpha(2i + 1) = 0$ for all $i$.

For $1 \Rightarrow 2$, just use that Cauchy real numbers are closed under addition.

For $2 \Rightarrow 3$, let $\alpha$ be a binary sequence with at most one $1$, and define two decimal expansions $a := 0.a_0 a_1 a_2 a_3 \ldots$ and $b := 0.b_0 b_1 b_2 b_3 \ldots$ where
$$
a_i = \begin{cases}
9 & \alpha(2i) = 0 \\
0 & \alpha(2i) = 1
\end{cases}
$$
$$
b_i = \begin{cases}
0 & \alpha(2 i + 1) = 0 \\
1 & \alpha(2 i + 1) = 1.
\end{cases}
$$
If the first digit of the decimal expansion of $a + b$ is $1$, then $\alpha(2i) = 0$ for all $i$, and if the first digit is $0$, then $\alpha(2 i + 1) = 0$ for all $i$.

Fer $3 \Rightarrow 1$, note that we can build the decimal expansion up a stage at time. If the current Cauchy approximation of a real $a$ at stage $n$ is exactly $0.a_1\ldots a_n$, and we need to find the $n$th decimal digit, we can use LLPO to show there exists $a_n' \in \{a_n - 1, a_n\}$ such that if $a_n' = a_n - 1$, then $a \leq 0.a_1\ldots a_n$ and if $a_n' = a_n$, then $a \geq 0.a_1\ldots a_n$, and we can choose such an $a_n'$ (for all elements of the countable set of finite decimal expansions) by countable choice.

3more comments