I'm currently reading Mac Lane's "Categories for the Working Mathematician", and on page 18 I found a construction which seems to me to use a universal choice function.
Namely, we work with the categories Finord and Setf, the latter being the category of finite sets and the former the category of sets of the form $$ n = \{0, 1, \ldots, n-1\} $$ as a full subcategory of Setf. And in constructing an equivalence of these categories, we choose a function $\theta_X: X \to \#X$ for each finite set $X$, where $\# X$ denotes the cardinality of $X$ (which is, of course, an ordinal number in a canonical way).
Here is my question:
Is there any way this may be accomplished using the axiom of choice, or do we need to assume the existence of a global choice function (or a different axiom stronger than the axiom of choice)?
You need global choice.
Add using an Easton support product two sets of Cohen subsets to each regular $\kappa$, namely force with $\operatorname{Add}(\kappa,2\times\kappa)$. In the resulting model there is no uniform way of assigning sets of size $2$ a bijection with $\{0,1\}$.