Consider sets $A, B$, where $B$ is equipped with an equivalence relation $R$. The induced pointwise equivalence is denoted $$f \mathrel{\tilde R} g \iff \forall x, f(x) \mathrel{R} g(x). $$ We have a natural mapping $(A \to B)/\tilde R \to (A \to B/R)$, defined by $\varphi([f], x) = [f(x)]$, where $[u]$ denotes the equivalence class of some element.
Theorem. The statement that $\varphi$ is a bijection for all $A, B, R$ is equivalent to the axiom of choice.
Proof. On one hand, given the axiom of choice and a function $g : A \to B/R$ we can pick a representative for each $g(a)$, getting $\hat g : A \to B$, and $[\hat g]$ is the desired inverse. This is readily verified to be independent of the choice.
On the other hand, if $\varphi$ is a bijection for all $A,B,R$, we can take any surjection $p : B \to A$. Consider the equivalence $$x \mathrel{R} y \iff p(x) = p(y).$$ We have $B/R \cong A$, and therefore the identity function $A \to A$ corresponds to some function $A \to B/R$. By the bijectivity of $\varphi$ we obtain an element $(A \to B)/\tilde R$. This confirms that the set of sections of $p$ is non-empty. $\square$
Consider this weaker statement: Given any $F : (A \to B) \to B$ that satisfies $$f \mathrel{\tilde R} g \implies F(f) \mathrel R F(g),$$ we can produce a lifting $\hat F : (A \to B/R) \to B/R$ such that $\hat F(a \mapsto [f(a)]) = [F(f)]$ holds.
The question: Is this statement equivalent to choice? If not, is it provable in ZF without choice?
Best Answer
The weaker statement requires no choice. Just fix some element $x_0\in B/R$ and define $\hat{F}(f)=[F(\tilde{f})]$ if a lift $\tilde{f}:A\to B$ of $f$ exists and $\hat{F}(f)=x_0$ if no lift of $f$ exists. (This assumes $B/R$ is nonempty; the case where it is empty is trivial.)