Does $2^X=2^Y\Rightarrow |X|=|Y|$ imply the axiom of choice? The Generalized Continuum Hypothesis can be stated as $2^{\aleph_\alpha}=\aleph_{\alpha+1}$. We know that GCH implies AC (Jech, The Axiom of Choice, Theorem 9.1 p.133).
In fact, a relatively weak formulation: $|X|\le|Y|< 2^X\implies |X|=|Y|$ would already imply the axiom of choice, although in this case the proof is slightly longer. [Note: in Herrlich's book he refers to GCH stated above as "The Aleph Hypothesis" and the weak formulation is called GCH]
GCH itself is independent of the axiom of choice, we can have the axiom of choice and power sets can grow wildly, or just "a little bit". We can have the continuum function to be injective, but the continuum hypothesis can fail on a proper class of cardinals (for example $2^\kappa=\kappa^{++}$ for regular cardinals).
Let ICF (Injective Continuum Function) be the assertion: $$2^X=2^Y\implies |X|=|Y|.$$
Question: Assuming ZF+ICF, can we deduce AC?
(I looked around Equivalents of the Axiom of Choice, but couldn't find much. It is possible that I missed this, though.)

Edits:

*

*In an exercise in Jech he states that if there exists an infinite Dedekind-finite cardinal, then ICF does not hold. From the assumption that it holds we can deduce that there are no infinite D-finite sets.


*Note that if $f\colon X\to Y$ is a surjection then $A\subseteq Y\mapsto f^{-1}(A)$ is an injection from $P(Y)$ into $P(X)$. This means that ICF implies the Dual Cantor-Schroeder-Bernstein theorem:
Assume that $X$ and $Y$ have surjections from one onto the other, then there are injections between their power-sets therefore $2^X=2^Y$ and thus $|X|=|Y|$.


*We shall abbreviate Goldstern's variant of ICF as Homomorphic Continuum Function, or HCF: $$2^X\leq 2^Y\implies |X|\leq|Y|$$
One major observation is that HCF implies The Partition Principle (PP), which states that $A$ can be mapped onto $B$ (or $B$ is empty) if and only if $B$ can be injected into $A$. This principle is quite an open choice principle, and it is unknown whether or not it implies AC in ZF.
To see that HCF implies PP, we observe the following: if $f\colon A\to B$ is surjective then the preimage map is an injection from $2^B$ into $2^A$, i.e. $2^B\leq 2^A$, from HCF it follows that $B\leq A$, i.e. there is $g\colon B\to A$ injective.
 A: Here is a little progress towards AC.
Theorem.
 ICF implies the dual Cantor-Schröder-Bernstein
theorem, that is $X$ surjects onto $Y$ and $Y$ surjects onto $X$,
then they are bijective.
Proof. You explain this in the edit to the question. If
$X\twoheadrightarrow Y$, then $2^Y\leq 2^X$ by taking pre-images,
and so if also $Y\twoheadrightarrow X$, then $2^X\leq 2^Y$ and so
$X\sim Y$ by ICF. QED
Theorem. ICF implies that there are no infinite D-finite
sets.
Proof. (This is a solution to the exercise that you mention.) If $A$ is infinite and
Dedekind-finite, then let $B$ be the set of all finite
non-repeating finite sequences from $A$. This is also D-finite,
since a countably infinite subset of $B$ easily gives rise to a
countably infinite subset of $A$. But meanwhile, $B$ surjects onto
$B+1$, since we can map the empty sequence to the new point, and
apply the shift map to chop off the first element of any sequence.
So $B$ and $B+1$ surject onto each other, and so by the dual
Cantor-Schöder-Bernstein result, they are bijective,
contradicting the fact that $B$ is D-finite. QED
Here is the new part:
Theorem. ICF implies that $\kappa^+$ injects into
$2^\kappa$ for every ordinal $\kappa$.
Proof. We may assume $\kappa$ is infinite. Notice that
$2^{\kappa^2}$ surjects onto $\kappa^+$, since every
$\alpha<\kappa$ is coded by a relation on $\kappa$. Since
$\kappa^2\sim\kappa$, this means
$2^\kappa\twoheadrightarrow\kappa^+$ and consequently
$2^{\kappa^+}\leq 2^{2^\kappa}$, by taking pre-images. It follows that
$2^{2^\kappa}=2^{2^\kappa}\cdot 2^{\kappa^+}=2^{2^\kappa+\kappa^+}$ and
so by ICF we get $2^\kappa+\kappa^+=2^\kappa$, which implies
$\kappa^+\leq 2^\kappa$, as desired. QED
This conclusion already contradicts AD, for example, since AD
implies that there is no $\omega_1$ sequence of distinct reals,
which violates the conclusion when $\kappa=\omega$. In particular,
this shows that ICF implies $\neg$AD, and so in every AD model, there are sets of different cardinalities, whose power sets are equinumerous.
