# 3.8 The axiom of choice

We can now properly formulate the axiom of choice in homotopy type theory. Assume a type $X$ and type families

 $A:X\to\mathcal{U}\qquad\text{and}\qquad P:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x)\to\mathcal{U},$

and moreover that

• $X$ is a set,

• $A(x)$ is a set for all $x:X$, and

• $P(x,a)$ is a mere proposition for all $x:X$ and $a:A(x)$.

The axiom of choice $\mathsf{AC}$ asserts that under these assumptions,

 $\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\Bigl{\|}% \mathchoice{\sum_{a:A(x)}\,}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a% :A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(% x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{% \textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}% }P(x,a)\Bigr{\|}\Bigr{)}\to\Bigl{\|}\mathchoice{\sum_{(g:\mathchoice{\prod_{x:% X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{% \prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x% :X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(% x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}% \,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod% _{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}% }{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_% {(x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{% \prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x% :X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(% x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}% \,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod% _{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}% }{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_% {(x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X% }\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}P(x,g(x))\Bigr{\|}.$ (3.8.1)

Of course, this is a direct translation of (3.2.1) (http://planetmath.org/32propositionsastypes#S0.E1) where we read “there exists $x:A$ such that $B(x)$” as $\mathopen{}\left\|\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)}}}B(x)\right\|\mathclose{}$, so we could have written the statement in the familiar logical notation as

 $\textstyle\Big{(}\forall(x:X).\,\exists(a:A(x)).\,P(x,a)\Big{)}\Rightarrow\Big% {(}\exists(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}% {\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(% x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x)).\,\forall(x% :X).\,P(x,g(x))\Big{)}.$

In particular, note that the propositional truncation appears twice. The truncation in the domain means we assume that for every $x$ there exists some $a:A(x)$ such that $P(x,a)$, but that these values are not chosen or specified in any known way. The truncation in the codomain means we conclude that there exists some function $g$, but this function is not determined or specified in any known way.

In fact, because of Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3), this axiom can also be expressed in a simpler form.

###### Lemma 3.8.2.

The axiom of choice (3.8.1) is equivalent to the statement that for any set $X$ and any $Y:X\to\mathcal{U}$ such that each $Y(x)$ is a set, we have

 $\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\Bigl{\|}Y(x)% \Bigr{\|}\Bigr{)}\to\Bigl{\|}\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}Y(x)\Bigr{\|}.$ (3.8.2)

This corresponds to a well-known equivalent form of the classical axiom of choice, namely “the cartesian product of a family of nonempty sets is nonempty.”

###### Proof.

By Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3), the codomain of (3.8.1) is equivalent to

 $\Bigl{\|}\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\mathchoice{\sum_% {(a:A(x))}\,}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{% (a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a% :A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(% x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}P(x,a)\Bigr{\|}.$

Thus, (3.8.1) is equivalent to the instance of (3.8.2) where $Y(x):\!\!\equiv\mathchoice{\sum_{a:A(x)}\,}{\mathchoice{{\textstyle\sum_{(a:A(% x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{% \textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}% }{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}{% \sum_{(a:A(x))}}}P(x,a).$ Conversely, (3.8.2) is equivalent to the instance of (3.8.1) where $A(x):\!\!\equiv Y(x)$ and $P(x,a):\!\!\equiv\mathbf{1}$. Thus, the two are logically equivalent. Since both are mere propositions, by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2) they are equivalent types. ∎

As with $\mathsf{LEM}$, the equivalent forms (3.8.1) and (3.8.2) are not a consequence of our basic type theory, but they may consistently be assumed as axioms.

###### Remark 3.8.4.

It is easy to show that the right side of (3.8.2) always implies the left. Since both are mere propositions, by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2) the axiom of choice is also equivalent to asking for an equivalence

 $\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\Bigl{\|}Y(x)% \Bigr{\|}\Bigr{)}\simeq\Bigl{\|}\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}Y(x)\Bigr{\|}$

This illustrates a common pitfall: although dependent function types preserve mere propositions (Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2)), they do not commute with truncation: $\mathopen{}\left\|\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)% \right\|\mathclose{}$ is not generally 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)}}}\mathopen{}\left\|P(x)\right\|% \mathclose{}$. The axiom of choice, if we assume it, says that this is true for sets; as we will see below, it fails in general.

The restriction in the axiom of choice to types that are sets can be relaxed to a certain extent. For instance, we may allow $A$ and $P$ in (3.8.1), or $Y$ in (3.8.2), to be arbitrary type families; this results in a seemingly stronger statement that is equally consistent. We may also replace the propositional truncation by the more general $n$-truncations to be considered in http://planetmath.org/node/87580Chapter 7, obtaining a spectrum of axioms $\mathsf{AC}_{n}$ interpolating between (3.8.1), which we call simply $\mathsf{AC}$ (or $\mathsf{AC}_{-1}$ for emphasis), and Theorem 0.3 (http://planetmath.org/215universalproperties#S0.Thmthm3), which we shall call $\mathsf{AC}_{\infty}$. See also http://planetmath.org/node/87816Exercise 7.8,http://planetmath.org/node/87863Exercise 7.10. However, observe that we cannot relax the requirement that $X$ be a set.

###### Lemma 3.8.5.

There exists a type $X$ and a family $Y:X\to\mathcal{U}$ such that each $Y(x)$ is a set, but such that (3.8.2) is false.

###### Proof.

Define $X:\!\!\equiv\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\sum_{(% A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:% \mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{% \textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U% })}}{\sum_{(A:\mathcal{U})}}}\mathopen{}\left\|\mathbf{2}=A\right\|\mathclose{}$, and let $x_{0}:\!\!\equiv(\mathbf{2},\mathopen{}\left|\mathsf{refl}_{\mathbf{2}}\right|% \mathclose{}):X$. Then by the identification of paths in $\Sigma$-types, the fact that $\mathopen{}\left\|A=\mathbf{2}\right\|\mathclose{}$ is a mere proposition, and univalence, for any $(A,p),(B,q):X$ we have $((A,p)=_{X}(B,q))\simeq(A\simeq B)$. In particular, $(x_{0}=_{X}x_{0})\simeq(\mathbf{2}\simeq\mathbf{2})$, so as in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6), $X$ is not a set.

On the other hand, if $(A,p):X$, then $A$ is a set; this follows by induction on truncation for $p:\mathopen{}\left\|\mathbf{2}=A\right\|\mathclose{}$ and the fact that $\mathbf{2}$ is a set. Since $A\simeq B$ is a set whenever $A$ and $B$ are, it follows that $x_{1}=_{X}x_{2}$ is a set for any $x_{1},x_{2}:X$, i.e. $X$ is a 1-type. In particular, if we define $Y:X\to\mathcal{U}$ by $Y(x):\!\!\equiv(x_{0}=x)$, then each $Y(x)$ is a set.

Now by definition, for any $(A,p):X$ we have $\mathopen{}\left\|\mathbf{2}=A\right\|\mathclose{}$, and hence $\mathopen{}\left\|x_{0}=(A,p)\right\|\mathclose{}$. Thus, we have $\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\mathopen{}\left\|Y(x)\right\|% \mathclose{}$. If (3.8.2) held for this $X$ and $Y$, then we would also have $\mathopen{}\left\|\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:% X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)% \right\|\mathclose{}$. Since we are trying to derive a contradiction ($\mathbf{0}$), which is a mere proposition, we may assume $\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)$, i.e. that $\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(x_{0}=x)$. But this implies $X$ is a mere proposition, and hence a set, which is a contradiction. ∎

Title 3.8 The axiom of choice
\metatable