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)).

Let $\mathcal{U}$ be a universe; 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

$\Bigl{(}\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathsf{isContr}(% P(x))\Bigr{)}\to\mathsf{isContr}\Bigl{(}\mathchoice{\prod_{x:A}\,}{\mathchoice% {{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x)\Bigr{)}$

for any family $P:A\to\mathcal{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 $\mathcal{U}$ is univalent, for any $A,B,X:\mathcal{U}$ and any $e:A\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=\mathsf{idtoeqv}(p)$ for some $p:A=B$ . Then by path induction, we may assume $p$ is $\mathsf{refl}_{A}$ , so that $e=\mathsf{id}_{A}$ . But in this case, post-composition with $e$ is the identity, hence an equivalence. ∎

Corollary 4.9.3.

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

$\alpha:\Bigl{(}A\to\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)\Bigr{)}\simeq(A\to A).$

Proof.

By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), for $\mathsf{pr}_{1}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}% }{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(X)\to A$ and $x : A$ we have an equivalence

${\mathsf{fib}}_{\mathsf{pr}_{1}}(x)\simeq P(x).$

Therefore $\mathsf{pr}_{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 $\mathsf{id}_{A}$ is contractible. Therefore, we can show that univalence implies weak function extensionality by showing that the dependent function type $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$ is a retract of ${\mathsf{fib}}_{\alpha}(\mathsf{id}_{A})$ .

Theorem 4.9.4.

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

Proof.

Define the functions

	$\displaystyle\varphi$	$\displaystyle:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:% A)}}{\prod_{(x:A)}}P(x)\to{\mathsf{fib}}_{\alpha}(\mathsf{id}_{A}),$
	$\displaystyle\varphi(f)$	$\displaystyle:\!\!\equiv({\lambda}x.\,(x,f(x)),\mathsf{refl}_{\mathsf{id}_{A}}),$
and
	$\displaystyle\psi$	$\displaystyle:{\mathsf{fib}}_{\alpha}(\mathsf{id}_{A})\to\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}P(x),$
	$\displaystyle\psi(g,p)$	$\displaystyle:\!\!\equiv{\lambda}x.\,{p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(% g(x))}\right)\mathclose{}.$

Then $\psi(\varphi(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 $\mathsf{happly}(f,g):(f=g)\to(f\sim 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).

Proof.

We want to show that

$\mathchoice{\prod_{(A:\mathcal{U})}\,}{\mathchoice{{\textstyle\prod_{(A:% \mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}\mathchoice{\prod_{(P:A\to\mathcal{U})% }\,}{\mathchoice{{\textstyle\prod_{(P:A\to\mathcal{U})}}}{\prod_{(P:A\to% \mathcal{U})}}{\prod_{(P:A\to\mathcal{U})}}{\prod_{(P:A\to\mathcal{U})}}}{% \mathchoice{{\textstyle\prod_{(P:A\to\mathcal{U})}}}{\prod_{(P:A\to\mathcal{U}% )}}{\prod_{(P:A\to\mathcal{U})}}{\prod_{(P:A\to\mathcal{U})}}}{\mathchoice{{% \textstyle\prod_{(P:A\to\mathcal{U})}}}{\prod_{(P:A\to\mathcal{U})}}{\prod_{(P% :A\to\mathcal{U})}}{\prod_{(P:A\to\mathcal{U})}}}\mathchoice{\prod_{(f,g:% \mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}\,}{\mathchoice{{% \textstyle\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_% {(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x))}}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{% \prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x% :A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\prod_{(f,g:\mathchoice{\prod_{x% :A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\prod_{(f,g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}}\mathsf{isequiv}(\mathsf{happly}(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

$\Bigl{(}\mathchoice{\sum_{g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x)}\,}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice% {{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A% }\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A% }\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}(f=g)\Bigr{)}\to\mathchoice{\sum_{g:\mathchoice{\prod_{% x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x)}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{% \prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x% :A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}% \,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod% _{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}% }{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_% {(x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{% \prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x% :A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}% \,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod% _{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}% }{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_% {(x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A% }\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}(f\sim g)$

induced by ${\lambda}(g\,{:}\,\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:% A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)).% \,\mathsf{happly}(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:

$\mathchoice{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{% (x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}% \,}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A% }\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:A% }\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}P(x))}}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{% {\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}{\sum_{(g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}P(x))}}}\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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

$\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathchoice{\sum_{(u:P(x))% }\,}{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}% }{\sum_{(u:P(x))}}}{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{% \sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{% \sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\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. ∎

Title	4.9 Univalence implies function extensionality
\metatable