Higher Inductive Types as Homotopy-Initial Algebras