A.3 Homotopy type theory

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

Title A.3 Homotopy type theory