Showing changes from revision #1 to #2:
Added | Removed | Changed
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.