10.1.5 The axiom of choice implies excluded middle

We begin with the following lemma.

Lemma 10.1.1.

If A is a mere proposition then its suspension Σ(A) is a set, and A is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to N=Σ(A)S.


To show that Σ(A) is a set, we define a family P:Σ(A)Σ(A)𝒰 with the property that P(x,y) is a mere proposition for each x,y:Σ(A), and which is equivalent to its identity type 𝖨𝖽Σ(A). We make the following definitions:

P(𝖭,𝖭) :𝟏 P(𝖲,𝖭) :A
P(𝖭,𝖲) :A P(𝖲,𝖲) :𝟏.

We have to check that the definition preserves paths. Given any a:A, there is a meridian 𝗆𝖾𝗋𝗂𝖽(a):𝖭=𝖲, so we should also have


But since A is inhabited by a, it is equivalent to 𝟏, so we have


The univalence axiom turns these into the desired equalities. Also, P(x,y) is a mere proposition for all x,y:Σ(A), which is proved by inductionMathworldPlanetmath on x and y, and using the fact that being a mere proposition is a mere proposition.

Note that P is a reflexive relation. Therefore we may apply \autorefthm:h-set-refrel-in-paths-sets, so it suffices to construct τ:(x,y:Σ(A))P(x,y)(x=y). We do this by a double induction. When x is 𝖭, we define τ(𝖭) by

τ(𝖭,𝖭,u):𝗋𝖾𝖿𝗅𝖭  and  τ(𝖭,𝖲,a):𝗆𝖾𝗋𝗂𝖽(a).

If A is inhabited by a then 𝗆𝖾𝗋𝗂𝖽(a):𝖭=𝖲 so we also need 𝗆𝖾𝗋𝗂𝖽(a)*(τ(𝖭,𝖭))=τ(𝖭,𝖲). This we get by function extensionality using the fact that, for all x:A,


In a symmetricMathworldPlanetmathPlanetmathPlanetmath fashion we may define τ(𝖲) by

τ(𝖲,𝖭,a):𝗆𝖾𝗋𝗂𝖽(a)-1  and  τ(𝖲,𝖲,u):𝗋𝖾𝖿𝗅𝖲.

To completePlanetmathPlanetmathPlanetmathPlanetmath the construction of τ, we need to check 𝗆𝖾𝗋𝗂𝖽(a)*(τ(𝖭))=τ(𝖲), given any a:A. The verification proceeds much along the same lines by induction on the second argument of τ.

Thus, by \autorefthm:h-set-refrel-in-paths-sets we have that Σ(A) is a set and that P(x,y)(x=y) for all x,y:Σ(A). Taking x:𝖭 and y:𝖲 yields A(𝖭=Σ(A)𝖲) as desired. ∎

Theorem 10.1.2 (Diaconescu).

We use the equivalent form of choice given in \autorefthm:ac-epis-split. Consider a mere proposition A. The function f:𝟐Σ(A) defined by f(0𝟐):𝖭 and f(1𝟐):𝖲 is surjectivePlanetmathPlanetmath. Indeed, we have (0𝟐,𝗋𝖾𝖿𝗅𝖭):𝖿𝗂𝖻f(𝖭) and (1𝟐,𝗋𝖾𝖿𝗅𝖲):𝖿𝗂𝖻f(𝖲). Since 𝖿𝗂𝖻f(x) is a mere proposition, by induction the claimed surjectivity follows.

By \autorefprop:trunc_of_prop_is_set the suspension Σ(A) is a set, so by the axiom of choice there merely exists a sectionMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath g:Σ(A)𝟐 of f. As equality on 𝟐 is decidable we get


and, since g is a section of f, hence injectivePlanetmathPlanetmath,


Finally, since (f(0𝟐)=f(1𝟐))=(𝖭=𝖲)=A by \autorefprop:trunc_of_prop_is_set, we have A+¬A. ∎

Theorem 10.1.3.

If the axiom of choice holds then the categoryMathworldPlanetmath Set is a well-pointed boolean elementary topos with choice.


Since 𝖠𝖢 implies 𝖫𝖤𝖬, we have a boolean elementary topos with choice by \autorefthm:settopos and the remark following it. We leave the proof of well-pointedness as an exercise for the reader (\autorefex:well-pointed). ∎

Remark 10.1.4.

The conditions on a category mentioned in the theoremMathworldPlanetmath are known as Lawvere’s axioms for the Elementary Theory of the Category of Sets [lawvere:etcs-long].

Title 10.1.5 The axiom of choice implies excluded middle