Natural isomorphisms and the axiom of choice The definitions of "natural transformation", "natural isomorphism between functors", and "natural isomorphism between objects" captures - among other things - the intuitive notion of "an isomorphism that does not depend on an arbitrary choice" (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 "being naturally
isomorphic" somehow related
to "being provably isomorphic from $ZF$ without $AC$"?
Or are these completely unrelated concepts?


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...
