4.9 Univalence implies function extensionality

In the last section of this chapter we include a proof that the univalence axiom implies functionextensionality. Thus, in this section we work without the function extensionality axiom.The proof consists of two steps. First we showin Theorem 4.9.4 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprethm1) that the univalenceaxiom implies a weak form of function extensionality, defined in Definition 4.9.1 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmpredefn1) below. Theprinciple 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 universe; we will explicitly indicate where we assume that it is univalent.

Definition 4.9.1.

The weak function extensionality principleasserts that there is a function

$$\left(\prod _{x:A}\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(P(x))\right)\to \mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}\left(\prod _{x:A}P(x)\right)$$

for any family $P\mathrm{:}A\mathrm{\to }\mathrm{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 $\mathrm{U}$ is univalent, for any $A\mathrm{,}B\mathrm{,}X\mathrm{:}\mathrm{U}$ and any $e\mathrm{:}A\mathrm{\simeq }B$, there is an equivalence

$$(X\to A)\simeq (X\to B)$$

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

Proof.

As in the proof of Lemma 4.1.1 (http://planetmath.org/41quasiinverses#Thmprelem1), we may assume that $e=\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p)$ for some $p:A=B$.Then by path induction, we may assume $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_A$, so that $e={\mathrm{𝗂𝖽}}_A$.But in this case, post-composition with $e$ is the identity, hence an equivalence.∎

Corollary 4.9.3.

Let $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ be a family of contractible types, i.e. ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathrm{isContr}\mathit{}\mathrm{(}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{)}\mathrm{.}$Then the projection ${\mathrm{pr}}_{\mathrm{1}}\mathrm{:}\mathrm{(}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{)}\mathrm{\to }A$ is an equivalence. Assuming $\mathrm{U}$ is univalent, it follows immediately that precomposition with ${\mathrm{pr}}_{\mathrm{1}}$ gives an equivalence

$$\alpha :(A\to \sum _{x:A}P(x))\simeq (A\to A).$$

Proof.

By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), for ${\mathrm{𝗉𝗋}}_1:{\sum }_{(x:A)}P(X)\to A$ and $x:A$ we have an equivalence

$${\mathrm{𝖿𝗂𝖻}}_{{\mathrm{𝗉𝗋}}_1}(x)\simeq P(x).$$

Therefore ${\mathrm{𝗉𝗋}}_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 ${\mathrm{𝗂𝖽}}_A$ is contractible. Therefore, we can show that univalence implies weak function extensionality by showing that the dependent function type ${\prod }_{(x:A)}P(x)$ is a retract of ${\mathrm{𝖿𝗂𝖻}}_{\alpha }({\mathrm{𝗂𝖽}}_A)$.

Theorem 4.9.4.

In a univalent universe $\mathrm{U}$, suppose that $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ is a family of contractible typesand let $\alpha$ be the function of Corollary 4.9.3 (http://planetmath.org/49univalenceimpliesfunctionextensionality#Thmprecor1).Then ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ is a retract of ${\mathrm{fib}}_{\alpha }\mathit{}\mathrm{(}{\mathrm{id}}_A\mathrm{)}$. As a consequence, ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ is contractible. In other words, the univalence axiom implies the weak function extensionality principle.

Proof.

Define the functions

$\phi$$:{\prod }_{(x:A)}P(x)\to {\mathrm{𝖿𝗂𝖻}}_{\alpha }({\mathrm{𝗂𝖽}}_A),$

$\phi (f)$$:\equiv (\lambda x.(x,f(x)),{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗂𝖽}}_A}),$

and

$\psi$$:{\mathrm{𝖿𝗂𝖻}}_{\alpha }({\mathrm{𝗂𝖽}}_A)\to {\prod }_{(x:A)}P(x),$

$\psi (g,p)$$:\equiv \lambda x.p_{*}\left({\mathrm{𝗉𝗋}}_2(g(x))\right).$

Then $\psi (\phi (f))=\lambda 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 $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(f,g):(f=g)\to (f\sim g)$ whichconverts equality of functions to homotopy. In the proof that follows, the univalenceaxiom is not used.

Theorem 4.9.5.

Weak function extensionality implies the function extensionality Axiom 2.9.3 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmpreaxiom1).

Proof.

We want to show that

$$\prod _{(A:𝒰)}\prod _{(P:A\to 𝒰)}\prod _{(f,g:{\prod }_{(x:A)}P(x))}\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(f,g)).$$

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

$$\left(\sum _{g:{\prod }_{(x:A)}P(x)}(f=g)\right)\to \sum _{g:{\prod }_{(x:A)}P(x)}(f\sim g)$$

induced by $\lambda (g:{\prod }_{(x:A)}P(x)).\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(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:

$$\sum _{(g:{\prod }_{(x:A)}P(x))}\prod _{(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 equivalent to

$$\prod _{(x:A)}\sum _{(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 product of contractible types, which is contractible by the weak function extensionality principle; hence (4.9.6) is also contractible.∎