* new preprint available @ 2017-01-11 8:58 Thierry Coquand 2017-01-14 19:52 ` [HoTT] " Martin Escardo 0 siblings, 1 reply; 6+ messages in thread From: Thierry Coquand @ 2017-01-11 8:58 UTC (permalink / raw) To: HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 303 bytes --] 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. Bassel, Fabian and Thierry [-- Attachment #2: Type: text/html, Size: 856 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] new preprint available 2017-01-11 8:58 new preprint available Thierry Coquand @ 2017-01-14 19:52 ` Martin Escardo 2017-01-16 10:35 ` Martin Escardo 2017-01-16 14:12 ` Andrew Swan 0 siblings, 2 replies; 6+ messages in thread From: Martin Escardo @ 2017-01-14 19:52 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] new preprint available 2017-01-14 19:52 ` [HoTT] " Martin Escardo @ 2017-01-16 10:35 ` Martin Escardo 2017-01-16 14:12 ` Andrew Swan 1 sibling, 0 replies; 6+ messages in thread From: Martin Escardo @ 2017-01-16 10:35 UTC (permalink / raw) To: HomotopyT...@googlegroups.com On 14/01/17 19:52, Martin Escardo wrote: > 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.) I would like to remark that this principle is equivalent to another choice principle. Let *propositional choice* be the principle Pi(P:U), isProp P -> Pi(X:P->U), (Pi(p:P), isSet(X(p)) -> (Pi(p:P), ||X(p)||) -> ||Pi(p:P), X(p)||. This is equivalent to Pi(P,Y:U), isProp P -> isSet(Y) -> (P -> ||Y||) -> ||P -> Y||. Hence we see that it holds for decidable P, and thus holds for all P if excluded middle holds. The above countable choice principle is equivalence to propositional choice with P of the form Sigma(n:N).a(n)=0 with a:N->2 and isProp(Sigma(n:N), a(n)=0). (The statement that all such P are decidable is called LPO.) Martin ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] new preprint available 2017-01-14 19:52 ` [HoTT] " Martin Escardo 2017-01-16 10:35 ` Martin Escardo @ 2017-01-16 14:12 ` Andrew Swan 2017-01-16 14:31 ` Thierry Coquand 1 sibling, 1 reply; 6+ messages in thread From: Andrew Swan @ 2017-01-16 14:12 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1560 bytes --] 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 > > [-- Attachment #1.2: Type: text/html, Size: 2350 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] new preprint available 2017-01-16 14:12 ` Andrew Swan @ 2017-01-16 14:31 ` Thierry Coquand 2017-01-19 21:49 ` Martin Escardo 0 siblings, 1 reply; 6+ messages in thread From: Thierry Coquand @ 2017-01-16 14:31 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 2485 bytes --] 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 <wakeli...@gmail.com<mailto:wakeli...@gmail.com>> 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<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 -- 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<mailto:HomotopyTypeThe...@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4656 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] new preprint available 2017-01-16 14:31 ` Thierry Coquand @ 2017-01-19 21:49 ` Martin Escardo 0 siblings, 0 replies; 6+ messages in thread From: Martin Escardo @ 2017-01-19 21:49 UTC (permalink / raw) To: Thierry Coquand, Andrew Swan; +Cc: Homotopy Type Theory On 16/01/17 14:31, Thierry Coquand wrote: > 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. Can you say a word about how this works not only in this case but in general? How do you move from sheaf semantics to stack semantics? Martin > Best, Thierry > >> On 16 Jan 2017, at 15:12, Andrew Swan <wakeli...@gmail.com >> <mailto:wakeli...@gmail.com>> 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 >> <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 <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 >> <mailto:HomotopyTypeThe...@googlegroups.com>. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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 > <mailto:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2017-01-19 21:49 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-01-11 8:58 new preprint available Thierry Coquand 2017-01-14 19:52 ` [HoTT] " Martin Escardo 2017-01-16 10:35 ` Martin Escardo 2017-01-16 14:12 ` Andrew Swan 2017-01-16 14:31 ` Thierry Coquand 2017-01-19 21:49 ` Martin Escardo
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).