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