with one univalent universe and propositional truncation.

Bassel, Fabian and Thierry

--_000_C79A505575594E008217E87C703E28FFchalmersse_-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.21.65 with SMTP id 1mr2530622ljv.4.1484423570090; Sat, 14 Jan 2017 11:52:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.157.8 with SMTP id g8ls399595lfe.39.gmail; Sat, 14 Jan 2017 11:52:48 -0800 (PST) X-Received: by 10.25.40.17 with SMTP id o17mr1376297lfo.25.1484423568768; Sat, 14 Jan 2017 11:52:48 -0800 (PST) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id d130si376504wmf.0.2017.01.14.11.52.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 14 Jan 2017 11:52:48 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cSUNc-0000S9-OL for HomotopyT...@googlegroups.com; Sat, 14 Jan 2017 19:52:48 +0000 Received: from [31.185.232.183] (helo=[192.168.1.128]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cSUNc-0002Bi-EO for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Sat, 14 Jan 2017 19:52:48 +0000 Subject: Re: [HoTT] new preprint available To: "HomotopyT...@googlegroups.com" References: From: Martin Escardo Message-ID: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> Date: Sat, 14 Jan 2017 19:52:48 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) 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 From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.156.197 with SMTP id f188mr2692992lfe.14.1484562758482; Mon, 16 Jan 2017 02:32:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.13.18 with SMTP id 18ls957878ljn.53.gmail; Mon, 16 Jan 2017 02:32:37 -0800 (PST) X-Received: by 10.46.78.26 with SMTP id c26mr335518ljb.20.1484562757709; Mon, 16 Jan 2017 02:32:37 -0800 (PST) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id d130si692567wmf.0.2017.01.16.02.32.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Jan 2017 02:32:37 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.127] (helo=bham.ac.uk) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cT4ab-00013p-O1 for HomotopyT...@googlegroups.com; Mon, 16 Jan 2017 10:32:37 +0000 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1cT4ab-0000Ov-EC for HomotopyT...@googlegroups.com using interface smart1.bham.ac.uk; Mon, 16 Jan 2017 10:32:37 +0000 Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1cT4ab-0007mq-Eo for HomotopyT...@googlegroups.com; Mon, 16 Jan 2017 10:32:37 +0000 Subject: Re: [HoTT] new preprint available To: "HomotopyT...@googlegroups.com" References: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> From: Martin Escardo Message-ID: <204f54d4-02bf-ee74-abe8-8efdb28a0d15@googlemail.com> Date: Mon, 16 Jan 2017 10:35:33 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 MIME-Version: 1.0 In-Reply-To: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes 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 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-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.9.206 with SMTP id 197mr3149208ljj.12.1484577106321; Mon, 16 Jan 2017 06:31:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.166.150 with SMTP id p144ls1522341wme.0.canary-gmail; Mon, 16 Jan 2017 06:31:45 -0800 (PST) X-Received: by 10.28.54.160 with SMTP id y32mr645729wmh.17.1484577105447; Mon, 16 Jan 2017 06:31:45 -0800 (PST) Return-Path: Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id d130si742288wmf.0.2017.01.16.06.31.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 16 Jan 2017 06:31:45 -0800 (PST) Received-SPF: neutral (google.com: 129.16.226.131 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.131; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.131 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Received: from tyrell.ita.chalmers.se (129.16.226.132) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (TLS) id 15.1.396.30; Mon, 16 Jan 2017 15:31:44 +0100 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.0396.037; Mon, 16 Jan 2017 15:31:44 +0100 From: Thierry Coquand To: Andrew Swan CC: Homotopy Type Theory Subject: Re: [HoTT] new preprint available Thread-Topic: [HoTT] new preprint available Thread-Index: AQHSa+jf2+scNBdo/0maBEhc65+oAKE4VvoAgALFkwCAAAViAA== Date: Mon, 16 Jan 2017 14:31:44 +0000 Message-ID: References: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> <8ec7b882-b52e-4c65-8c68-075585ddba26@googlegroups.com> In-Reply-To: <8ec7b882-b52e-4c65-8c68-075585ddba26@googlegroups.com> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-exchange-messagesentrepresentingtype: 1 x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_D893469D9283474799856B4C8E1AAC86chalmersse_" MIME-Version: 1.0 --_000_D893469D9283474799856B4C8E1AAC86chalmersse_ Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: base64 IEkgdGhpbmsgc28gdG9vLiBUaGUgc3BhY2VzIHdlIGhhdmUgYmVlbiB1c2luZyBhcmUgdW5pdCBp bnRlcnZhbCAoMCwxKSBmb3INCmNvdW50YWJsZSBjaG9pY2UgYW5kIENhbnRvciBzcGFjZSB7MCwx fV5OIGZvciBNYXJrb3YgcHJpbmNpcGxlLCBhbmQgdGhlDQp0b3BvbG9naWNhbCBzcGFjZSBpbiB5 b3VyIGNvdW50ZXItZXhhbXBsZSBpcyB0aGUgcHJvZHVjdCBvZiB0aGVzZQ0KdHdvIHNwYWNlcy4N CiBUbyBhZGFwdCB0aGUgc3RhY2sgbW9kZWwgaW4gdGhpcyBjYXNlLCBvbmUgY2FuIG5vdGljZSB0 aGF0IGEgY29udGludW91cw0KZnVuY3Rpb24gVSB4IFYgLT4gTmF0LCB3aGVyZSBVIGlzIGFuIG9w ZW4gaW50ZXJ2YWwNCmluICgwLDEpIGFuZCBWIGEgY2xvc2VkIG9wZW4gc3Vic2V0IG9mIENhbnRv ciBzcGFjZSwgaXMgZXhhY3RseSBnaXZlbg0KYnkgYSBmaW5pdGUgcGFydGl0aW9uIFYxLOKApixW ayBvZiBWIGluIGNsb3NlZCBvcGVuIHN1YnNldHMgYW5kIGsgZGlzdGluY3QNCm5hdHVyYWwgbnVt YmVycy4NCiBCZXN0LCBUaGllcnJ5DQoNCk9uIDE2IEphbiAyMDE3LCBhdCAxNToxMiwgQW5kcmV3 IFN3YW4gPHdha2VsaS4uLkBnbWFpbC5jb208bWFpbHRvOndha2VsaS4uLkBnbWFpbC5jb20+PiB3 cm90ZToNCg0KSSBkb24ndCBrbm93IG11Y2ggYWJvdXQgc3RhY2tzLCBidXQgYWZ0ZXIgYSBicmll ZiByZWFkIHRocm91Z2ggb2YgVGhpZXJyeSdzIHBhcGVyLCBpdCBsb29rcyBsaWtlIHRoZXkgYXJl IHN1ZmZpY2llbnRseSBzaW1pbGFyIHRvIHNoZWF2ZXMgdGhhdCB0aGUgdG9wb2xvZ2ljYWwgbW9k ZWwgSSBza2V0Y2hlZCBvdXQgaW4gdGhlIGNvbnN0cnVjdGl2ZW5ld3MgdGhyZWFkIGJlZm9yZTxo dHRwczovL2dyb3Vwcy5nb29nbGUuY29tL2QvbXNnL2NvbnN0cnVjdGl2ZW5ld3MvUGVMc1FXREZK TmcvVnNHRmtab01BUUFKPiBzaG91bGQgc3RpbGwgd29yay4NCg0KQmVzdCwNCkFuZHJldw0KDQpP biBTYXR1cmRheSwgMTQgSmFudWFyeSAyMDE3IDIwOjUyOjUwIFVUQysxLCBNYXJ0aW4gSG90emVs IEVzY2FyZG8gd3JvdGU6DQpPbiAxMS8wMS8xNyAwODo1OCwgVGhpZXJyeSBDb3F1YW5kIHdyb3Rl Og0KPg0KPiAgQSBuZXcgcHJlcHJpbnQgaXMgYXZhaWxhYmxlIG9uIGFyWGl2DQo+DQo+IGh0dHA6 Ly9hcnhpdi5vcmcvYWJzLzE3MDEuMDI1NzENCj4NCj4gd2hlcmUgd2UgcHJlc2VudCBhIHN0YWNr IHNlbWFudGljcyBvZiB0eXBlIHRoZW9yeSwgYW5kIHVzZSBpdCB0bw0KPiBzaG93IHRoYXQgY291 bnRhYmxlIGNob2ljZSBpcyBub3QgcHJvdmFibGUgaW4gZGVwZW5kZW50IHR5cGUgdGhlb3J5DQo+ IHdpdGggb25lIHVuaXZhbGVudCB1bml2ZXJzZSBhbmQgcHJvcG9zaXRpb25hbCB0cnVuY2F0aW9u Lg0KDQpOaWNlLiBBbmQgdXNlZnVsIHRvIGtub3cuDQoNCkkgd29uZGVyIHdoZXRoZXIgeW91ciBt b2RlbCwgb3IgYSBzdWl0YWJsZSBhZGFwdGF0aW9uLCBjYW4gcHJvdmUNCnNvbWV0aGluZyBzdHJv bmdlciwgbmFtZWx5IHRoYXQgYSB3ZWFrZW5pbmcgb2YgY291bnRhYmxlIGNob2ljZSBpcw0KYWxy ZWFkeSBub3QgcHJvdmFibGUuIChXZSBjYW4gZGlzY3VzcyBpbiBhbm90aGVyIG9wcG9ydHVuaXR5 IHdoeSB0aGlzIGlzDQppbnRlcmVzdGluZyBhbmQgaG93IGl0IGFyaXNlcy4pDQoNClRoZSB3ZWFr ZW5pbmcgaXMNCg0KICAgICgobjpOKSAtPiB8fCBBIG4gKyBCIHx8KSAtPiB8fCAobjpOKSAtPiBB IG4gKyBCIHx8DQoNCndoZXJlIEEgbiBpcyBhIGRlY2lkYWJsZSBwcm9wb3NpdGlvbiBhbmQgQiBp cyBhIHNldC4NCg0KKEFjdHVhbGx5LCB0aGUgZnVydGhlciB3ZWFrZW5pbmcgaW4gd2hpY2ggQiBp cyBhbiBhcmJpdHJhcnkgc3Vic2V0IG9mDQp0aGUgQ2FudG9yIHR5cGUgKE4tPjIpIGlzIGFsc28g aW50ZXJlc3RpbmcuIEl0IHdvdWxkIGFsc28gYmUgaW50ZXJlc3RpbmcNCnRvIGtub3cgd2hldGhl ciBpdCBpcyBwcm92YWJsZS4gSSBzdXNwZWN0IGl0IGlzbid0LikNCg0KV2Uga25vdyB0aGF0IGNv dW50YWJsZSBjaG9pY2UgaXMgbm90IHByb3ZhYmxlIGZyb20gZXhjbHVkZWQgbWlkZGxlLg0KDQpC dXQgdGhlIGFib3ZlIGluc3RhbmNlIGlzLiAoQW5kIG11Y2ggbGVzcyB0aGFuIGV4Y2x1ZGVkIG1p ZGRsZSBpcyBlbm91Z2guKQ0KDQpCZXN0LA0KTWFydGluDQoNCg0KLS0NCllvdSByZWNlaXZlZCB0 aGlzIG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQgdG8gdGhlIEdvb2dsZSBHcm91 cHMgIkhvbW90b3B5IFR5cGUgVGhlb3J5IiBncm91cC4NClRvIHVuc3Vic2NyaWJlIGZyb20gdGhp cyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNlbmQgYW4gZW1haWwg dG8gSG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb208bWFpbHRvOkhvbW90b3B5VHlw ZVRoZS4uLkBnb29nbGVncm91cHMuY29tPi4NCkZvciBtb3JlIG9wdGlvbnMsIHZpc2l0IGh0dHBz Oi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQuDQoNCg== --_000_D893469D9283474799856B4C8E1AAC86chalmersse_ Content-Type: text/html; charset="utf-8" Content-ID: <716DBA95FD738F4E...@chalmers.se> Content-Transfer-Encoding: base64 PGh0bWw+DQo8aGVhZD4NCjxtZXRhIGh0dHAtZXF1aXY9IkNvbnRlbnQtVHlwZSIgY29udGVudD0i dGV4dC9odG1sOyBjaGFyc2V0PXV0Zi04Ij4NCjwvaGVhZD4NCjxib2R5IHN0eWxlPSJ3b3JkLXdy YXA6IGJyZWFrLXdvcmQ7IC13ZWJraXQtbmJzcC1tb2RlOiBzcGFjZTsgLXdlYmtpdC1saW5lLWJy ZWFrOiBhZnRlci13aGl0ZS1zcGFjZTsiIGNsYXNzPSIiPg0KPGRpdiBjbGFzcz0iIj4mbmJzcDtJ IHRoaW5rIHNvIHRvby4gVGhlIHNwYWNlcyB3ZSBoYXZlIGJlZW4gdXNpbmcgYXJlIHVuaXQgaW50 ZXJ2YWwgKDAsMSkgZm9yPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPmNvdW50YWJsZSBjaG9pY2UgYW5k IENhbnRvciBzcGFjZSB7MCwxfV5OIGZvciBNYXJrb3YgcHJpbmNpcGxlLCBhbmQgdGhlPC9kaXY+ DQo8ZGl2IGNsYXNzPSIiPnRvcG9sb2dpY2FsIHNwYWNlIGluIHlvdXIgY291bnRlci1leGFtcGxl IGlzIHRoZSBwcm9kdWN0IG9mIHRoZXNlPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPnR3byBzcGFjZXMu Jm5ic3A7PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPiZuYnNwO1RvIGFkYXB0IHRoZSBzdGFjayBtb2Rl bCBpbiB0aGlzIGNhc2UsIG9uZSBjYW4gbm90aWNlIHRoYXQgYSBjb250aW51b3VzPC9kaXY+DQo8 ZGl2IGNsYXNzPSIiPmZ1bmN0aW9uIFUgeCBWIC0mZ3Q7IE5hdCwgd2hlcmUgVSBpcyBhbiBvcGVu IGludGVydmFsPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPmluICgwLDEpIGFuZCBWIGEgY2xvc2VkIG9w ZW4gc3Vic2V0IG9mIENhbnRvciBzcGFjZSwgaXMgZXhhY3RseSBnaXZlbiZuYnNwOzwvZGl2Pg0K PGRpdiBjbGFzcz0iIj5ieSBhIGZpbml0ZSBwYXJ0aXRpb24gVjEs4oCmLFZrIG9mIFYgaW4gY2xv c2VkIG9wZW4gc3Vic2V0cyBhbmQgayBkaXN0aW5jdDwvZGl2Pg0KPGRpdiBjbGFzcz0iIj5uYXR1 cmFsIG51bWJlcnMuJm5ic3A7PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPiZuYnNwO0Jlc3QsIFRoaWVy cnk8L2Rpdj4NCjxiciBjbGFzcz0iIj4NCjxkaXY+DQo8YmxvY2txdW90ZSB0eXBlPSJjaXRlIiBj bGFzcz0iIj4NCjxkaXYgY2xhc3M9IiI+T24gMTYgSmFuIDIwMTcsIGF0IDE1OjEyLCBBbmRyZXcg U3dhbiAmbHQ7PGEgaHJlZj0ibWFpbHRvOndha2VsaS4uLkBnbWFpbC5jb20iIGNsYXNzPSIiPndh a2VsaS4uLkBnbWFpbC5jb208L2E+Jmd0OyB3cm90ZTo8L2Rpdj4NCjxiciBjbGFzcz0iQXBwbGUt aW50ZXJjaGFuZ2UtbmV3bGluZSI+DQo8ZGl2IGNsYXNzPSIiPg0KPGRpdiBkaXI9Imx0ciIgY2xh c3M9IiI+SSBkb24ndCBrbm93IG11Y2ggYWJvdXQgc3RhY2tzLCBidXQgYWZ0ZXIgYSBicmllZiBy ZWFkIHRocm91Z2ggb2YgVGhpZXJyeSdzIHBhcGVyLCBpdCBsb29rcyBsaWtlIHRoZXkgYXJlIHN1 ZmZpY2llbnRseSBzaW1pbGFyIHRvIHNoZWF2ZXMgdGhhdCB0aGUgdG9wb2xvZ2ljYWwgbW9kZWwg SSBza2V0Y2hlZCBvdXQgaW4gdGhlDQo8YSBocmVmPSJodHRwczovL2dyb3Vwcy5nb29nbGUuY29t L2QvbXNnL2NvbnN0cnVjdGl2ZW5ld3MvUGVMc1FXREZKTmcvVnNHRmtab01BUUFKIiBjbGFzcz0i Ij4NCmNvbnN0cnVjdGl2ZW5ld3MgdGhyZWFkIGJlZm9yZTwvYT4gc2hvdWxkIHN0aWxsIHdvcmsu DQo8ZGl2IGNsYXNzPSIiPjxiciBjbGFzcz0iIj4NCjwvZGl2Pg0KPGRpdiBjbGFzcz0iIj5CZXN0 LDwvZGl2Pg0KPGRpdiBjbGFzcz0iIj5BbmRyZXc8YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+ DQpPbiBTYXR1cmRheSwgMTQgSmFudWFyeSAyMDE3IDIwOjUyOjUwIFVUQyYjNDM7MSwgTWFydGlu IEhvdHplbCBFc2NhcmRvIHdyb3RlOg0KPGJsb2NrcXVvdGUgY2xhc3M9ImdtYWlsX3F1b3RlIiBz dHlsZT0ibWFyZ2luOiAwO21hcmdpbi1sZWZ0OiAwLjhleDtib3JkZXItbGVmdDogMXB4ICNjY2Mg c29saWQ7cGFkZGluZy1sZWZ0OiAxZXg7Ij4NCk9uIDExLzAxLzE3IDA4OjU4LCBUaGllcnJ5IENv cXVhbmQgd3JvdGU6IDxiciBjbGFzcz0iIj4NCiZndDsgPGJyIGNsYXNzPSIiPg0KJmd0OyAmbmJz cDtBIG5ldyBwcmVwcmludCBpcyBhdmFpbGFibGUgb24gYXJYaXYgPGJyIGNsYXNzPSIiPg0KJmd0 OyA8YnIgY2xhc3M9IiI+DQomZ3Q7IDxhIGhyZWY9Imh0dHA6Ly9hcnhpdi5vcmcvYWJzLzE3MDEu MDI1NzEiIHRhcmdldD0iX2JsYW5rIiByZWw9Im5vZm9sbG93IiBvbm1vdXNlZG93bj0idGhpcy5o cmVmPSdodHRwOi8vd3d3Lmdvb2dsZS5jb20vdXJsP3FceDNkaHR0cCUzQSUyRiUyRmFyeGl2Lm9y ZyUyRmFicyUyRjE3MDEuMDI1NzFceDI2c2FceDNkRFx4MjZzbnR6XHgzZDFceDI2dXNnXHgzZEFG UWpDTkVtZDFIMVo1VG83Mkd1bVRMRnM3Z1RpYzVkOFEnO3JldHVybiB0cnVlOyIgb25jbGljaz0i dGhpcy5ocmVmPSdodHRwOi8vd3d3Lmdvb2dsZS5jb20vdXJsP3FceDNkaHR0cCUzQSUyRiUyRmFy eGl2Lm9yZyUyRmFicyUyRjE3MDEuMDI1NzFceDI2c2FceDNkRFx4MjZzbnR6XHgzZDFceDI2dXNn XHgzZEFGUWpDTkVtZDFIMVo1VG83Mkd1bVRMRnM3Z1RpYzVkOFEnO3JldHVybiB0cnVlOyIgY2xh c3M9IiI+DQpodHRwOi8vYXJ4aXYub3JnL2Ficy8xNzAxLjx3YnIgY2xhc3M9IiI+MDI1NzE8L2E+ IDxiciBjbGFzcz0iIj4NCiZndDsgPGJyIGNsYXNzPSIiPg0KJmd0OyB3aGVyZSB3ZSBwcmVzZW50 IGEgc3RhY2sgc2VtYW50aWNzIG9mIHR5cGUgdGhlb3J5LCBhbmQgdXNlIGl0IHRvIDxiciBjbGFz cz0iIj4NCiZndDsgc2hvdyB0aGF0IGNvdW50YWJsZSBjaG9pY2UgaXMgbm90IHByb3ZhYmxlIGlu IGRlcGVuZGVudCB0eXBlIHRoZW9yeSA8YnIgY2xhc3M9IiI+DQomZ3Q7IHdpdGggb25lIHVuaXZh bGVudCB1bml2ZXJzZSBhbmQgcHJvcG9zaXRpb25hbCB0cnVuY2F0aW9uLiA8YnIgY2xhc3M9IiI+ DQo8YnIgY2xhc3M9IiI+DQpOaWNlLiBBbmQgdXNlZnVsIHRvIGtub3cuIDxiciBjbGFzcz0iIj4N CjxiciBjbGFzcz0iIj4NCkkgd29uZGVyIHdoZXRoZXIgeW91ciBtb2RlbCwgb3IgYSBzdWl0YWJs ZSBhZGFwdGF0aW9uLCBjYW4gcHJvdmUgPGJyIGNsYXNzPSIiPg0Kc29tZXRoaW5nIHN0cm9uZ2Vy LCBuYW1lbHkgdGhhdCBhIHdlYWtlbmluZyBvZiBjb3VudGFibGUgY2hvaWNlIGlzIDxiciBjbGFz cz0iIj4NCmFscmVhZHkgbm90IHByb3ZhYmxlLiAoV2UgY2FuIGRpc2N1c3MgaW4gYW5vdGhlciBv cHBvcnR1bml0eSB3aHkgdGhpcyBpcyA8YnIgY2xhc3M9IiI+DQppbnRlcmVzdGluZyBhbmQgaG93 IGl0IGFyaXNlcy4pIDxiciBjbGFzcz0iIj4NCjxiciBjbGFzcz0iIj4NClRoZSB3ZWFrZW5pbmcg aXMgPGJyIGNsYXNzPSIiPg0KPGJyIGNsYXNzPSIiPg0KJm5ic3A7ICZuYnNwOyAoKG46TikgLSZn dDsgfHwgQSBuICYjNDM7IEIgfHwpIC0mZ3Q7IHx8IChuOk4pIC0mZ3Q7IEEgbiAmIzQzOyBCIHx8 IDxiciBjbGFzcz0iIj4NCjxiciBjbGFzcz0iIj4NCndoZXJlIEEgbiBpcyBhIGRlY2lkYWJsZSBw cm9wb3NpdGlvbiBhbmQgQiBpcyBhIHNldC4gPGJyIGNsYXNzPSIiPg0KPGJyIGNsYXNzPSIiPg0K KEFjdHVhbGx5LCB0aGUgZnVydGhlciB3ZWFrZW5pbmcgaW4gd2hpY2ggQiBpcyBhbiBhcmJpdHJh cnkgc3Vic2V0IG9mIDxiciBjbGFzcz0iIj4NCnRoZSBDYW50b3IgdHlwZSAoTi0mZ3Q7MikgaXMg YWxzbyBpbnRlcmVzdGluZy4gSXQgd291bGQgYWxzbyBiZSBpbnRlcmVzdGluZyA8YnIgY2xhc3M9 IiI+DQp0byBrbm93IHdoZXRoZXIgaXQgaXMgcHJvdmFibGUuIEkgc3VzcGVjdCBpdCBpc24ndC4p IDxiciBjbGFzcz0iIj4NCjxiciBjbGFzcz0iIj4NCldlIGtub3cgdGhhdCBjb3VudGFibGUgY2hv aWNlIGlzIG5vdCBwcm92YWJsZSBmcm9tIGV4Y2x1ZGVkIG1pZGRsZS4gPGJyIGNsYXNzPSIiPg0K PGJyIGNsYXNzPSIiPg0KQnV0IHRoZSBhYm92ZSBpbnN0YW5jZSBpcy4gKEFuZCBtdWNoIGxlc3Mg dGhhbiBleGNsdWRlZCBtaWRkbGUgaXMgZW5vdWdoLikgPGJyIGNsYXNzPSIiPg0KPGJyIGNsYXNz PSIiPg0KQmVzdCwgPGJyIGNsYXNzPSIiPg0KTWFydGluIDxiciBjbGFzcz0iIj4NCjxiciBjbGFz cz0iIj4NCjwvYmxvY2txdW90ZT4NCjwvZGl2Pg0KPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPjxiciBj bGFzcz0id2Via2l0LWJsb2NrLXBsYWNlaG9sZGVyIj4NCjwvZGl2Pg0KLS0gPGJyIGNsYXNzPSIi Pg0KWW91IHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBiZWNhdXNlIHlvdSBhcmUgc3Vic2NyaWJlZCB0 byB0aGUgR29vZ2xlIEdyb3VwcyAmcXVvdDtIb21vdG9weSBUeXBlIFRoZW9yeSZxdW90OyBncm91 cC48YnIgY2xhc3M9IiI+DQpUbyB1bnN1YnNjcmliZSBmcm9tIHRoaXMgZ3JvdXAgYW5kIHN0b3Ag cmVjZWl2aW5nIGVtYWlscyBmcm9tIGl0LCBzZW5kIGFuIGVtYWlsIHRvDQo8YSBocmVmPSJtYWls dG86SG9tb3RvcHlUeXBlVGhlb3J5JiM0Mzt1bnN1Li4uQGdvb2dsZWdyb3Vwcy5jb20iIGNsYXNz PSIiPkhvbW90b3B5VHlwZVRoZW9yeSYjNDM7dW5zdS4uLkBnb29nbGVncm91cHMuY29tPC9hPi48 YnIgY2xhc3M9IiI+DQpGb3IgbW9yZSBvcHRpb25zLCB2aXNpdCA8YSBocmVmPSJodHRwczovL2dy b3Vwcy5nb29nbGUuY29tL2Qvb3B0b3V0IiBjbGFzcz0iIj5odHRwczovL2dyb3Vwcy5nb29nbGUu Y29tL2Qvb3B0b3V0PC9hPi48YnIgY2xhc3M9IiI+DQo8L2Rpdj4NCjwvYmxvY2txdW90ZT4NCjwv ZGl2Pg0KPGJyIGNsYXNzPSIiPg0KPC9ib2R5Pg0KPC9odG1sPg0K --_000_D893469D9283474799856B4C8E1AAC86chalmersse_-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.157.70 with SMTP id g67mr44624wme.1.1484862569711; Thu, 19 Jan 2017 13:49:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.33.230 with SMTP id h99ls387311lji.23.gmail; Thu, 19 Jan 2017 13:49:28 -0800 (PST) X-Received: by 10.46.8.10 with SMTP id 10mr1107964lji.21.1484862568829; Thu, 19 Jan 2017 13:49:28 -0800 (PST) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id v70si45918wmf.0.2017.01.19.13.49.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jan 2017 13:49:28 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cUKaG-0001y4-O8; Thu, 19 Jan 2017 21:49:28 +0000 Received: from [31.185.232.183] (helo=[192.168.1.128]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cUKaG-0006zs-E6 using interface auth-smtp.bham.ac.uk; Thu, 19 Jan 2017 21:49:28 +0000 Subject: Re: [HoTT] new preprint available To: Thierry Coquand , Andrew Swan References: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com> <8ec7b882-b52e-4c65-8c68-075585ddba26@googlegroups.com> Cc: Homotopy Type Theory From: Martin Escardo Message-ID: Date: Thu, 19 Jan 2017 21:49:27 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) 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 > > 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 >> >> 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 >> . >> 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 > . > For more options, visit https://groups.google.com/d/optout.