Book HoTT

*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

Created on May 27, 2020 at 14:50:23. See the history of this page for a list of all contributions to it.