10.1.5 The axiom of choice implies excluded middle
We begin with the following lemma.
If is a mere proposition then its suspension is a set, and is equivalent to .
But since is inhabited by , it is equivalent to , so we have
The univalence axiom turns these into the desired equalities. Also, is a mere proposition for all , which is proved by induction on and , and using the fact that being a mere proposition is a mere proposition.
If is inhabited by then so we also need This we get by function extensionality using the fact that, for all ,
In a symmetric fashion we may define by
Thus, by \autorefthm:h-set-refrel-in-paths-sets we have that is a set and that for all . Taking and yields as desired. ∎
We use the equivalent form of choice given in \autorefthm:ac-epis-split. Consider a mere proposition . The function defined by and is surjective. Indeed, we have and . Since is a mere proposition, by induction the claimed surjectivity follows.
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). ∎
|Title||10.1.5 The axiom of choice implies excluded middle|