I don't know much about stacks, but after a brief read through of Thierry's 
paper, it looks like they are sufficiently similar to sheaves that the 
topological model I sketched out in the constructivenews thread before 
<https://groups.google.com/d/msg/constructivenews/PeLsQWDFJNg/VsGFkZoMAQAJ> 
should still work.

Best,
Andrew

On Saturday, 14 January 2017 20:52:50 UTC+1, Martin Hotzel Escardo wrote:
>
> On 11/01/17 08:58, Thierry Coquand wrote: 
> > 
> >  A new preprint is available on arXiv 
> > 
> > http://arxiv.org/abs/1701.02571 
> > 
> > where we present a stack semantics of type theory, and use it to 
> > show that countable choice is not provable in dependent type theory 
> > with one univalent universe and propositional truncation. 
>
> Nice. And useful to know. 
>
> I wonder whether your model, or a suitable adaptation, can prove 
> something stronger, namely that a weakening of countable choice is 
> already not provable. (We can discuss in another opportunity why this is 
> interesting and how it arises.) 
>
> The weakening is 
>
>     ((n:N) -> || A n + B ||) -> || (n:N) -> A n + B || 
>
> where A n is a decidable proposition and B is a set. 
>
> (Actually, the further weakening in which B is an arbitrary subset of 
> the Cantor type (N->2) is also interesting. It would also be interesting 
> to know whether it is provable. I suspect it isn't.) 
>
> We know that countable choice is not provable from excluded middle. 
>
> But the above instance is. (And much less than excluded middle is enough.) 
>
> Best, 
> Martin 
>
>