Spahn W-type

See §2 in

• Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv:1201.3898