# 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