I don't know if you know this: In a topos in which Countable Choice holds, the Cauchy reals are isomorphic to the Dedekind reals. In other words, it doesn't matter whether the reals are constructed via Cauchy sequences or Dedekind cuts. But in some toposes where Countable Choice fails, the two objects Dedekind Reals and Cauchy Reals may become non-isomorphic. In the sheaf topos Sh([0,1]) for instance, the Dedekind reals are (externally) the sheaf formed out of the continuous functions [0,1]->R, and the Cauchy reals are the sheaf formed out of the constant functions [0,1]->R.