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