<p>There is a trivial sense in which the answer is yes.  For any proposition <span class="math-container">$P$</span>, there's a modality <span class="math-container">$O_P$</span> called the open modality determined by <span class="math-container">$P$</span>, defined by <span class="math-container">$O_P(X) \equiv (P\to X)$</span>.  If you take <span class="math-container">$P$</span> to be the statement of the axiom of choice (relative to some universe), then for <span class="math-container">$M=O_P$</span> the type you showed is inhabited, since you get to use the axiom of choice in proving the conclusion.</p>

<p>However, this is not as useful as the double-negation modality for LEM.  To see why, notice that there is an even <em>more</em> trivial sense in which the answer is yes, namely when <span class="math-container">$M$</span> is the trivial modality, <span class="math-container">$M_{\rm triv}(X) \equiv \mathbf{1}$</span>.  Obviously that's not very interesting.  The point is that <span class="math-container">$M_{\rm triv} = O_{\mathbf{0}}$</span>, and  if we don't know whether <span class="math-container">$P=\mathbf{0}$</span> (such as when <span class="math-container">$P=\rm AC$</span>), then we don't know whether <span class="math-container">$O_P = M_{\rm triv}$</span>.  (And in fact, in models where <span class="math-container">$\rm AC$</span> is refutable, we do have <span class="math-container">$O_{\rm AC} = M_{\rm triv}$</span>.)  The same argument applies to <span class="math-container">$P=\rm LEM$</span>, of course; but <span class="math-container">$O_{\rm LEM}$</span> is not the same as double-negation, and we can prove that double-negation is always nontrivial (e.g. <span class="math-container">$\neg\neg \mathbf{0} = \mathbf{0}$</span>).  So this "answer" is not really telling us anything.</p>

<p>As Ingo says, it seems unlikely that we can construct any provably-nontrivial modality with this property.  I don't know how to prove that we can't, but I think I can prove that no such <em>lex</em> modality can be constructed in the absence of univalence.  Take a model of ZF that doesn't satisfy AC.  Then its topos of sets is a model of MLTT with function extensionality, propositional extensionality, propositional truncation, and propositional resizing, in which lex modalities correspond to geometric subtoposes; but it has no proper nontrivial geometric subtoposes.</p>

<p>It should be possible to include Univalence as well, but I'm hazy on the necessary details.  Voevodsky's original simplicial model of HoTT has no nontrivial proper lex modalities, but its construction uses AC.  More recent cubical-type models of HoTT are constructive, but many of them do have nontrivial proper lex modalities.  Possibly the recent "equivariant" cartesian cubical model would work: it exists constructively, and classically is Quillen equivalent to the simplicial model and hence has no nontrivial proper lex modalities; but I'm not quite sure whether the latter equivalence uses AC or only LEM.</p>

<p>Relaxing lexness is going to be trickier, since even the classical simplicial model has lots of nontrivial proper non-lex modalities, like the <span class="math-container">$n$</span>-truncations for all <span class="math-container">$n$</span>.  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.</p>

CC BY-SA 4.0
2019-09-27T19:19:21.153Z
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.
Mike Shulman
CC BY-SA 4.0
2019-09-29T02:28:48.927Z
That's a lot of input for me. I will mark this as an answer even if I know that my question is not really precise enough to give a definite one. I appreciate the effort.
WorldSEnder
CC BY-SA 4.0
2019-09-26T17:22:04.313Z
2019-09-26T17:22:04.313Z
Mike Shulman
<p>In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity <a href="https://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/" rel="noreferrer">it is refutable</a>.</p>

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

<p>The question now is, can the same be done to obtain the axiom of choice? To be exact, is there a modality <code>M</code> such that the type <span class="math-container">$\Pi x : A. \|\Sigma y : B. R(x, y)\| \to M \|\Sigma f : A \to B. \Pi x : A. R (x, f(x))\|$</span> is inhabited?</p>

CC BY-SA 4.0
2019-09-26T15:11:29.613Z
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.)
Ingo Blechschmidt
CC BY-SA 4.0
2019-09-26T19:26:31.540Z
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?
Andrej Bauer
CC BY-SA 4.0
2019-09-26T21:53:55.667Z
@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.
WorldSEnder
<modal-logic><homotopy-type-theory>
Obtaining the Axiom of Choice through a modality in HTT
WorldSEnder
# Obtaining the Axiom of Choice through a modality in HTT

(Asked by: username_0 on 2019-09-25)

In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity [it is refutable](https://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/).

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?

**Tags:** modal-logic, homotopy-type-theory

> **Comments:**
> **username_1**: 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.)  
> **username_2**: 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?  
> **username_0**: @AndrejBauer $\|-\|$ is propositional truncation but I think the other point, defining modality, as also username_3 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.  

---

## 1 answers

### Answer by username_3 on 2019-09-26. Score: 5 | Accepted answer

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.

As Ingo says, it seems unlikely that we can construct any provably-nontrivial modality with this property. I don't know how to prove that we can't, but I think I can prove that no such *lex* modality can be constructed in the absence of univalence. Take a model of ZF that doesn't satisfy AC. Then its topos of sets is a model of MLTT with function extensionality, propositional extensionality, propositional truncation, and propositional resizing, in which lex modalities correspond to geometric subtoposes; but it has no proper nontrivial geometric subtoposes.

It should be possible to include Univalence as well, but I'm hazy on the necessary details. Voevodsky's original simplicial model of HoTT has no nontrivial proper lex modalities, but its construction uses AC. More recent cubical-type models of HoTT are constructive, but many of them do have nontrivial proper lex modalities. Possibly the recent "equivariant" cartesian cubical model would work: it exists constructively, and classically is Quillen equivalent to the simplicial model and hence has no nontrivial proper lex modalities; but I'm not quite sure whether the latter equivalence uses AC or only LEM.

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.

> **Comments:**
> **username_3**: 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.  
> **username_0**: That's a lot of input for me. I will mark this as an answer even if I know that my question is not really precise enough to give a definite one. I appreciate the effort.  

---

