## Definition ## A __univalent Martin-Loef type theory__ is a [[Martin-Loef type theory]] that is also a [[univalent type theory]]. ## See also ## * [[Martin-Loef type theory]] * [[univalent type theory]] * [[book homotopy type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)