There is a difference between the meaning of a statement and its truth value. Logical equivalence preserves truth values but not meanings. Thus the statements "all unicorns have two horns" and "1 + 1 = 2" are both true, hence equivalent, but they have different meanings. Likewise, the axiom of choice and the well-ordering principle have different meanings, even though they are equivalent. If you wonder about AC being equivalent to a well-ordering principle, you should also wonder about many other equivalences in mathematics that relate statements with different meanings. As for your question "what is a choice principle, really?" I would say that choice principles are a certain kind of reversal of quantifiers. The axiom of choice can be stated as $$(\forall x \in A . \exists y \in B . \phi(x,y)) \implies \exists f \in B^A . \forall x \in A . \phi(x, f(x))$$ where $\phi$ is a relation between the sets $A$ and $B$. This for of the axiom of choice does not require any set theory, just a bit of simple type theory and first-order logic (if you read schematically in $\phi$). **Exercise:** convince yourself that the above statement is equivalent to AC. Hint: given a family of sets $(C_i)_{i \in I}$ let $A = I$, $B = \bigcup_{i \in I} C_i$ and $\phi(i, x) \iff x \in C_i$. Conversely, given $A$, $B$ and $\phi$, let $I = A$ and $C_i = \{y \in B \mid \phi(i,y)\}$. A category theorist might say that choice is about splitting epis. **Exercise:** given a family $(C_i)_{i \in I}$, consider the map $e : \coprod_{i \in I} C_i \to I$ defined by $e (i,x) = i$. Then $(C_i)_{i \in I}$ is a family of non-empty sets if, and only if, $e$ is surjective (epi), and it has a choice map if, and only if, $e$ has a right inverse (is split).