[[!redirects intensional Martin-Loef type theory]] ## Definition ## A __Martin-Loef type theory__ is a [[homotopy type theory]] with all [[W-types]]. ## See also ## * [[homotopy type theory]] * [[cubical type theory]] * [[higher observational type theory]] * [[univalent Martin-Loef type theory]] * [[extensional Martin-Loef type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)