Re: [HoTT] new preprint available

[Martin Escardo <escardo...@googlemail.com>]

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.