A.3 Homotopy type theory
In this section we state the additional axioms of homotopy type theory which distinguish it from standard Martin-Löf type theory
: function extensionality, the
univalence axiom, and higher inductive types. We state them in the style
of the second presentation
\autorefsec:syntax-more-formally, although the first presentation \autorefsec:syntax-informally could be used just as well.
| Title | A.3 Homotopy type theory |
|---|---|
| \metatable |