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 $\mathrm{\Sigma }\mathit{}\mathrm{(}A\mathrm{)}$ is a set,and $A$ is equivalent to $\mathrm{N}{\mathrm{=}}_{\mathrm{\Sigma }\mathit{}\mathrm{(}A\mathrm{)}}\mathrm{S}$.

Proof.

To show that $\mathrm{\Sigma }(A)$ is a set, we define afamily $P:\mathrm{\Sigma }(A)\to \mathrm{\Sigma }(A)\to 𝒰$ with theproperty that $P(x,y)$ is a mere proposition for each $x,y:\mathrm{\Sigma }(A)$,and which is equivalent to its identity type ${\mathrm{𝖨𝖽}}_{\mathrm{\Sigma }(A)}$.We make the following definitions:

$P(𝖭,𝖭)$$:\equiv \mathrm{𝟏}$$P(𝖲,𝖭)$$:\equiv A$

$P(𝖭,𝖲)$$:\equiv A$$P(𝖲,𝖲)$$:\equiv \mathrm{𝟏}.$

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

$$P(𝖭,𝖭)=P(𝖭,𝖲)=P(𝖲,𝖭)=P(𝖲,𝖲).$$

But since $A$ is inhabited by $a$, it is equivalent to $\mathrm{𝟏}$, so we have

$$P(𝖭,𝖭)\simeq P(𝖭,𝖲)\simeq P(𝖲,𝖭)\simeq P(𝖲,𝖲).$$

The univalence axiom turns these into the desired equalities. Also, $P(x,y)$ is a mereproposition for all $x,y:\mathrm{\Sigma }(A)$, which is proved by induction on $x$ and $y$, andusing the fact that being a mere proposition is a mere proposition.

Note that $P$ is a reflexive relation.Therefore we may apply thm:h-set-refrel-in-paths-sets, so it suffices toconstruct $\tau :{\prod }_{(x,y:\mathrm{\Sigma }(A))}P(x,y)\to (x=y)$. We do this by a double induction.When $x$ is $𝖭$, we define $\tau (𝖭)$ by

$$\tau (𝖭,𝖭,u):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}\tau (𝖭,𝖲,a):\equiv \mathrm{𝗆𝖾𝗋𝗂𝖽}(a).$$

If $A$ is inhabited by $a$ then $\mathrm{𝗆𝖾𝗋𝗂𝖽}(a):𝖭=𝖲$ so we also need$\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a)}_{*}\left(\tau (𝖭,𝖭)\right)=\tau (𝖭,𝖲).$This we get by function extensionality using the fact that, for all $x:A$,

$$\begin{array}{c}\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a)}_{*}\left(\tau (𝖭,𝖭,x)\right)=\tau (𝖭,𝖭,x)\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a)}^{-1}\equiv \hfill \\ \hfill {\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)=\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)=\mathrm{𝗆𝖾𝗋𝗂𝖽}(x)\equiv \tau (𝖭,𝖲,x).\end{array}$$

In a symmetric fashion we may define $\tau (𝖲)$ by

$$\tau (𝖲,𝖭,a):\equiv \mathrm{𝗆𝖾𝗋𝗂𝖽}{(a)}^{-1}\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}\tau (𝖲,𝖲,u):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{𝖲}.$$

To complete the construction of $\tau$, we need to check $\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a)}_{*}\left(\tau (𝖭)\right)=\tau (𝖲)$,given any $a:A$. The verification proceeds much along the same lines by induction on thesecond argument of $\tau$.

Thus, by thm:h-set-refrel-in-paths-sets we have that $\mathrm{\Sigma }(A)$ is a set and that $P(x,y)\simeq (x=y)$ for all $x,y:\mathrm{\Sigma }(A)$.Taking $x:\equiv 𝖭$ and $y:\equiv 𝖲$ yields $A\simeq (𝖭{=}_{\mathrm{\Sigma }(A)}𝖲)$ as desired.∎

Theorem 10.1.2 (Diaconescu).

The axiom of choice implies the law of excluded middle.

Proof.

We use the equivalent form of choice given in thm:ac-epis-split.Consider a mere proposition $A$.The function $f:\mathrm{𝟐}\to \mathrm{\Sigma }(A)$ defined by$f(0_{\mathrm{𝟐}}):\equiv 𝖭$ and $f(1_{\mathrm{𝟐}}):\equiv 𝖲$is surjective.Indeed, we have$(0_{\mathrm{𝟐}},{\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}):{\mathrm{𝖿𝗂𝖻}}_f(𝖭)$and $(1_{\mathrm{𝟐}},{\mathrm{𝗋𝖾𝖿𝗅}}_{𝖲}):{\mathrm{𝖿𝗂𝖻}}_f(𝖲)$.Since $\parallel {\mathrm{𝖿𝗂𝖻}}_f(x)\parallel$ is a mere proposition, by induction the claimed surjectivity follows.

By prop:trunc_of_prop_is_set the suspension $\mathrm{\Sigma }(A)$is a set, so by the axiom of choice there merely exists asection $g:\mathrm{\Sigma }(A)\to \mathrm{𝟐}$ of $f$.As equality on $\mathrm{𝟐}$ is decidable we get

$$(g(f(0_{\mathrm{𝟐}}))=g(f(1_{\mathrm{𝟐}})))+\mathrm{\neg }(g(f(0_{\mathrm{𝟐}}))=g(f(1_{\mathrm{𝟐}}))),$$

and, since $g$ is a section of $f$, hence injective,

$$(f(0_{\mathrm{𝟐}})=f(1_{\mathrm{𝟐}}))+\mathrm{\neg }(f(0_{\mathrm{𝟐}})=f(1_{\mathrm{𝟐}})).$$

Finally, since $(f(0_{\mathrm{𝟐}})=f(1_{\mathrm{𝟐}}))=(𝖭=𝖲)=A$ by prop:trunc_of_prop_is_set, we have $A+\mathrm{\neg }A$.∎

Theorem 10.1.3.

If the axiom of choice holds then the category $\mathrm{S}\mathit{}e\mathit{}t$ is a well-pointed boolean elementary topos with choice.

Proof.

Since $\mathrm{𝖠𝖢}$ implies $\mathrm{𝖫𝖤𝖬}$, we have a boolean elementary topos with choice by thm:settopos and the remark following it. We leave the proof of well-pointedness asan exercise for the reader (ex:well-pointed).∎

Remark 10.1.4.

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