I don't think there is any confusion here. Of course ZF set theory can express this weaker notion. But in ZF these different functions have different domains and ranges A, A mod r, B, B mod r, where r is the equivalence relation.
In my experience it is type theory which introduces A LOT of confusion. Like the above confused comment.
I am not saying ZF cannot distinguish functions which respect an equivalence relation and those which do not — the axiom of choice concerns equality, not any old equivalence relation.
I am saying that ZF cannot distinguish those sets for which the logical "for all x there exists a y" defines a function. This is because logical equality in ZF can be forced to be be any equivalence relation, without any additional restriction on the logical constructions. This forces us to add extra axioms saying which sets are ok: countable choice, dependent choice etc. At the extreme end there is the axiom saying all sets have this property, with consequences such as Banach-Tarski and Diaconescu's theorem.
Type theory introduces nuances, which may not be appreciated by the non-logician (constructiveness, intensionality…). Homotopy type theory goes some way in mitigating this by allowing quotients (but the logical constructions are suitably restricted to preserve choice), and adding function extensionality (not to mention univalence).
And ZF should'nt distinguish those sets for which the logical "for all x there exists a y" defines a function or not. If you want the notion of a unique function, you should have the logical statement "for all x there exists a unique x".
I have no problem with Banach-Tarski. Sets of points just do not describe properly our intuition of 3-dimensional space. Measurable sets of points more so.
Type theory just shuts out certain things its inventors don't want to think about. How does that help anyone?
The intuition behind the type theoretical axiom of choice is that the choice is given by a (hypothetical) proof of the "∀x ∈ A ∃ y …"-statement. The constructive interpretation of the statement is precisely that there is such a choice function — so it becomes a tautology (provable without any extra axioms). And I believe that agrees with the naive intuition one has why the axiom of choice is true. The problem is when the logic allows proofs (or semantics) which does not preserve the equality. In type theory the equality is intensional and thus preserved by structure.
Unique choice is besides the point here. There may be a unique function, or there may be many. The intuition of choosing is the same.
I also have no issue with B-T, as I expect weird consequences of ZFC; the axioms and logic being so profoundly non-constructive and removed from my intuitions in the first place. That said, I would not deny the set-theorists enjoying their theory, I merely observe that there are subtle things their theories fail to describe.
Type theory does not shout anything, but is carefully constructed from the needs of its creators. Some people want to extract algorithms from their proofs, or want to prove that their algorithms are correct. And if you want this, the nuances of type theory are actually nuances of things you care about — algorithms and proofs. If these are not among your interests, then type theory is not for you. Thats fine, I am sure you have other interests.
In my experience it is type theory which introduces A LOT of confusion. Like the above confused comment.