# Obtaining the Axiom of Choice through a modality in HTT

In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity it is refutable.

But, one can work inside the double negation modality to obtain (a form of) the law of excluded middle.

The question now is, can the same be done to obtain the axiom of choice? To be exact, is there a modality M such that the type $$\Pi x : A. \|\Sigma y : B. R(x, y)\| \to M \|\Sigma f : A \to B. \Pi x : A. R (x, f(x))\|$$ is inhabited?

• This is a good question, for which I don't know the answer. But let me share my intuition that no such modality exists: As you say, by exploiting the double negation modality, we can eliminate the law of excluded middle from proofs (at the cost of also modifying the claimed statements). But no similarly general technique for eliminating the axiom of choice is known. (Of course there are several specialized techniques, for instance employing generic models which live in classifying toposes or employing the dynamical methods in algebra, but these are not based on a modality.) Sep 26 '19 at 15:11
• Waht is $\|{-}\|$? Shouldn't the modal AC read $(\Pi (x : A) . M(\Sigma (y : B) . R(x,y))) \to M (\Sigma (f : A \to B) . \Pi (x : A) . R(x, f(x)))$? And while you're at it, what does "modality" mean for you? Like the ones in the HoTT book? Sep 26 '19 at 19:26
• @AndrejBauer $\|-\|$ is propositional truncation but I think the other point, defining modality, as also Mike Shulman points out in his answer below, is more challenging. Initially I meant the terms in HoTT book, yes. I posed this question from an undergraduate view, and as of now, I think the question is ill-posed. There is definitly a lot to unpack for me already. I believe a better question for now (homework for me) would be "why, exactly, is the double negation modality so useful". The reason I asked was to get a sense how to translate a proof using AC into HoTT language. Sep 26 '19 at 21:53

There is a trivial sense in which the answer is yes. For any proposition $$P$$, there's a modality $$O_P$$ called the open modality determined by $$P$$, defined by $$O_P(X) \equiv (P\to X)$$. If you take $$P$$ to be the statement of the axiom of choice (relative to some universe), then for $$M=O_P$$ the type you showed is inhabited, since you get to use the axiom of choice in proving the conclusion.
However, this is not as useful as the double-negation modality for LEM. To see why, notice that there is an even more trivial sense in which the answer is yes, namely when $$M$$ is the trivial modality, $$M_{\rm triv}(X) \equiv \mathbf{1}$$. Obviously that's not very interesting. The point is that $$M_{\rm triv} = O_{\mathbf{0}}$$, and if we don't know whether $$P=\mathbf{0}$$ (such as when $$P=\rm AC$$), then we don't know whether $$O_P = M_{\rm triv}$$. (And in fact, in models where $$\rm AC$$ is refutable, we do have $$O_{\rm AC} = M_{\rm triv}$$.) The same argument applies to $$P=\rm LEM$$, of course; but $$O_{\rm LEM}$$ is not the same as double-negation, and we can prove that double-negation is always nontrivial (e.g. $$\neg\neg \mathbf{0} = \mathbf{0}$$). So this "answer" is not really telling us anything.
Relaxing lexness is going to be trickier, since even the classical simplicial model has lots of nontrivial proper non-lex modalities, like the $$n$$-truncations for all $$n$$. I don't know whether there's any classification of all such modalities, or any other way to verify that none of them make AC true.
• One other thing I meant to mention but forgot: in addition to the actual double-negation modality $\neg\neg$, at least if we have propositional resizing we can form the double-negation-sheafification modality by localizing at all the double-negation-closed propositions. The latter is lex and hence yields an entire "world" in which LEM holds, whereas for $\neg\neg$ itself the only modal types are the double-negation-closed propositions themselves. Sep 27 '19 at 19:19