Inductive types in homotopy type theory