## Idea ## The [[homotopy type theory]] presented in the [[HoTT book]]. ## Definition ## __Book homotopy type theory__ is a [[univalent Martin-Loef type theory]] with all [[higher inductive types]]. ## See also ## * [[homotopy type theory]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)