From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.117.197 with SMTP id kg5mr3772112wjb.6.1473325670114; Thu, 08 Sep 2016 02:07:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.152.5 with SMTP id a5ls1860678wme.24.canary; Thu, 08 Sep 2016 02:07:49 -0700 (PDT) X-Received: by 10.28.222.4 with SMTP id v4mr1532605wmg.0.1473325669367; Thu, 08 Sep 2016 02:07:49 -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 185si542476wmr.2.2016.09.08.02.07.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Sep 2016 02:07:49 -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 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 1bhvJF-0002J9-N9 for HomotopyT...@googlegroups.com; Thu, 08 Sep 2016 10:07:49 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1bhvJF-0007tb-DL for HomotopyT...@googlegroups.com using interface smart1.bham.ac.uk; Thu, 08 Sep 2016 10:07:49 +0100 Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1bhvJF-0004Sj-1V for HomotopyT...@googlegroups.com; Thu, 08 Sep 2016 10:07:49 +0100 Subject: Re: [HoTT] A puzzle about "univalent equality" References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> To: Homotopy Type Theory From: Martin Escardo Message-ID: Date: Thu, 8 Sep 2016 10:07:51 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes On 08/09/16 07:45, Michael Shulman wrote: > Type theory does have set-theoretic models, of course. But that > doesn't provide a notion of equality that makes sense *inside* MLTT, > compelling or otherwise. Exactly: elementwise equality can't even be formulated internally. However, there is one situation in which elementwise equality can both be formulated and is the equality we get. For a type X define its powerset to be PX := X->Prop. For A:PX write x \in A (like in topos type theory) to mean A(x). Then (A=B) = (forall x:X, x \in A <-> x \in B). In topos type theory we get this because both function extensionality and propositional extensionality hold. In HoTT we get this because these two extensionality properties are a particular case of univalence. In MLTT with equality reflection, you don't get this, because although you get function extensionality, you don't get propositional extensionality. So equality reflection is not doing the job of capturing elementwise equality in the powerset. But univalence is. Martin > > On Wed, Sep 7, 2016 at 11:34 PM, Matt Oliveri wrote: >> True, the language does not provide this structure. But that doesn't mean it >> isn't in the model. Is there a problem interpreting ITT as all Zermelo-style >> sets, with identity as a subsingletons for equality? >> >> On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman wrote: >>> >>> Does "Zermelo-style set-theoretic equality" even make sense in MLTT? >>> Types don't have the global membership structure that Zermelo-sets do. >>> >>> On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri wrote: >>>> On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escardo >>>> wrote: >>>>> >>>>> Some people like the K-axiom for U because ... (let them fill the >>>>> answer). >>>> >>>> >>>> It allows you to interpret (within type theory) the types of ITT + K as >>>> types of U, and their elements as the corresponding elements. >>>> (Conjecture?) >>>> Whereas without K, we don't know how to interpret ITT types as types of >>>> U. >>>> In other words, K is a simple way to give ITT reflection. >>>> >>>>> Can we stare at the type (Id U X Y) objectively, mathematically, say >>>>> within intensional MLTT, where it was introduced, and, internally in >>>>> MLTT, ponder what it can be, and identify the only "compelling" thing >>>>> it >>>>> can be as the type of equivalences X~Y, where "compelling" is a notion >>>>> remote from univalence? >>>> >>>> >>>> How does Zermelo-style set-theoretic equality get ruled out as a >>>> potential >>>> "compelling" meaning for identity? Of course, there's a potential >>>> argument >>>> about what "compelling" ought to be getting at. You seem to not consider >>>> set-theoretic equality compelling, which I can play along with. >> >> -- >> 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. >