new preprint available

[Thierry Coquand]

 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

[Martin Escardo]

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

[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

[Andrew Swan]

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

[Thierry Coquand]

 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

--
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.

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

>> <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>.