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