From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aca:3344:: with SMTP id z65mr10069002oiz.95.1588614919412; Mon, 04 May 2020 10:55:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a4a:2f4d:: with SMTP id p74ls754405oop.1.gmail; Mon, 04 May 2020 10:55:17 -0700 (PDT) X-Received: by 2002:a4a:ba95:: with SMTP id d21mr15976595oop.19.1588614917852; Mon, 04 May 2020 10:55:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588614917; cv=none; d=google.com; s=arc-20160816; b=Tzq93mZRoBkuW6g11lMcJYaClikrXtakmbbyWGC0tZ3+LO/yFG8UJbXKfCaatdqmMj 8q9RMPkuKU2dhdfpS0vQhRWFj29cjCL96uzj7Kk1naeD8ABeNROfFhZPRSyEkXzDA7fq 0kp6KS/NwZ6Kccsg2RcPgdhmGySjvS2rHB8z0EfgJIcrocjX6Z1Qzt4A/HHCn1UlXlez kgKmpr0IxVENaPCdpgtleGN3lTDbFJXW/KbRLGXtRUYR7Z9oIQHZ0IkSqJqUX7df12Hj /89d8uMVbJ1uQnKKdMadue5dWQACywQ1NnP3ozxY5SjgsO5VL+Ob6khlo7CR3sgC8VF2 ueGg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=yJ8dq/Ny1VYe6ItYQR5HmMpLGpMQ5zwP9yw/jRsDi5o=; b=lSRihxUZkmu6ps0NbaXQa7U0tUQrfW2CbVnrx3Skil7DGO58Kx1/CIeFK3tUphNAW3 m8lFt6PVZ8dn781fnVTOXdOJcPDyoSh091T91Rp1+lQOyuUvSAhvkOI6+d/TXdC+ntbj 1VfcNG6D0X6N+7nOXsgNCgTfT3NFxrzPzNfAFAgbNEu66eZPXdumW8H1yebDcwnpMRbY 190bmdvZgjWCuTmIqH4x/S40Fvse89wS9zsX6weGPdOQ7QPKwqRZWKvccC1OvjiCz9c6 zmNC4O1W8JaOrkN+fhiPI6T6BTxofCCM30PWNwMuGlbcdS3OGT4pPxWVWwONX4PMlwIu zFFg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=qL5f4RBj; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qt1-x835.google.com (mail-qt1-x835.google.com. [2607:f8b0:4864:20::835]) by gmr-mx.google.com with ESMTPS id w196si555127oif.4.2020.05.04.10.55.17 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 10:55:17 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) client-ip=2607:f8b0:4864:20::835; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=qL5f4RBj; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qt1-x835.google.com with SMTP id z90so223806qtd.10 for ; Mon, 04 May 2020 10:55:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=yJ8dq/Ny1VYe6ItYQR5HmMpLGpMQ5zwP9yw/jRsDi5o=; b=qL5f4RBjuLgxk62vLownAhe1BYReEVKOUTchC2S+N5XVE2eWks3lsZjcWmI+TbnNfO +0KMAPm9O9XDA1rcYjTUnabITgJqzSOnZQ4hKIDdNYMXo6zpHOVrL6T5PwdZVwLlPkPL fH7LAVnM00RO48X4SRqdMjTS+xwPkTj0AX0Dy2uTavHJipnZwFlqUpo73UIlLggXWMK1 SP5YvzxdAhIGjDrrCGa4cs9VS2crn/LFooUg2oMRQUWearR+v7uQuLV2oBnmEq6iqX67 11dUxhkjT9zMFxbN3hu7Y4NoAIgmFHto4yoiL72UrajGwoxkMgmT9aqToRFOUthvX+w7 y78w== X-Gm-Message-State: AGi0PuZfiFdZh7Yo2oIEL0jtWXTZJuSj/FaGz7wFJq9f0/pEX1laWbv0 GGPFUC1kZm2PeJ+yyO9a9zLECw== X-Received: by 2002:ac8:6c24:: with SMTP id k4mr257135qtu.257.1588614917181; Mon, 04 May 2020 10:55:17 -0700 (PDT) Return-Path: Received: from [192.168.1.13] (pool-74-111-173-45.pitbpa.fios.verizon.net. [74.111.173.45]) by smtp.gmail.com with ESMTPSA id w18sm10556994qkw.113.2020.05.04.10.55.16 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 10:55:16 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.5\)) Subject: Re: [HoTT] "Identifications" ? From: Steve Awodey In-Reply-To: <055F0AF8-C683-48CE-88A0-3BC9A0EEF28A@nottingham.ac.uk> Date: Mon, 4 May 2020 13:55:15 -0400 Cc: Michael Shulman , Stefan Monnier , "homotopyt...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <4657A23E-2B56-4A87-8CF3-A3A1159BA044@cmu.edu> References: <14AEC162-00A7-41E5-88EF-11501EF7C2AB@gmail.com> <055F0AF8-C683-48CE-88A0-3BC9A0EEF28A@nottingham.ac.uk> To: Thorsten Altenkirch X-Mailer: Apple Mail (2.3445.9.5) > On May 4, 2020, at 1:25 PM, Thorsten Altenkirch wrote: >=20 > Hi Steve, >=20 > 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. >=20 > I suppose this was just a way to move on without having to reach an agree= ment. yup >=20 > 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. you seem to prefer the term =E2=80=9Cequality=E2=80=9D over =E2=80=9Cidenti= ty=E2=80=9D - even when (mis)quoting Leibniz! maybe that=E2=80=99s part of the problem: if we talk about =E2=80=9Cidentit= y types=E2=80=9D instead of =E2=80=9Cequality types=E2=80=9D then it=E2=80= =99s easier to regard them as structures,=20 the inhabitants of which are =E2=80=9Cidentifications=E2=80=9D, rather than= =E2=80=9Cequality proofs=E2=80=9D (which introduces an unwanted meta-persp= ective). Frege once considered equality as a relation between symbols, rather than w= hat they denote =E2=80=94 he later rejected that view, but I don=E2=80=99t = think it's so bad. =20 Definitional equality can be thought of like this =E2=80=94 it=E2=80=99s a = meta-statement about (pseudo-) syntactic things. The relation that we can reason about inside the system is called *identity= *, and it=E2=80=99s a "proof relevant=E2=80=9D relation=20 =E2=80=94 or better put, it=E2=80=99s a proper structure, not a mere propos= ition =E2=80=94=20 its elements are identifications, and these we know admit an oo-groupoid st= ructure.=20 >=20 > Does this make sense? Sorry, I realize it is a bit philosophical but then= you are in the department of philosophy=E2=80=A6 __ to my everlasting regret =E2=80=94 and thanks for not calling me a philosop= her! Steve >=20 > Thorsten >=20 > =EF=BB=BFOn 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" = wrote: >=20 >=20 >=20 >> On May 4, 2020, at 12:17 PM, Thorsten Altenkirch wrote: >>=20 >>=20 >> I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s ema= il account. The real Thorsten went through all this with us many years ago.= =20 >> : - ) >>=20 >> One of our dogs gained access to my laptop - sorry. These animals can be= very awkward. >>=20 >> 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 equality ty= pe.=20 >=20 > I remember that conversation.=20 > I think we decided to put the question =E2=80=9Cwhat does x=3Dy mean?= =E2=80=9D aside,=20 > until we had taken care of more important things. >=20 > So is it time now? >=20 > Steve >=20 >>=20 >> Thorsten >>=20 >> On 04/05/2020, 17:08, "Steve Awodey" wrote: >>=20 >> I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s ema= il account. The real Thorsten went through all this with us many years ago.= =20 >> : - ) >>=20 >>=20 >>> On May 4, 2020, at 12:00, Michael Shulman wrote: >>>=20 >>> The word "path" is closely tied to the homotopy interpretation, and to >>> the classical perspective of oo-groupoids presented via topological >>> 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. >>>=20 >>>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier wrote: >>>>=20 >>>>> I don't think using "identification" necessarily implies any >>>>> difference between "identification" and "equality". I don't think of >>>>> it that way. For me the point is just to have a word that refers 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 identit= y >>>>> type carries information. Calling it "an identification" suggests >>>>> exactly the information that it carries: a way of identifying two >>>>> things. >>>>=20 >>>> I thought that's what "path" was for? >>>>=20 >>>>=20 >>>> Stefan "who really doesn't know what he's talking about" >>>>=20 >>>=20 >>> --=20 >>> You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2= Q%40mail.gmail.com. >>=20 >>=20 >>=20 >>=20 >> 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.=20 >>=20 >> 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=20 >> where permitted by law. >>=20 >>=20 >>=20 >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyT...@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.= uk. >=20 >=20 >=20 >=20 >=20 > 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.=20 >=20 > 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=20 > where permitted by law. >=20 >=20 >=20 >=20