4.9 Univalence implies function extensionality
In the last section of this chapter we include a proof that the univalence axiom implies function extensionality. Thus, in this section we work without the function extensionality axiom. The proof consists of two steps. First we show in Theorem 4.9.4 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprethm1) that the univalence axiom implies a weak form of function extensionality, defined in Definition 4.9.1 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmpredefn1) below. The principle of weak function extensionality in turn implies the usual function extensionality, and it does so without the univalence axiom (Theorem 4.9.5 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprethm2)).
The weak function extensionality principle asserts that there is a function
for any family of types over any type .
The following lemma is easy to prove using function extensionality; the point here is that it also follows from univalence without assuming function extensionality separately.
Assuming is univalent, for any and any , there is an equivalence
of which the underlying map is given by post-composition with the underlying function of .
Let be a family of contractible types, i.e. Then the projection is an equivalence. Assuming is univalent, it follows immediately that precomposition with gives an equivalence
In particular, the homotopy fiber of the above equivalence at is contractible. Therefore, we can show that univalence implies weak function extensionality by showing that the dependent function type is a retract of .
In a univalent universe , suppose that is a family of contractible types and let be the function of Corollary 4.9.3 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprecor1). Then is a retract of . As a consequence, is contractible. In other words, the univalence axiom implies the weak function extensionality principle.
Define the functions
Then , which is , by the uniqueness principle for dependent function types. ∎
We now show that weak function extensionality implies the usual function extensionality. Recall from (2.9.2) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E2) the function which converts equality of functions to homotopy. In the proof that follows, the univalence axiom is not used.
Weak function extensionality implies the function extensionality Axiom 2.9.3 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmpreaxiom1).
We want to show that
Since a fiberwise map induces an equivalence on total spaces if and only if it is fiberwise an equivalence by Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4), it suffices to show that the function of type
induced by is an equivalence. Since the type on the left is contractible by Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), it suffices to show that the type on the right:
is contractible. Now Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) says that this is equivalent to
The proof of Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) uses function extensionality, but only for one of the composites. Thus, without assuming function extensionality, we can conclude that (4.9.6) is a retract of (4.9.7). And (4.9.7) is a product of contractible types, which is contractible by the weak function extensionality principle; hence (4.9.6) is also contractible. ∎
|Title||4.9 Univalence implies function extensionality|