From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.210.10 with SMTP id j10mr1410688wmg.4.1473317177702; Wed, 07 Sep 2016 23:46:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.197 with SMTP id 188ls50710ljf.36.gmail; Wed, 07 Sep 2016 23:46:16 -0700 (PDT) X-Received: by 10.25.152.10 with SMTP id a10mr610922lfe.4.1473317176937; Wed, 07 Sep 2016 23:46:16 -0700 (PDT) Return-Path: Received: from mail-lf0-x22a.google.com (mail-lf0-x22a.google.com. [2a00:1450:4010:c07::22a]) by gmr-mx.google.com with ESMTPS id r137si395858wmf.0.2016.09.07.23.46.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 23:46:16 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4010:c07::22a is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2a00:1450:4010:c07::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-lf0-x22a.google.com with SMTP id h127so14191884lfh.0 for ; Wed, 07 Sep 2016 23:46:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=qQ4A8SLa1xUvdtjY4dILLy9vuZRP9gbiPJOVaeBdwvQ=; b=Ms8GOgnS4c1jaQEbOA5aB34lmjdv8csAxpWXZTbU7WbkQxhzogNialeZnfUxTecCzP 7lSGY4wvBgK8MU4OUV2gx/jgzbU8X2j7chHUtRK03l4pw6FSTDskasN4cOMBfDih/41b zVHtSOtaen4jMX6GfZ+17Bw0r1IOwBphpu7pv4OSjptYx/Hnw3F7tkv7HThtzTKW+eo2 AdUJqCVQuhQbhmZZTEo7217XHlkjTOsbVMiGoxHaWYv7vk5mYBCji5WpffrtQ7XyE/ma saQhEfNoTZJpJvYgQpJXWxARyVa35sNZ+10nRTI7Om83IgLgGVqbzBZQEHgDr5ecw8xW zYPg== X-Gm-Message-State: AE9vXwN15GoeOlmYe8cax+pNV4KCOkYZ2c1LlqJDFlfaOlzVLsGCRhEzhuWNZ6RyUArm0Beo X-Received: by 10.46.71.69 with SMTP id u66mr908501lja.14.1473317176271; Wed, 07 Sep 2016 23:46:16 -0700 (PDT) Return-Path: Received: from mail-lf0-f42.google.com (mail-lf0-f42.google.com. [209.85.215.42]) by smtp.gmail.com with ESMTPSA id 202sm2848115ljf.48.2016.09.07.23.46.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 23:46:15 -0700 (PDT) Received: by mail-lf0-f42.google.com with SMTP id h127so14202124lfh.0 for ; Wed, 07 Sep 2016 23:46:15 -0700 (PDT) X-Received: by 10.25.234.1 with SMTP id i1mr920972lfh.84.1473317174873; Wed, 07 Sep 2016 23:46:14 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Wed, 7 Sep 2016 23:45:54 -0700 (PDT) In-Reply-To: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> From: Michael Shulman Date: Wed, 7 Sep 2016 23:45:54 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 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. 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.