Homotopy-Initial Algebras in Type Theory