Is just one W-type enough for formalizing mathematics?
We certainly do not need very many $W$-types.
If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).