3.8 The axiom of choice
and moreover that
is a set,
is a set for all , and
is a mere proposition for all and .
The axiom of choice asserts that under these assumptions,
Of course, this is a direct translation of (3.2.1) (http://planetmath.org/32propositionsastypes#S0.E1) where we read “there exists such that ” as , 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 there exists some such that , 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 , 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.
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 Conversely, (3.8.2) is equivalent to the instance of (3.8.1) where and . 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. ∎
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: is not generally equivalent to . 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 and in (3.8.1), or 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 -truncations to be considered in http://planetmath.org/node/87580Chapter 7, obtaining a spectrum of axioms interpolating between (3.8.1), which we call simply (or 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 be a set.
There exists a type and a family such that each is a set, but such that (3.8.2) is false.
Define , and let . Then by the identification of paths in -types, the fact that is a mere proposition, and univalence, for any we have . In particular, , so as in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6), is not a set.
On the other hand, if , then is a set; this follows by induction on truncation for and the fact that is a set. Since is a set whenever and are, it follows that is a set for any , i.e. is a 1-type. In particular, if we define by , then each is a set.
Now by definition, for any we have , and hence . Thus, we have . If (3.8.2) held for this and , then we would also have . Since we are trying to derive a contradiction (), which is a mere proposition, we may assume , i.e. that . But this implies is a mere proposition, and hence a set, which is a contradiction. ∎
|Title||3.8 The axiom of choice|