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. ∎

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 \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