How do we define functions on quotient sets? Let $X$ be a set and $\sim$ an equivalence relation on $X$. I know how to define the quotient set
$$ X/{\sim} := \{ [x] \in \mathcal{P}(X) \mid x \in X \}, $$
but I'm a bit confused about how exactly to define a function on the quotient set. I have seen it done by writing something like
$$ \begin{align}\phi\colon X/{\sim} &\to Y, \\ [x] &\mapsto \phi([x]), \end{align}$$
for some set $Y$, where the definition of $\phi$ makes use of the representative $x$ explicitly in some way, say $\phi([x]) := \psi(x)$ for some $\psi\colon X \to Y$. So assume that we have shown that the function is well-defined.
What exactly do we mean when we write $[x]$ in the definition above? We need to use the representative to find the image of the equivalence class under $\phi$, but how do we choose the representative? Do we need to appeal to the axiom of choice?
Also, I thought there might at least be cases in which we didn't need choice, e.g. if $X$ is well-ordered. We would then construct a set of representatives (without choice), map each equivalence class to its chosen representative and use that to define $\phi$. But the function is not defined in terms of the representatives, but in terms of the equivalence classes themselves, so we presumably still need to show that the image of some equivalence class under $\phi$ is independent of the choice of representative. After all, our choice of representative is not part of the function. And it seems like that still requires choosing a generic element, but I'm very unsure whether that requires choice or not.
In general, I think I'm very confused about when we are making a choice that requires the axiom
 A: The axiom of choice is not needed here (assuming you can define your function $\psi:X\to Y$ without it and the resulting function $\phi$ is well-defined).  Explicitly, define $$S=\{([x],\psi(x)):x\in X\}\subseteq X/{\sim}\times Y.$$
This is a perfectly well-defined set of ordered pairs and no choice is needed to define it.  If this set is actually the graph of a function (in other words, for every element $a\in X/{\sim} \times Y$ there exists a unique $b\in Y$ such that $(a,b)\in S$), then that function is the function $\phi$ you are trying to define.
So to check that we have defined a function, we just need to check that $S$ is the graph of a function.  For any $a\in X/{\sim}$, there exists $x\in a$, and then $a=[x]$ so $(a,\psi(x))=([x],\psi(x))\in S$.  So for any $a\in X/{\sim}$, there exists at least one $b\in Y$ such that $(a,b)\in S$.  We now just have to show this $b$ is unique.  So suppose $(a,b)$ and $(a,c)$ are both elements of $S$.  By definition of $S$, this means there exist $x,y\in X$ such that $(a,b)=([x],\psi(x))$ and $(a,c)=([y],\psi(y))$.  We need to know that $b=c$ under these circumstances.  In other words, we need to know that whenever $[x]=[y]$, we have $\psi(x)=\psi(y)$.
Or, in other words, we need to know that whenever $x\sim y$, we have $\psi(x)=\psi(y)$.  In other words, we need to check that our function $\psi$ always gives the same output on two equivalent inputs, so that defining $\phi([x])=\psi(x)$ gives a well-defined output that is independent of the representative $x$ chosen for the equivalence class $a=[x]$.
So, in this situation we do indeed get a function $\phi$.  Given any $a\in X/{\sim}$, we can evaluate $\phi(a)$ by choosing any $x\in a$ (so that then $a=[x]$) and then we have $\phi(a)=\psi(x)$.  We get the same answer no matter what element $x\in a$ we choose, using our assumption about the function $\psi$.
To put it another way, we can avoid using the axiom of choice by just making all choices simultaneously and then checking that the result is well-defined.  That's what our set $S$ above does: it defines $\phi([x])=\psi(x)$ for all possible representatives $x$ of an equivalence class, without singling out any choice.  Then we just have to check that this really is a function.

Now, where does the axiom of choice come in?  It comes in when you don't actually have a function $\psi$ satisfying this property at all, but still want to somehow define a function $\phi$.  In other words, you want to define $\phi(a)=\psi(x)$ for some $x\in a$, but $\psi(x)$ will actually give a different answer depending on what $x\in a$ you choose so the construction above does not define a function.
In this case, what you do instead is use a choice function (via the axiom of choice or otherwise) $p:X/{\sim}\to X$ such that $p(a)\in a$ for each $a\in X/{\sim}$, and then define $\phi(a)=\psi(p(a))$.  That is, we define $\phi(a)$ to be $\psi(x)$ where $x$ is our specific representative of $a$ that is chosen by the choice function $p$, rather than any arbitrary element of $a$.  When we do this construction, we do not have to check that anything is well-defined, since $\phi$ is defined as a composition of two functions and therefore is automatically a function.
A: When you write $[x]$, this is a very explicit and very concrete subset of $X$. So when you want to define $\phi([x])$, you really want to define it for the equivalence class.
This is fine, and no use of the axiom of choice is needed. However, if your definition of $\phi([x])$ somehow depends on $x$, then you need to verify that for $x'\in[x]$, the definition yields the same result. This is what it means to be well-defined.
So for example, $\phi([x])=[x]$ does not depend on $[x]$, it's just the identity function, and it's easier to see as $\phi(A)=A$ for $A\in X/{\sim}$, for that matter. But something like $[x]+[y]=[x+y]$, certainly depends on the values of $x$ and $y$, and you want to show that $+$ as defined on $X$ behaves nicely with respect to $\sim$. This requires, in the majority of cases, no choice. Since you only need to work one or two equivalence classes at a time, so you're only choosing two members from a non-empty set. No choice is used for that.
Using representatives is a tricky thing, though. While on its own, the existence of a system of representative from an arbitrary equivalence relation is the enough to prove the full axiom of choice, it is worth noting that you already assumed that $\phi$ is well-defined. In that case $\psi(x)$ is literally defined as $\phi([x])$, which is the other way around and no choice was used for that. Of course, I suspect that you meant that first you chose representatives, then you had the function $\psi$ and then you defined $\phi([x])=\psi(x')$, where $x'$ is the representative for $[x]$. But if that's not the case, and you first had $\phi$, and only then defined $\psi$, then choice was not used at all.
