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
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
HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit
https://groups.google.com/d/optout.