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{𝖿𝗎𝗇𝖾𝗑𝗍}$ which asserts 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).

Title	A.3.1 Function extensionality and univalence