Comment by bmacho

Tangential, but a choice function is one of the ur-examples of Dependent Type Theory (DTT). In standard ZFC the choice function on X would have the type signature

   f: X -> UX (union X).

And you know the additional information that (∀A:X) (f(A) ∈ A), which is not encoded in the type signature, just an additional fact that you know, and have to keep track of it. In DTT the codomain can be the function of the picked element of the domain. In this case, the DTT type signature of f would be

   f: (A:X) -> A. 

So in this case the signature of the function carries strictly more information than in the case of normal, static function type signatures in ZFC. And the axiom of choice simply states that the type (A:X) -> A is non-empty if every A are non-empty.