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.
Revision on May 27, 2020 at 18:54:36 by Ali Caglayan. See the history of this page for a list of all contributions to it.