Is there a constructive proof that $2^X$ can't inject into $X$? Let $X$ be a set.  Constructively, it is not hard to show that $\mathcal{P}(X)$ does not inject into $X$:  If $f : \mathcal{P}(X) \rightarrow X$ is an injection, consider $D := \lbrace x \in X \mid  \exists Y f(Y) = x \wedge x \not\in Y \rbrace$.  Then $f(D) \in D \Leftrightarrow f(D) \not\in D$.
However, this argument doesn't carry over if we replace $\mathcal{P}(X)$ with $2^X$, since the $D$ from above cannot generally be assumed to be decidable.  Is there another argument that works for $2^X$ or is the statement that $2^X$ doesn't inject into $X$ independent of constructive mathematics?
Edit:  $2^X$ is the set of functions from $X$ to $\lbrace 0,1\rbrace$, or equivalently, the decidable subsets of $X$.  In constructive mathematics we are not able to conflate $\mathcal{P}(X)$ and $2^X$.
 A: It's consistent with constructive mathematics that there is an injection from $\mathbb{N}^\mathbb{N} \rightarrow \mathbb{N}$, and in particular composing with the inclusion $2^\mathbb{N} \hookrightarrow \mathbb{N}^\mathbb{N}$ gives an injection $2^\mathbb{N} \rightarrow \mathbb{N}$.
This was proved not so long ago by Andrej Bauer in An injection from the Baire space to natural numbers. The proof is basically to work in a realizability model over infinite time Turing machines. Similarly to the more usual forms of realizability, in the model the functions $\mathbb{N} \rightarrow \mathbb{N}$ are those that are computable by some infinite time Turing machine, $\psi_e$. However, with infinite time Turing machines we can compute a partial function $r : \mathbb{N} \rightarrow \mathbb{N}$ such that if $\psi_e$ is total, then $r(e)$ is defined and $\psi_{r(e)} = \psi_e$, and so that if $\psi_e = \psi_{e'}$ (ie $e$ and $e'$ are programs that happen to give the same function), then $r(e) = r(e')$. In the realizability model, this means that we get an actual well defined function $R\colon \mathbb{N}^{\mathbb{N}} \rightarrow \mathbb{N}$ such that for any $f \in \mathbb{N}^\mathbb{N}$, $f = \psi_{R(f)}$. Any such function is necessarily injective.
