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

###### Proof.

To show that $\Sigma(A)$ is a set, we define a family $P:\Sigma(A)\to\Sigma(A)\to\mathcal{U}$ with the property that $P(x,y)$ is a mere proposition for each $x,y:\Sigma(A)$, and which is equivalent to its identity type $\mathsf{Id}_{\Sigma(A)}$. We make the following definitions:

 $\displaystyle P(\mathsf{N},\mathsf{N})$ $\displaystyle:\!\!\equiv\mathbf{1}$ $\displaystyle P(\mathsf{S},\mathsf{N})$ $\displaystyle:\!\!\equiv A$ $\displaystyle P(\mathsf{N},\mathsf{S})$ $\displaystyle:\!\!\equiv A$ $\displaystyle P(\mathsf{S},\mathsf{S})$ $\displaystyle:\!\!\equiv\mathbf{1}.$

We have to check that the definition preserves paths. Given any $a:A$, there is a meridian $\mathsf{merid}(a):\mathsf{N}=\mathsf{S}$, so we should also have

 $P(\mathsf{N},\mathsf{N})=P(\mathsf{N},\mathsf{S})=P(\mathsf{S},\mathsf{N})=P(% \mathsf{S},\mathsf{S}).$

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

 $P(\mathsf{N},\mathsf{N})\simeq P(\mathsf{N},\mathsf{S})\simeq P(\mathsf{S},% \mathsf{N})\simeq P(\mathsf{S},\mathsf{S}).$

The univalence axiom turns these into the desired equalities. Also, $P(x,y)$ is a mere proposition for all $x,y:\Sigma(A)$, which is proved by induction 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 $\tau:\mathchoice{\prod_{x,y:\Sigma(A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:% \Sigma(A))}}}{\prod_{(x,y:\Sigma(A))}}{\prod_{(x,y:\Sigma(A))}}{\prod_{(x,y:% \Sigma(A))}}}{\mathchoice{{\textstyle\prod_{(x,y:\Sigma(A))}}}{\prod_{(x,y:% \Sigma(A))}}{\prod_{(x,y:\Sigma(A))}}{\prod_{(x,y:\Sigma(A))}}}{\mathchoice{{% \textstyle\prod_{(x,y:\Sigma(A))}}}{\prod_{(x,y:\Sigma(A))}}{\prod_{(x,y:% \Sigma(A))}}{\prod_{(x,y:\Sigma(A))}}}P(x,y)\to(x=y)$. We do this by a double induction. When $x$ is $\mathsf{N}$, we define $\tau(\mathsf{N})$ by

 $\tau(\mathsf{N},\mathsf{N},u):\!\!\equiv\mathsf{refl}_{\mathsf{N}}\qquad\text{% and}\qquad\tau(\mathsf{N},\mathsf{S},a):\!\!\equiv\mathsf{merid}(a).$

If $A$ is inhabited by $a$ then $\mathsf{merid}(a):\mathsf{N}=\mathsf{S}$ so we also need ${\mathsf{merid}(a)}_{*}\mathopen{}\left({\tau(\mathsf{N},\mathsf{N})}\right)% \mathclose{}=\tau(\mathsf{N},\mathsf{S}).$ This we get by function extensionality using the fact that, for all $x:A$,

 $\displaystyle{\mathsf{merid}(a)}_{*}\mathopen{}\left({\tau(\mathsf{N},\mathsf{% N},x)}\right)\mathclose{}=\tau(\mathsf{N},\mathsf{N},x)\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{% \mathsf{merid}(a)}^{-1}}\equiv\\ \displaystyle\mathsf{refl}_{\mathsf{N}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{merid}(a)=\mathsf{merid}% (a)=\mathsf{merid}(x)\equiv\tau(\mathsf{N},\mathsf{S},x).$

In a symmetric fashion we may define $\tau(\mathsf{S})$ by

 $\tau(\mathsf{S},\mathsf{N},a):\!\!\equiv\mathord{{\mathsf{merid}(a)}^{-1}}% \qquad\text{and}\qquad\tau(\mathsf{S},\mathsf{S},u):\!\!\equiv\mathsf{refl}_{% \mathsf{S}}.$

To complete the construction of $\tau$, we need to check ${\mathsf{merid}(a)}_{*}\mathopen{}\left({\tau(\mathsf{N})}\right)\mathclose{}=% \tau(\mathsf{S})$, given any $a:A$. The verification proceeds much along the same lines by induction on the second argument of $\tau$.

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

###### Proof.

We use the equivalent form of choice given in \autorefthm:ac-epis-split. Consider a mere proposition $A$. The function $f:\mathbf{2}\to\Sigma(A)$ defined by $f({0_{\mathbf{2}}}):\!\!\equiv\mathsf{N}$ and $f({1_{\mathbf{2}}}):\!\!\equiv\mathsf{S}$ is surjective. Indeed, we have ${\mathopen{}({0_{\mathbf{2}}},\mathsf{refl}_{\mathsf{N}})\mathclose{}}:{% \mathsf{fib}}_{f}(\mathsf{N})$ and ${\mathopen{}({1_{\mathbf{2}}},\mathsf{refl}_{\mathsf{S}})\mathclose{}}:{% \mathsf{fib}}_{f}(\mathsf{S})$. Since $\bigl{\|}{\mathsf{fib}}_{f}(x)\bigr{\|}$ is a mere proposition, by induction the claimed surjectivity follows.

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

 $(g(f({0_{\mathbf{2}}}))=g(f({1_{\mathbf{2}}})))+\lnot(g(f({0_{\mathbf{2}}}))=g% (f({1_{\mathbf{2}}}))),$

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

 $(f({0_{\mathbf{2}}})=f({1_{\mathbf{2}}}))+\lnot(f({0_{\mathbf{2}}})=f({1_{% \mathbf{2}}})).$

Finally, since $(f({0_{\mathbf{2}}})=f({1_{\mathbf{2}}}))=(\mathsf{N}=\mathsf{S})=A$ by \autorefprop:trunc_of_prop_is_set, we have $A+\neg A$. ∎

###### Theorem 10.1.3.

If the axiom of choice holds then the category $\mathcal{S}et$ is a well-pointed boolean elementary topos with choice.

###### Proof.

Since $\mathsf{AC}$ implies $\mathsf{LEM}$, 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 theorem 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 \metatable