Usually in defining Dedekind cuts, you’d use truth values rather than booleans for the codomain of indicator functions.
There’s a ton of other nuances to real numbers in constructive math. For instance, Dedekind cuts defined by their lower bound, their upper bound, or both bounds are inequivalent (with both bounds being more appropriate in general, but lower bounds being useful sometimes in measure theory IIRC), and for Cauchy sequences you’d usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).
For a complete construction of the real numbers in constructive foundations, I recommend the Homotopy Type Theory book.
Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut
When constructed more carefully, every Cauchy sequence corresponds to a Dedekind cut, but it requires something stronger (such as excluded middle) to show that every Dedekind cut corresponds to a Cauchy sequence.
In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.
Usually in defining Dedekind cuts, you’d use truth values rather than booleans for the codomain of indicator functions.
There’s a ton of other nuances to real numbers in constructive math. For instance, Dedekind cuts defined by their lower bound, their upper bound, or both bounds are inequivalent (with both bounds being more appropriate in general, but lower bounds being useful sometimes in measure theory IIRC), and for Cauchy sequences you’d usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).
For a complete construction of the real numbers in constructive foundations, I recommend the Homotopy Type Theory book.
When constructed more carefully, every Cauchy sequence corresponds to a Dedekind cut, but it requires something stronger (such as excluded middle) to show that every Dedekind cut corresponds to a Cauchy sequence.
By truth values do you mean Prop or something else?
In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.