From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.15.216 with SMTP id 85mr606909lfp.22.1484125109632; Wed, 11 Jan 2017 00:58:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.149.76 with SMTP id x73ls4098lfd.44.gmail; Wed, 11 Jan 2017 00:58:28 -0800 (PST) X-Received: by 10.25.190.200 with SMTP id o191mr606434lff.8.1484125108820; Wed, 11 Jan 2017 00:58:28 -0800 (PST) Return-Path: Received: from targaryen.ita.chalmers.se (targaryen.ita.chalmers.se. [129.16.226.133]) by gmr-mx.google.com with ESMTPS id h198si103494wmg.1.2017.01.11.00.58.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Wed, 11 Jan 2017 00:58:28 -0800 (PST) Received-SPF: neutral (google.com: 129.16.226.133 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.133; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.133 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 targaryen.ita.chalmers.se (129.16.226.133) with Microsoft SMTP Server (TLS) id 15.1.396.30; Wed, 11 Jan 2017 09:58:27 +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; Wed, 11 Jan 2017 09:58:27 +0100 From: Thierry Coquand To: "HomotopyT...@googlegroups.com" Subject: new preprint available Thread-Topic: new preprint available Thread-Index: AQHSa+jftUXpj31jX0utXkkCilmgew== Date: Wed, 11 Jan 2017 08:58:27 +0000 Message-ID: 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_C79A505575594E008217E87C703E28FFchalmersse_" MIME-Version: 1.0 --_000_C79A505575594E008217E87C703E28FFchalmersse_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable 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 --_000_C79A505575594E008217E87C703E28FFchalmersse_ Content-Type: text/html; charset="us-ascii" Content-ID: Content-Transfer-Encoding: quoted-printable

 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 typ= e theory
with one univalent universe and propositional truncation.

 Bassel, Fabian and Thierry
--_000_C79A505575594E008217E87C703E28FFchalmersse_--