From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.192.13 with SMTP id q13mr42736194vkf.0.1473314780908; Wed, 07 Sep 2016 23:06:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.20.97 with SMTP id h88ls1931191oth.6.gmail; Wed, 07 Sep 2016 23:06:20 -0700 (PDT) X-Received: by 10.31.194.79 with SMTP id s76mr42509428vkf.10.1473314780399; Wed, 07 Sep 2016 23:06:20 -0700 (PDT) Return-Path: Received: from mail-qk0-x22d.google.com (mail-qk0-x22d.google.com. [2607:f8b0:400d:c09::22d]) by gmr-mx.google.com with ESMTPS id d206si3075078ywh.3.2016.09.07.23.06.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 23:06:20 -0700 (PDT) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::22d as permitted sender) client-ip=2607:f8b0:400d:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::22d as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-qk0-x22d.google.com with SMTP id w204so34337478qka.0 for ; Wed, 07 Sep 2016 23:06:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=sxzKnn9ZysGr11ZBnyYNTY1MLLkpZYA7Gz8lRfXlk1A=; b=f4mkPaTCT00VwojJujPc2k5ovca6UfaG78zCtZOELK7cUVMp5kI67qcx0ifI6S1jY1 /6DIIzg5Qu31SEi8Be6wVi45GMOv5KnelXL/TQs5AAwNJUQKxUai+UEFIzDJPw4o7NjV 8g9z7y2VUph70R/Ca11funCfsWCXvG7JxzsNhz2NayNUgodkDOiPdnUJlrLkaY1CTPG/ g9ES14UfeV42F8G/QLhSCCQvqRgcc/PWeEKk//KokH3aDAqW8yDhOOwbgGBi1C7LeT+l RMHQoVhgtFPyVH8Qoq7m2DzX5zh6qh1yBragIKg5zb9Pcxg0L1RsHpTuQGu6PqZ/x/Mc M9OQ== X-Gm-Message-State: AE9vXwPlVwGI++xZroclSZX5xFl6uEiQskmbQSzSGZSLvGkX6OgCdbUfFr9Znh8UwbntToWe07KHW5bSlTrYOA== X-Received: by 10.55.217.2 with SMTP id u2mr41554388qki.246.1473314780136; Wed, 07 Sep 2016 23:06:20 -0700 (PDT) MIME-Version: 1.0 References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> In-Reply-To: From: Jason Gross Date: Thu, 08 Sep 2016 06:06:08 +0000 Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Michael Shulman , Matt Oliveri Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a1149aaa01cccf7053bf8d42d --001a1149aaa01cccf7053bf8d42d Content-Type: text/plain; charset=UTF-8 > 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? I am not sure what you mean by internally, but the way I usually motivate univalence is: we can ask "which equalities (Id U X Y) are provable in MLTT?" The answer is: "only when X and Y are definitionally equal." We can ask: "when can we prove that (Id U X Y) is absurd?" The answer turns out to be: "exactly when X and Y are provably not isomorphic." (The proof that this is the most general answer is the proof that univalence is consistent.) So it seems natural to ask about the two extremes. On the one hand, the converse of the strictest equality we can have is the equality reflection rule. On the other extreme, the inverse of the weakest equality rule is logically equivalent to univalence. On Wed, Sep 7, 2016, 9:15 PM 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. > > -- > 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. > --001a1149aaa01cccf7053bf8d42d Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

> 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?

I am not sure what you mean by internally, but the way I usu= ally motivate univalence is: we can ask "which equalities (Id U X Y) a= re provable in MLTT?"=C2=A0 The answer is: "only when X and Y are= definitionally equal."=C2=A0 We can ask: "when can we prove that= (Id U X Y) is absurd?"=C2=A0 The answer turns out to be: "exactl= y when X and Y are provably not isomorphic."=C2=A0 (The proof that thi= s is the most general answer is the proof that univalence is consistent.)= =C2=A0 So it seems natural to ask about the two extremes.=C2=A0 On the one = hand, the converse of the strictest equality we can have is the equality re= flection rule.=C2=A0 On the other extreme, the inverse of the weakest equal= ity rule is logically equivalent to univalence.=C2=A0


On Wed, Sep 7, 2016, 9:15 P= M Michael Shulman <shu...@sandieg= o.edu> wrote:
Does "Zer= melo-style set-theoretic equality" even make sense in MLTT?
Types don't have the global membership structure that Zermelo-sets do.<= br>
On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri <atm...@gmail.com> wrote:
> On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escar= do
> 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 a= s
> types of U, and their elements as the corresponding elements. (Conject= ure?)
> Whereas without K, we don't know how to interpret ITT types as typ= es 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, s= ay
>> within intensional MLTT, where it was introduced, and, internally = in
>> MLTT, ponder what it can be, and identify the only "compellin= g" thing it
>> can be as the type of equivalences X~Y, where "compelling&quo= t; is a notion
>> remote from univalence?
>
>
> How does Zermelo-style set-theoretic equality get ruled out as a poten= tial
> "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 Gro= ups
> "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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--001a1149aaa01cccf7053bf8d42d--