Choosing a Cauchy sequence for a real 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. 
 A: Such a choice mechanism would translate to a canonical choice for a function $\Bbb N \to \Bbb N_{>0}$ from a given set $S$ of such functions. If I'm not mistaken, this is some nontrivial choice principle (and if I am, please do correct me).
Given $f: \Bbb N \to \Bbb N_{>0}$, define: $$b_f (n) = \begin{cases}2^{-k} &: n = \sum\limits_{i=0}^k f(i) \\0&: \text{otherwise}\end{cases}$$
Now define $s_f(n) = \sum\limits_{i=0}^n b_f(i)$. Then for all $f$: $$\lim_{n\to\infty} s_f(n) = 2$$
and $f \leftrightarrow s_f$ is a bijective correspondence. Hence a choice function for each set $\{s_f: f \in S\}$ amounts to a choice function for each $S \subseteq (\Bbb N_{>0})^{\Bbb N}$.

By defining, for $f: \Bbb N \to 2$: $$b_f(n) = \begin{cases}2^{-k} &: n = k + \sum\limits_{i=0}^k f(i) \\0&: \text{otherwise}\end{cases}$$ the argument seems to carry over to $2^{\Bbb N}$.
A: Let me take Lord_Farin's answer, and crank it all the way to $2^{\aleph_0}$.
Suppose that we could have chosen from any family of Cauchy sequences. Fix for each real number a canonical Cauchy sequence of rationals $r_n$ which is strictly increasing. This is of course doable without choice.
Now suppose that $A_r\subseteq 2^\omega\setminus 2^{<\omega}$ is non-empty for each $r\in\Bbb R$, then consider $C_r=\{\langle r_n\mid a_n\neq 0\rangle\mid\langle a_n\rangle\in A_r\}$. Namely we encode each $a\in A_r$ as a subsequence of $r_n$, with the assumption that $a$ is not eventually $0$.
By the assumption there will be a choice from each $C_r$, and then we can easily decode this into a choice from $A_r$. So we have proved the axiom of choice for families of size $\leq2^{\aleph_0}$ of sets of reals. And of course we cannot even prove choice for countable families of sets of reals in $\sf ZF$ itself.
