4.9 Univalence implies function extensionality

In the last sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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)).

Let 𝒰 be a universePlanetmathPlanetmath; we will explicitly indicate where we assume that it is univalent.

Definition 4.9.1.

The weak function extensionality principle asserts that there is a function


for any family P:A→U of types over any type A.

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.

Lemma 4.9.2.

Assuming U is univalent, for any A,B,X:U and any e:A≃B, there is an equivalence


of which the underlying map is given by post-composition with the underlying function of e.


As in the proof of Lemma 4.1.1 (http://planetmath.org/41quasiinverses#Thmprelem1), we may assume that e=π—‚π–½π—π—ˆπ–Ύπ—Šπ—β’(p) for some p:A=B. Then by path inductionMathworldPlanetmath, we may assume p is 𝗋𝖾𝖿𝗅A, so that e=𝗂𝖽A. But in this case, post-composition with e is the identityPlanetmathPlanetmathPlanetmathPlanetmath, hence an equivalence. ∎

Corollary 4.9.3.

Let P:Aβ†’U be a family of contractible types, i.e. ∏(x:A)isContr⁒(P⁒(x)). Then the projection pr1:(βˆ‘(x:A)P⁒(x))β†’A is an equivalence. Assuming U is univalent, it follows immediately that precomposition with pr1 gives an equivalence


By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), for 𝗉𝗋1:βˆ‘(x:A)P⁒(X)β†’A and x:A we have an equivalence


Therefore 𝗉𝗋1 is an equivalence whenever each P⁒(x) is contractible. The assertion is now a consequence of Lemma 4.9.2 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprelem1). ∎

In particular, the homotopy fiber of the above equivalence at 𝗂𝖽A is contractible. Therefore, we can show that univalence implies weak function extensionality by showing that the dependent function type ∏(x:A)P⁒(x) is a retract of 𝖿𝗂𝖻α⁒(𝗂𝖽A).

Theorem 4.9.4.

In a univalent universe U, suppose that P:Aβ†’U is a family of contractible types and let Ξ± be the function of Corollary 4.9.3 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprecor1). Then ∏(x:A)P⁒(x) is a retract of fibα⁒(idA). As a consequence, ∏(x:A)P⁒(x) is contractible. In other words, the univalence axiom implies the weak function extensionality principle.


Define the functions

Ο† :∏(x:A)P⁒(x)→𝖿𝗂𝖻α⁒(𝗂𝖽A),
φ⁒(f) :≑(Ξ»x.(x,f(x)),𝗋𝖾𝖿𝗅𝗂𝖽A),
ψ :𝖿𝗂𝖻α⁒(𝗂𝖽A)β†’βˆ(x:A)P⁒(x),
ψ⁒(g,p) :≑λx.p*(𝗉𝗋2(g(x))).

Then ψ⁒(φ⁒(f))=λ⁒x.f⁒(x), which is f, 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 𝗁𝖺𝗉𝗉𝗅𝗒(f,g):(f=g)β†’(f∼g) which converts equality of functions to homotopy. In the proof that follows, the univalence axiom is not used.

Theorem 4.9.5.

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 Ξ»(g:∏(x:A)P(x)).𝗁𝖺𝗉𝗉𝗅𝗒(f,g) 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:

βˆ‘(g:∏(x:A)P(x))∏(x:A)f⁒(x)=g⁒(x) (4.9.6)

is contractible. Now Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) says that this is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to

∏(x:A)βˆ‘(u:P(x))f⁒(x)=u. (4.9.7)

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 productMathworldPlanetmathPlanetmathPlanetmath 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