## Idea ## *Book HoTT* is the name given to the type theory presented in the [[HoTT Book]]. There are two presentations of this type theory given in Appendix A. Book HoTT can be regarded as intentional [[Martin-Löf Type Theory]] together with the [[univalence axiom]] and various [[higher inductive types]]. category: type theory