W-Types in Homotopy Type Theory