Why are W-types called "W"?
Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions associated to order theory, whereas W-types don't directly have to do with order relations (if at all).
You write:
Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with order relations (if at all).
I don’t know an official source for this, but I’ve always assumed W stands for “well-founded” as you suggest. (Edit: I asked Per Martin-Löf, and he confirmed that this was what he meant by it.) The justification for this is several-fold.
On the one hand, W-types do naturally carry well-founded partial orders (the structurally smaller relation), and the recursion/induction principles of W-types can be seen as well-founded induction over these orders.
On the other hand, well-foundedness was originally defined and developed to analyse and explain induction principles — it ended up becoming part of “order theory”, but it was motivated by Cantor’s analysis of induction. W-types give an alternative analysis of induction principles, not starting with an order relation — so as such, they can be seen as an alternative exploration of the original intention of well-foundedness.
And on the third hand, an important way of viewing W-types is as types of well-founded labelled trees, in exactly the traditional order-theoretic sense of well-founded trees. This can be made precise in two directions. If you are modelling type theory with W-types inside set theory (or indeed any other foundation without native inductive types), one way to model W-types is to define them as sets of isomorphism classes of suitably-labelled well-founded trees. On the other hand, inside type theory, you can associate to each element of a W-type a well-founded labelled tree, and show that elements of the W-type correspond precisely to isomorphism classes of such trees.
