For the sake of concreteness let's say we're talking about ZF, though I imagine this question can be asked for any 'typical' set theory without a choice axiom (and would prefer an answer that doesn't rely on some particular detail about ZF specifically).
Let $X$ be a set and $\mathcal{P}X$ its power set. Cantor's theorem states that there exists no surjective map $X \to \mathcal{P}X$ (and therefore no bijection between the two). The usual proof of this fact by diagonalization is entirely constructive, and goes through just fine in an intuitionistic setting without the use of any choice axioms.
One might ask about a dual version of this theorem: that there exists no injective map $\mathcal{P}X \to X$.
Can this be proven without appeal to a choice axiom?
Can it be proven without appeal to the law of excluded middle?
Best Answer
As far as the axiom of choice part goes, this is quite easy. If $f\colon X\to Y$ is an injective function, the either $X$ is empty, or there is $g\colon Y\to X$ such that $g(f(x))=x$.
To see this, note that if $x$ is not empty, then we can fix $x_0\in x$ and define $g(y)=x$ exactly when $f(x)=y$, and if not such $x$ exists, then $g(y)=x_0$.
No choice necessary here. But of course, we did rely on excluded middle quite a lot. For example, every set is empty or not; $y$ is in the range of $f$ or is not.
I am not the expert to remark on usage of excluded middle, so I will leave this to someone else.