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.