It is easy to form in ZF, for each real $a$, a "canonical" Cauchy sequence that converges to $a$. For example, one can take the sequence of finite initial segments of the decimal expansion of $a$, being careful when $a$ is a base-10 rational to pick one of the two decimal expansions explicitly.
But what if we are given a set of Cauchy sequences of rationals, all converging to the same real. The set might not contain all the Cauchy sequences for that real. How hard is it to pick a "canonical" representative from the sequences that are in the set?
To make this question precise: consider a family of sets $C$ so that each $X \in C$ is a set of Cauchy sequences of rationals that all converge to the same real $a(X)$. Note that $X$ is not required to have the entire set of Cauchy sequences for $a(X)$. Does ZF prove the existence of a choice function for each family $C$ of this kind?
There are two aspects of Cauchy sequences that make this problem interesting. First, every infinite subsequence of a Cauchy sequence is again a Cauchy sequence converging to the same real. So we cannot hope for a "minimal" sequence. Also, we may prepend any finite sequence to a Cauchy sequence to yield a new Cauchy sequence converging to the same real. So we cannot hope for a "maximal" sequence. Cauchy sequences are very slippery in this way.
Dedekind cuts behave differently: once we specify whether cuts for rationals can have a maximum element, we have a unique Dedekind cut for each real, whereas we always have infinitely many Cauchy sequences.
I have a vague memory of encountering something similar to this question in the past, but I cannot remember any details. It also seems to have a flavor related to Borel equivalence relations, although this question is not written in that way.