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 equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, 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 π–Ώπ—Žπ—‡π–Ύπ—‘π— which asserts that 𝗁𝖺𝗉𝗉𝗅𝗒 is an equivalence: {mathparpagebreakable} \inferrule*[right=Ξ -ext] Ξ“ ⊒f : ∏_(x:A)B
Ξ“ ⊒g : ∏_(x:A)B Ξ“ ⊒funext(f,g) : π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—(happly_f,g) The definitions of 𝗁𝖺𝗉𝗉𝗅𝗒 and π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π— 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=𝒰i-univ] Ξ“ ⊒A : 𝒰 _i
Ξ“ ⊒B : 𝒰 _i Ξ“ βŠ’π—Žπ—‡π—‚π—π–Ίπ—…π–Ύπ—‡π–Όπ–Ύ (A,B) : π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—(π—‚π–½π—π—ˆπ–Ύπ—Šπ— _A,B) The definition of π—‚π–½π—π—ˆπ–Ύπ—Šπ— can be found inΒ (LABEL:eq:uidtoeqv).

Title A.3.1 Function extensionality and univalence
\metatable