## Definition ## A __univalent type theory__ is a [[homotopy type theory]] with [[universes]] such that all universes are [[univalent universes]]. ### Examples ### * [[univalent Martin-Loef type theory]] * [[cubical type theory]] * [[higher observational type theory]] ## See also ## * [[dependent type theory]] * [[homotopy type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)