The definitions provided appear as though they are constructive, but they are not actually constructive, they are set-theoretic existence claims that quantify over all sequences, in particular over undefinable sets. Specifically, the description that appears constructive doesn't actually define any particular real number, it only defines the universe in which the real numbers live.

Another subtle detail is that while it's true that every real number corresponds to (and can be represented by) a Cauchy sequence of rationals, the very sequence itself might be undefinable.