I was trying to prove this statement:
Let $f:X\to Y$ a surjective map and $g: X\to Z$ such that $$\forall\,x,y\in X: f(x)=f(y)\implies g(x)=g(y).$$ Then exists a unique map $h:Y\to Z$ such that $g=h\circ f.\,\,(\ast)$
using the Axiom of Choice, as follows.
Since $f$ is surjective, the fiber $f^{-1}(\{y\})$ is non-empty for each $y\in Y$: thanks to AC, exists a choice function $\sigma: Y\to X$ such that $\forall\, y\in Y: \sigma(y)\in f^{-1}(\{y\})$. Now, $h:=g\circ\sigma$ satisfies $(\ast)$ because $$\forall\,x\in X: h(f(x))=g(\sigma(f(x)))=g(x)$$ since $f(\sigma(f(x)))=f(x)$ from its definition and the hypothesis on $g$. Moreover, if $h':Y\to Z$ satisfies $(\ast)$, we can conclude that $h'=h$: in fact, for all $y\in Y$ we have that $$h'(y)=h'(f(\sigma(y)))=g(\sigma(y))=h(f(\sigma(y)))=h(y).$$
I'd like to understand if my use of AC is correct and necessary because I actually struggle a lot to find when I do need it and when not... For example, I suspect it is necessary here because we don't know if $Y$ is finite and there's no common property among the fibers of $f$ that allows me to pick a particular element from each one at the same moment. Any help on the question -- and tips on the proper use of AC in general -- is appreciated!
Since we can assume $g$ is a surjection as well, it's really not about functions. It's about the partitions they induce. What the condition say, is that the partition induced by $f$ refines the partition induced by $g$. Namely, a fiber of $g$ is the union of fibers of $f$.
So there is really no need to use AC here. Since $f$ induces a partition of the partition induced by $g$, it also induces that unique function you described.
In general, any type of finitary definition will not really depend on AC. Indeed, if you want to be explicit, simply define $$h=\{(f(x),g(x))\mid x\in X\}$$ Now the condition on $f$ and $g$ proves that this is a function and it is not hard to prove that it satisfies the needed conditions.