## Definition ## __Homotopy type theory__ is a [[dependent type theory]] where every [[type]] is a [[homotopy type]], or equivalently where every [[type]] has an [[identity type]] between any two terms of the type. ## See also ## * [[dependent type theory]] * [[univalent type theory]] * [[intensional Martin-Loef type theory]] * [[cubical type theory]] * [[higher observational type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)