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.

axiom:funext is formalized by introduction of a constant $\mathrm{𝖿𝗎𝗇𝖾𝗑𝗍}$ whichasserts that $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ is an equivalence:*[right=$\mathrm{\Pi }$-ext]Γ ⊢f : ∏_(x:A)B
Γ ⊢g : ∏_(x:A)BΓ ⊢funext(f,g) : $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}$(happly_f,g)The definitions of $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ and $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}$ can be found in (LABEL:eq:happly) and§4.5 (http://planetmath.org/45onthedefinitionofequivalences), respectively.

axiom:univalence is formalized in a similar fashion, too:*[right=${𝒰}_i$-univ]Γ ⊢A : $𝒰$ _i
Γ ⊢B : $𝒰$ _iΓ ⊢$\mathrm{𝗎𝗇𝗂𝗏𝖺𝗅𝖾𝗇𝖼𝖾}$ (A,B) : $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}$($\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$ _A,B)The definition of $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$ can be found in (LABEL:eq:uidtoeqv).