From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 16 Jan 2017 06:12:28 -0800 (PST) From: Andrew Swan To: Homotopy Type Theory Message-Id: <8ec7b882-b52e-4c65-8c68-075585ddba26@googlegroups.com> In-Reply-To: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> References: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> Subject: Re: [HoTT] new preprint available MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1207_1940603227.1484575948511" ------=_Part_1207_1940603227.1484575948511 Content-Type: multipart/alternative; boundary="----=_Part_1208_385860805.1484575948511" ------=_Part_1208_385860805.1484575948511 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 > > ------=_Part_1208_385860805.1484575948511 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
I don't know much about stacks, but after a brief read= through of Thierry's paper, it looks like they are sufficiently simila= r to sheaves that the topological model I sketched out in the co= nstructivenews thread before should still work.

Best= ,
Andrew

On Saturday, 14 January 2017 20:52:50 UTC+1, Mart= in Hotzel Escardo wrote:
On 11= /01/17 08:58, Thierry Coquand wrote:
>
> =C2=A0A 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 theor= y
> 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 i= s
interesting and how it arises.)

The weakening is

=C2=A0 =C2=A0 ((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 interes= ting
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 enoug= h.)

Best,
Martin

------=_Part_1208_385860805.1484575948511-- ------=_Part_1207_1940603227.1484575948511--