Natural isomorphisms and the axiom of choice The definitions of &quot;natural transformation&quot;, &quot;natural isomorphism between functors&quot;, and &quot;natural isomorphism between objects&quot; captures - among other things - the intuitive notion of &quot;an isomorphism that does not depend on an arbitrary choice&quot; (from Wikipedia). The standard example is a finite dimensional vector space $V$ being naturally isomorphic to its double dual $V$** because the isomorphism doesn't depend on the choice of basis.
What I wonder:

Does this informal notion of choice have to do
with the formal notion of choice in the axiom of
choice?
Is &quot;being naturally
isomorphic&quot; somehow related
to &quot;being provably isomorphic from $ZF$ without $AC$&quot;?
Or are these completely unrelated concepts?
"Naturality" in a categorical sense is much more than "not depending on choices", and, also, is essentially unrelated to issues about the Axiom of Choice.

In the example of vector spaces over a field, we can look at the category of _finite_dimensional_ vector spaces, to avoid worrying about using AxCh to find elements of the dual. The non naturality of any isomorphisms of finite-dimensional vectorspaces with their duals resides in the fact that, provably, as a not-hard exercise, there is no collection of isomorphisms $\phi_V:V\rightarrow V^*$ of isomorphisms of f.d. v.s.'s $V$ to their duals, compatible with all v.s. homs $f:V\rightarrow W$. 

In contrast, the isomorphism $\phi_V:V\rightarrow V^{**}$ to the second dual, by $\phi_V(v)(\lambda)=\lambda(v)$ is compatible with all homs, as an easy exericise! This latter compatibility is the serious meaning of "naturality".

True, if capricious or random choices play a role, the chance that the outcome is natural in this sense is certainly diminished! But that aspect is not the defining property!

Edit (16 Apr '12): as alancalvitti notes, the ubiquity of adjunctions, and the naturality and sense of "naturality", and counter-examples to naive portrayals, deserve wider treatment at introductory levels. After all, this can be done with almost no serious "formal" category-theoretic overhead, and pays wonderful returns, at the very least organizing one's thinking. Distinguishing "characterization" from "construction-to-prove-existence" is related. E.g., "Why is the product topology so coarse?": to say that "it's the definition" is unhelpful; to take the categorical definition of "product" and _find_out_ what topology on the cartesian product of sets is the categorical product topology is a do-able, interesting exercise! :)
I'm no expert but I think they're different. My understanding is that "natural isomorphism" has always been a little vaguely defined but the concept is fairly intuitive.

It's a case where there is clearly a "best" or simplest isomorphism. Like the Chinese Remainder Theorem perhaps. Cmn ~ Cm x Cn where m, n are relatively prime. There may be more than one isomorphism but one stands out as the most natural or most obvious, I guess.

Generally the "natural" isomorphisms are easily and unambiguously provable. It's recognising that such a connection exists that's the real art. Funnily enough I find the axiom of choice much vaguer (and have never been a fan).

I'm probably way off...