3.8 The axiom of choice

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

A:X→𝒰  and  P:∏x:XA⁒(x)→𝒰,

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 𝖠𝖒 asserts that under these assumptionsPlanetmathPlanetmath,

(∏x:Xβˆ₯βˆ‘a:A⁒(x)P⁒(x,a)βˆ₯)β†’βˆ₯βˆ‘(g:∏(x:X)A(x))∏(x:X)P⁒(x,g⁒(x))βˆ₯. (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 βˆ₯βˆ‘(x:A)B⁒(x)βˆ₯, so we could have written the statement in the familiar logical notation as


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 equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the statement that for any set X and any Y:Xβ†’U such that each Y⁒(x) is a set, we have

(∏x:Xβˆ₯Y⁒(x)βˆ₯)β†’βˆ₯∏x:XY⁒(x)βˆ₯. (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.”


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


Thus,Β (3.8.1) is equivalent to the instance ofΒ (3.8.2) where Y(x):β‰‘βˆ‘(a:A(x))P(x,a). Conversely,Β (3.8.2) is equivalent to the instance ofΒ (3.8.1) where A(x):≑Y(x) and P(x,a):β‰‘πŸ. 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 𝖫𝖀𝖬, the equivalent formsΒ (3.8.1) andΒ (3.8.2) are not a consequence of our basic type theoryPlanetmathPlanetmath, 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


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: βˆ₯∏(x:A)P⁒(x)βˆ₯ is not generally equivalent to ∏(x:A)βˆ₯P(x)βˆ₯. 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 restrictionPlanetmathPlanetmathPlanetmath 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 𝖠𝖒n interpolating betweenΒ (3.8.1), which we call simply 𝖠𝖒 (or 𝖠𝖒-1 for emphasis), and Theorem 0.3 (http://planetmath.org/215universalproperties#S0.Thmthm3), which we shall call π– π–’βˆž. 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β†’U such that each Y⁒(x) is a set, but such thatΒ (3.8.2) is false.


Define X:β‰‘βˆ‘(A:𝒰)βˆ₯𝟐=Aβˆ₯, and let x0:≑(𝟐,|π—‹π–Ύπ–Ώπ—…πŸ|):X. Then by the identification of paths in Ξ£-types, the fact that βˆ₯A=𝟐βˆ₯ is a mere proposition, and univalence, for any (A,p),(B,q):X we have ((A,p)=X(B,q))≃(A≃B). In particular, (x0=Xx0)≃(πŸβ‰ƒπŸ), 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 inductionMathworldPlanetmath on truncation for p:βˆ₯𝟐=Aβˆ₯ and the fact that 𝟐 is a set. Since A≃B is a set whenever A and B are, it follows that x1=Xx2 is a set for any x1,x2:X, i.e.Β X is a 1-type. In particular, if we define Y:X→𝒰 by Y(x):≑(x0=x), then each Y⁒(x) is a set.

Now by definition, for any (A,p):X we have βˆ₯𝟐=Aβˆ₯, and hence βˆ₯x0=(A,p)βˆ₯. Thus, we have ∏(x:X)βˆ₯Y(x)βˆ₯. IfΒ (3.8.2) held for this X and Y, then we would also have βˆ₯∏(x:X)Y⁒(x)βˆ₯. Since we are trying to derive a contradictionMathworldPlanetmathPlanetmath (𝟎), which is a mere proposition, we may assume ∏(x:X)Y⁒(x), i.e.Β that ∏(x:X)(x0=x). But this implies X is a mere proposition, and hence a set, which is a contradiction. ∎

Title 3.8 The axiom of choice