From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.215.220 with SMTP id q89mr786965lfi.28.1491588604978; Fri, 07 Apr 2017 11:10:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.28.10 with SMTP id c10ls349420wmc.9.gmail; Fri, 07 Apr 2017 11:10:04 -0700 (PDT) X-Received: by 10.28.156.198 with SMTP id f189mr33788wme.19.1491588604064; Fri, 07 Apr 2017 11:10:04 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id d184si313612wmc.0.2017.04.07.11.10.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 07 Apr 2017 11:10:04 -0700 (PDT) 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 1cwYKh-0000NJ-Oc; Fri, 07 Apr 2017 19:10:03 +0100 Received: from 128.172.125.91.dyn.plus.net ([91.125.172.128] helo=[192.168.1.75]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cwYKh-0005cC-Ef using interface auth-smtp.bham.ac.uk; Fri, 07 Apr 2017 19:10:03 +0100 Subject: Re: [HoTT] Conjecture To: Michael Shulman References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com> <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> <20170406115247.GC25210@mathematik.tu-darmstadt.de> <4c10260c-cde9-a1e9-8ed1-f8b19610e059@googlemail.com> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: <2c2fac47-505a-07d9-31e2-5e1a32f360a1@googlemail.com> Date: Fri, 7 Apr 2017 19:10:03 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 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 07/04/17 18:11, Michael Shulman wrote: > On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type > Theory wrote: >> (1) Indeed, I do like to think of the fragment of univalent type >> theory consisting of function extensionality + proposition >> extensionality + propositional truncation as essentially the same >> thing as topos logic, provided we have propositional resizing. (But, >> as discussed, much can be done without propositional resizing (but not >> all), and one way of looking at HIT's is as a mechanism to avoid >> resizing.) > > I would say that to really be talking about (elementary) topos logic, > one should also do without universes other than hProp. Of course, > elementary 1-toposes also validate UIP. Agreed. (But you can consider elementary toposes with a universe object, and a number of people have worked on that independently of any connection with dependent type theory.) > If we also omit hProp and propositional resizing, but include > nonrecursive HITs as well as ordinary inductive types, then it ought > to be basically Pi-W-pretopos logic; right? I'd let the experts on these details to answer this. I noticed the following mistake immediately after I send my message this morning, and this is a good opportunity to rectify it: >> In topos logic, you define (for the dominance of all propositions) >> >> Lift(X) = { A:X->Omega | (exists(x:X), A x) & >> forall(x,y:X), A x -> A y -> x = y } >> Lift(X) = { A:X->Omega | forall(x,y:X), A x -> A y -> x = y } If anybody noticed, they probably knew I meant that, and, if they didn't notice, they probably understood that. There are other possibilities, of course. :-) Martin