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 𝒰\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}P:\prod _{x:X}A(x)\to 𝒰,$$

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$\mathrm{𝖠𝖢}$ asserts that under these assumptions,

$$\left(\prod _{x:X}\parallel \sum _{a:A(x)}P(x,a)\parallel \right)\to \parallel \sum _{(g:{\prod }_{(x:X)}A(x))}\prod _{(x:X)}P(x,g(x))\parallel .$$(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 $\parallel {\sum }_{(x:A)}B(x)\parallel$, so we could have written the statement in the familiar logical notation as

$$(\forall (x:X).\exists (a:A(x)).P(x,a))\Rightarrow (\exists (g:{\prod }_{(x:X)}A(x)).\forall (x:X).P(x,g(x))).$$

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\mathrm{:}X\mathrm{\to }\mathrm{U}$ such that each $Y\mathit{}\mathrm{(}x\mathrm{)}$ is a set, we have

$$\left(\prod _{x:X}\parallel Y(x)\parallel \right)\to \parallel \prod _{x:X}Y(x)\parallel .$$(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

$$\parallel \prod _{(x:X)}\sum _{(a:A(x))}P(x,a)\parallel .$$

Thus, (3.8.1) is equivalent to the instance of (3.8.2) where $Y(x):\equiv {\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 \mathrm{𝟏}$.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 $\mathrm{𝖫𝖤𝖬}$, 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

$$\left(\prod _{x:X}\parallel Y(x)\parallel \right)\simeq \parallel \prod _{x:X}Y(x)\parallel$$

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: $\mathrm{\parallel }{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\parallel }$ is not generally equivalent to ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathrm{\parallel }P\mathrm{(}x\mathrm{)}\mathrm{\parallel }$.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 ${\mathrm{𝖠𝖢}}_n$ interpolating between (3.8.1), which we call simply $\mathrm{𝖠𝖢}$ (or ${\mathrm{𝖠𝖢}}_{-1}$ for emphasis), and Theorem 0.3 (http://planetmath.org/215universalproperties#S0.Thmthm3), which we shall call ${\mathrm{𝖠𝖢}}_{\mathrm{\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\mathrm{:}X\mathrm{\to }\mathrm{U}$ such that each $Y\mathit{}\mathrm{(}x\mathrm{)}$ is a set, but such that (3.8.2) is false.

Proof.

Define $X:\equiv {\sum }_{(A:𝒰)}\parallel \mathrm{𝟐}=A\parallel$, and let $x_0:\equiv (\mathrm{𝟐},\left|{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝟐}}\right|):X$.Then by the identification of paths in $\mathrm{\Sigma }$-types, the fact that $\parallel A=\mathrm{𝟐}\parallel$ 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 (\mathrm{𝟐}\simeq \mathrm{𝟐})$, 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:\parallel \mathrm{𝟐}=A\parallel$ and the fact that $\mathrm{𝟐}$ 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 𝒰$ by $Y(x):\equiv (x_0=x)$, then each $Y(x)$ is a set.

Now by definition, for any $(A,p):X$ we have $\parallel \mathrm{𝟐}=A\parallel$, and hence $\parallel x_0=(A,p)\parallel$.Thus, we have ${\prod }_{(x:X)}\parallel Y(x)\parallel$.If (3.8.2) held for this $X$ and $Y$, then we would also have $\parallel {\prod }_{(x:X)}Y(x)\parallel$.Since we are trying to derive a contradiction ($\mathrm{𝟎}$), which is a mere proposition, we may assume ${\prod }_{(x:X)}Y(x)$, i.e. that ${\prod }_{(x:X)}(x_0=x)$.But this implies $X$ is a mere proposition, and hence a set, which is a contradiction.∎