# A.3.1 Function extensionality and univalence

There are two basic ways of introducing axioms which do not introduce new syntax or judgmental equalities (function extensionality and univalence are of this form): either add a primitive constant to inhabit the axiom, or prove all theorems which depend on the axiom by hypothesizing a variable that inhabits the axiom, cf.Β Β§1.1 (http://planetmath.org/11typetheoryversussettheory). While these are essentially equivalent, we opt for the former approach because we feel that the axioms of homotopy type theory are an essential part of the core theory.

\autoref

axiom:funext is formalized by introduction of a constant $\mathsf{funext}$ which asserts that $\mathsf{happly}$ is an equivalence: {mathparpagebreakable} \inferrule*[right=$\Pi$-ext] Ξ β’f : β_(x:A)B
Ξ β’g : β_(x:A)B Ξ β’funext(f,g) : $\mathsf{isequiv}$(happly_f,g) The definitions of $\mathsf{happly}$ and $\mathsf{isequiv}$ can be found inΒ (LABEL:eq:happly) and Β§4.5 (http://planetmath.org/45onthedefinitionofequivalences), respectively.

\autoref

axiom:univalence is formalized in a similar fashion, too: {mathparpagebreakable} \inferrule*[right=$\mathcal{U}_{i}$-univ] Ξ β’A : $\mathcal{U}$ _i
Ξ β’B : $\mathcal{U}$ _i Ξ β’$\mathsf{univalence}$ (A,B) : $\mathsf{isequiv}$($\mathsf{idtoeqv}$ _A,B) The definition of $\mathsf{idtoeqv}$ can be found inΒ (LABEL:eq:uidtoeqv).

 Title A.3.1 Function extensionality and univalence \metatable