I think so too. The spaces we have been using are unit interval (0,1) for countable choice and Cantor space {0,1}^N for Markov principle, and the topological space in your counter-example is the product of these two spaces. To adapt the stack model in this case, one can notice that a continuous function U x V -> Nat, where U is an open interval in (0,1) and V a closed open subset of Cantor space, is exactly given by a finite partition V1,…,Vk of V in closed open subsets and k distinct natural numbers. Best, Thierry On 16 Jan 2017, at 15:12, Andrew Swan > wrote: 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 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 -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.