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 which
asserts that is an equivalence:
Γ ⊢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.
axiom:univalence is formalized in a similar fashion, too:
Γ ⊢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|