You think the Axiom of Choice is something? Boy, do I have something for you...
https://en.wikipedia.org/wiki/Axiom_of_global_choice

>>16718151 (OP)
The axiom of global choice is almost the same thing of the axiom of "local choice" (a.k.a the ordinary axiom of choice you've always heard about). See e.g. "The theory of Zermelo-Fraenkel sets with Hilbert ɛ-terms" By V.N. Grishin

>>16718225
It's not. It's much more powerful, especially in the context of category theory. For example, it lets you extend Cat, the category of all small categories, to the category of all categories.

Here's roughly the idea. Let f be a new function symbol,let F be a new binary relation symbol added to the language of ZFC. Let T be the theory ZFC+ the axioms "F is the graph of the function f" "forall x, x!= empty_set => f(x) belongs to x" and "f(empty_set) = empty_set". For every property x ->P(x), we interpret the global choice operator t(P) as f(X_P) where (relying upon the foundation axiom), X_P is the set of objects satisfying P and having minimal rank.
NB: f is not mandatory (we can discard it and express all the above axioms in terms of F alone and use extensions by definitions; we'll assume that from now)
In summary, ZF + global choice is interpreted in T.

It turns out that T is a conservative extension of ZFC to see it consider the following forcing construction: let C be the class of maps g such that for every non empty x in domain(g), g(x) belongs to x and g(empty_set) = empty_set. We define g <= h:= h extends g. We set for every p in C, "p ||- x % y":= x % y (when % is the equal symbol or the belongs symbol). "p ||- F(x,y)":= for all q >= p, there exists r >= q such that (x,y) belongs to r; "p ||- false":= false, "p ||- A => B":= forall q>= p, (q ||- A) => (q ||- B) and "p ||- forall x A":= forall x, p ||- A.

It can be checked that all ZFC axioms are forced by this forcing relationship (including the replacement scheme all formulas,even those featuring F, which is the tricky part of the theorem), and that for any formula P not containing F and any q in C, q ||- P implies P.

>>16718228
It is not more powerful in the sense that you don't prove more theorems however it is much more expressive and convenient to use I agree (Grothendieck explicitely recommended its usage in SGA 4)

>>16718151 (OP)
no i dont think the axiom of choice is anything real

>>16718228
> especially in the context of category theory.
I thought all you guys had kys already

>>16718840
The smaller prime larger than 3^(3^(3^n)) isn't real either when n is larger than 20 and yet so-called constructive maths says it is (because of some views about "algorithms" that they don't even realize the blatant platonist content).

>>16718845
>>>16718228
Category theory is alive and well (though they communicate with the outside world in a very poor way).