new preprint available

new preprint available

[Thierry Coquand]

[-- 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 --]

Re: [HoTT] new preprint available

[Martin Escardo]

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

Re: [HoTT] new preprint available

[Martin Escardo]

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

Re: [HoTT] new preprint available

[Andrew Swan]

[-- 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 --]

Re: [HoTT] new preprint available

[Thierry Coquand]

[-- 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 --]

Re: [HoTT] new preprint available

[Martin Escardo]

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.