Is "every non-empty set is injective" equivalent to AC?

Question

It is well known that "every surjection has a section" is an equivalent form of the axiom of choice (in fact, for me it is the most natural formulation of the axiom of choice). In detail, the statement is that for any map $f:X\to Y$ such that for every $y\in Y$ there is an $x\in X$ with $f(x)=y$ there is a map $s:Y\to X$ with $f(s(y))=y$ for every $y\in Y$.

Consider the statement "every injection with non-empty domain has a retraction". In detail, for any map $f:X\to Y$ such that $X$ is not empty and $f(x)=f(x')$ implies $x=x'$ for any $x,x'\in X$, there is a map $r:Y\to X$ with $r(f(x))=x$ for every $x\in X$.

Is this statement also equivalent to the axiom of choice? If not, is it weaker or stronger? What are some "well-established" set-theoretic principles equivalent to it?

Answer 1

No. Fix a point $x'\in X$ and define$$\begin{array}{rccc}r\colon&Y&\longrightarrow&X\\&y&\mapsto&\begin{cases}x&\text{ if $y=f(x)$ for some }x\in X\\x'&\text{ otherwise.}\end{cases}\end{array}$$

Answer 2

Previous answer shows proving your statement does not require the axiom of choice. Your statement, however, implies the weak excluded middle. We will work over CZF and take the terminology $0=\{\}$ and $1=\{0\}$.

Let $\phi$ be a $\Delta_0$-formula. Take $a = \{0\mid \phi\}$ and consider the inclusion map $i:\{0,1\}\to \{0,a,1\}$. Assume that $i$ has a corresponding retraction $r:\{0,a,1\}\to \{0,1\}$, then $r(a)=0$ or $r(a)=1$.

Now assume that $r(a)=0$ and $\phi$. The combination of them implies $r(1)=0$. However $r(1) = r(i(1)) = 1$, a contradiction. Hence $r(a)=0$ implies $\lnot\phi$. Similarly we can prove $r(a)=1$ implies $\lnot\lnot\phi$. In summary, we have $\lnot\phi\lor\lnot\lnot\phi$.

As the proof suggests, your statement implies weak excluded middle for any formulas if we assume the full separation.