W-types in homotopy type theory. (June 2015)