Do basic open propositions have choice?

[felixwellen]

A type $X$ has choice if $\prod_{x:X}||B(x)||\to ||\prod_{x:X}B(x)||$. We know that closed propositions and more generally every spectrum of a finitely presented local algebra has choice (and finite coproducts thereof). Open propositions should not have choice in general. I tend more to believing that basic open propositions do not satisfy choice, but I don't know if we have a result in either direction.

[dwarn]

Somehow the only obstruction to choice over affine schemes is the locality axiom, so I would look for a counterexample there. Specifically, let $x ,y : R$ be arbitrary ring elements, let $X$ be the basic open proposition $\mathrm{inv}(x+y)$, and let $B$ be the type $\mathrm{inv}(x) + \mathrm{inv}(y)$. Then we do have $X \to \lVert B \rVert$, but I'd expect we can show it's not true that $\lVert X \to B \rVert$ for all $x,y : R$.