From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:dc56:: with SMTP id f22mr102499pgj.284.1588614198772; Mon, 04 May 2020 10:43:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:ea0e:: with SMTP id t14ls16018079pfh.3.gmail; Mon, 04 May 2020 10:43:17 -0700 (PDT) X-Received: by 2002:aa7:9511:: with SMTP id b17mr19350748pfp.135.1588614196905; Mon, 04 May 2020 10:43:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588614196; cv=none; d=google.com; s=arc-20160816; b=XwWHKTN5ExXCydJJty3nReH+LkqKJtb+OSSLcuBdi6R1Kh4YyzgnrP3/vRAkPkrLm2 xk2XU28nt8uqXSgDGB8c8QfPvaVB4Fzy0hyFxmK8haXeTFdQ9oH2i+xaa0s94a7SLZOq rT9CzKAif4DYLO1E3uGWccJhccJBEgxB9qU70X+mklDZYmKShJHB0sem9hnlF1BU0PRL XmOvi6G4n/HJPwWoNasnshAX6j3rt6VtAxWVMiDxA8gL3yBI2pSiZnNYX4grdUV3B6NF ZNfOiKOnjTcvpRBTmwKSNgWF5JehZUkadzIBvo645oT5R076vh1sm/HVHWabUczp3tkF yI4Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=YhuhZcECsD3AseLykQtoQJZA5UCX9JiqiI6++LspSgA=; b=edHWkPTLqbJgmSUKMlAfYyKPonZnWxlJGwn/jJ3G6uFeVxE5LNhKumtfMX93Cq1PdU 448ixMKzEkYegnBjR5JmT0+Rq3DDusa59wUOTU+83ll1bEAdrQBb9TUVEHuCbPxfPPx3 JaoraQQEq4rsUIc885bDq7ZNvHce7RS2mie8CRum6fOiHN8Ror8KFTTPwpOukDTueiDP sniUh6ZOVzIYFHBaFHeMzA5YSa8XPsfrfFkKy+VhWlbTaAkUhSeK8SXqZyX7kgPSedLB 8qE/tu42b2rpYrQFM88o0S+MjXubmz83jWIdZ2BXemnRJAdjxRM1s9Eq1auPPP/QNtZt H4og== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="kWTNJ/qM"; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::335 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x335.google.com (mail-ot1-x335.google.com. [2607:f8b0:4864:20::335]) by gmr-mx.google.com with ESMTPS id g20si970631pfb.2.2020.05.04.10.43.16 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 10:43:16 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::335 as permitted sender) client-ip=2607:f8b0:4864:20::335; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="kWTNJ/qM"; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::335 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x335.google.com with SMTP id e20so9623731otk.12 for ; Mon, 04 May 2020 10:43:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=YhuhZcECsD3AseLykQtoQJZA5UCX9JiqiI6++LspSgA=; b=kWTNJ/qMErez8X3v5QVkwidzmPGlbvZtFWrU60/N/52vCVJ5hLvgvp+rabS3rvlgOy bwliSdReu6uWrM8yV5sZfpr39bQliWkCOFB8aL2JurbqhghwrICIw/P25Bm/PgBqoi66 buGlcZzI7bRKFE4pqVgkV7v48Gfz0v8mAmFpcFgKG3PNZWnAE6CfYXeS3ZunOUMXNbCc PRJ4UUAIMwRFOUY+9vngcXDPoDMZjlvz9+oq65m+Dbb+qO9Zuzsw6uHWt81QJ/wd0pn3 r+CSJ+DKtIDsgVSSQF3pgefiYii9oWcWQFyaJJJHdATOb7Ycon6l4GYPGwx5LDoVKpr3 Co0g== X-Gm-Message-State: AGi0PuZxXEm+Q+Z71kAGkHxFn5GosOK1AOxif45pqPN9jbaD3pmR6ApB 1PRyfRIIgA0/2q0qPwonmVzeOrnbAlUcsL9KzvoYLTXzvPOE03XtZ35vGHzhfrFVw7eShnSQANF 26Cx3/hoA2dclxQgeF1V8w/zzeiPkuMxJ0uHrf02oLADRzChfBdmwiTc/6QYlz61fPf52Tyc0e2 Lzkpl6b/rO X-Received: by 2002:a9d:7418:: with SMTP id n24mr16195753otk.54.1588614195517; Mon, 04 May 2020 10:43:15 -0700 (PDT) Return-Path: Received: from mail-ot1-f49.google.com (mail-ot1-f49.google.com. [209.85.210.49]) by smtp.gmail.com with ESMTPSA id p17sm3207798oot.17.2020.05.04.10.43.14 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 10:43:14 -0700 (PDT) Received: by mail-ot1-f49.google.com with SMTP id 72so9688097otu.1 for ; Mon, 04 May 2020 10:43:14 -0700 (PDT) X-Received: by 2002:a9d:170e:: with SMTP id i14mr15643866ota.283.1588614193860; Mon, 04 May 2020 10:43:13 -0700 (PDT) MIME-Version: 1.0 References: <14AEC162-00A7-41E5-88EF-11501EF7C2AB@gmail.com> <055F0AF8-C683-48CE-88A0-3BC9A0EEF28A@nottingham.ac.uk> In-Reply-To: <055F0AF8-C683-48CE-88A0-3BC9A0EEF28A@nottingham.ac.uk> From: Michael Shulman Date: Mon, 4 May 2020 10:43:00 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] "Identifications" ? To: Thorsten Altenkirch Cc: Steve Awodey , Stefan Monnier , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I think "identification" is a nice middle-ground between "equality" and "path/isomorphism". On the one hand it signals that something more is meant than the thing traditionally called "equality" (even though I agree with Thorsten that inside of type theory this is the thing called "equality") -- and, I think, does a good job of suggesting precisely *what* more is meant. On the other hand, it still carries the meaning that two things are *the same* (in a particular way) -- two things that have been "identified" are now "identical" -- whereas "path" and "isomorphism" suggest their traditional meanings of two things that are *not* fundamentally the same but are related in some same-like-way. On Mon, May 4, 2020 at 10:25 AM Thorsten Altenkirch wrote: > > Hi Steve, > > I remember that conversation. > I think we decided to put the question =E2=80=9Cwhat does x=3Dy mean?= =E2=80=9D aside, > until we had taken care of more important things. > > I suppose this was just a way to move on without having to reach an agree= ment. > > I think it is more than a discussion about terms. What do we mean by equa= lity? Does the equality type in HoTT is something fundamentally different? = In a way yes, because it is proof relevant so some of the old terminology d= oesn't apply anymore. That is equality of structures is a structure not a p= roposition. But nevertheless I find it confusing to call it anything but eq= uality. I would say two mathematical objects which share all the same prope= rties, which behave the same, are equal. I don't like Leibniz's "equality o= f indiscernibles" because it uses a negative. > > I noticed that many people use type theory always as something we talk ab= out. It is just a formalism. Hence the equality type just expresses an iden= tification of things which are actually different. In the real world. Howev= er, I think when we talk in type theory then this is our real world (at lea= st metaphorically) and then the metatheoretic perspective is just a confusi= on. > > Does this make sense? Sorry, I realize it is a bit philosophical but then= you are in the department of philosophy... __ > > Thorsten > > =EF=BB=BFOn 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" = wrote: > > > > > On May 4, 2020, at 12:17 PM, Thorsten Altenkirch wrote: > > > > > > I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80= =99s email account. The real Thorsten went through all this with us many ye= ars ago. > > : - ) > > > > One of our dogs gained access to my laptop - sorry. These animals c= an be very awkward. > > > > However, even the real Thorsten had a friendly argument with Andre = Joyal when we were writing the book about whether to use =3D for the equali= ty type. > > I remember that conversation. > I think we decided to put the question =E2=80=9Cwhat does x=3Dy mean?= =E2=80=9D aside, > until we had taken care of more important things. > > So is it time now? > > Steve > > > > > Thorsten > > > > On 04/05/2020, 17:08, "Steve Awodey" wrote: > > > > I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80= =99s email account. The real Thorsten went through all this with us many ye= ars ago. > > : - ) > > > > > >> On May 4, 2020, at 12:00, Michael Shulman wr= ote: > >> > >> The word "path" is closely tied to the homotopy interpretation, an= d to > >> the classical perspective of oo-groupoids presented via topologica= l > >> spaces, which has various problems. This is particularly an issue= in > >> cohesive type theory, where there is a separate "point-set level" > >> notion of path that it is important to distinguish from > >> identifications. > >> > >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier wrote: > >>> > >>>> I don't think using "identification" necessarily implies any > >>>> difference between "identification" and "equality". I don't thi= nk of > >>>> it that way. For me the point is just to have a word that refer= s to > >>>> an *element* of an identity type. Calling it "an equality" can = have > >>>> the wrong connotation because classically, an equality is just a > >>>> proposition (or a true proposition), whereas an element of an id= entity > >>>> type carries information. Calling it "an identification" sugges= ts > >>>> exactly the information that it carries: a way of identifying tw= o > >>>> things. > >>> > >>> I thought that's what "path" was for? > >>> > >>> > >>> Stefan "who really doesn't know what he's talking about" > >>> > >> > >> -- > >> 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 HomotopyT...@googlegroups.com. > >> To view this discussion on the web visit https://groups.google.com= /d/msgid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGs= D%2B2Q%40mail.gmail.com. > > > > > > > > > > This message and any attachment are intended solely for the address= ee > > and may contain confidential information. If you have received this > > message in error, please contact the sender and delete the email an= d > > attachment. > > > > Any views or opinions expressed by the author of this email do not > > necessarily reflect the views of the University of Nottingham. Emai= l > > communications with the University of Nottingham may be monitored > > where permitted by law. > > > > > > > > > > -- > > 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, s= end an email to HomotopyT...@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/= d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingha= m.ac.uk. > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > >