# 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 |