## Definition ## In [[dependent type theory]], a __homotopy type__ is a type with some sort of [[identity types]] between any two terms in the type. ## See also ## * [[dependent type theory]] * [[identity type]] * [[identity system]] * [[homotopy type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)