From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:4c1d:: with SMTP id z29mr8310499pga.243.1588797061591; Wed, 06 May 2020 13:31:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:54:: with SMTP id 81ls2770729pfa.10.gmail; Wed, 06 May 2020 13:30:59 -0700 (PDT) X-Received: by 2002:a63:1161:: with SMTP id 33mr8922135pgr.313.1588797059651; Wed, 06 May 2020 13:30:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588797059; cv=none; d=google.com; s=arc-20160816; b=M3sJlHmF2HzZsbWK7PlYJDnkNyoO809olumWLQbftPwrVYYJIT8tZuME7H1rhBItqc 3qnadB67ejYAh6xpvTDavX6FhwO+UWlpMqU6kRrczHyMdJDCURwwwWx9yg3zuENEdPCU jjBV6oTSEJSyeQ8ct5k+8Fys3eiNg7pqdyQDwbkuj44yLxGKhbmAVdvy/AandMbW36Ii eSpl7RD64lkfKEYOStpCmKcHLVmUlXYtW78Q6+WvGzjTUX3l6nEV6uunWjtUUL+/+DIJ MtLolXOr1GHhjp1plR3qS6e9Yn37tLmkyl9zMGug+GKjVnstMO38ggGYV83JsVdtqp5T q85Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=wNarMCDdPDF6f6gCxosceEbfX7V3E4lPI2BqY6+sHYE=; b=UrddUfIIlApAIXxVEe7yf7zSiEq2+ocETXasmX56v1aBnm4oR02r4OUdbVpGXolO4P o04FQkNZDEs5RUDbIsVrx8DScSMPj7E6uXnBDUdVckP57j7zJ3+1RxsVKggpZdito0CR 6HsT7VchUsLs9O2WIc1t+dIhQvgHGBZyiXvDcMq/U6AG0VGTy6ZQnO8BL0XIFuwuWqg+ iAGot3P0MlKdDmH/zbkyIdBOZR2WXdAlam2APwvMWvAeDeIH6ollwjYKHub7gVJDCJ4F l/sEYzb7FTuCdumx+B92ZVQo8V5gxjXBMvWJSe/x4nHqJnYwKB+sf+J0I/UQRWCypTiq nKsA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id gn24si819655pjb.2.2020.05.06.13.30.59 for ; Wed, 06 May 2020 13:30:59 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: 947dPQqaY9fBpeGyt2ioOdYpmNb6BMw7XLCvZi9Vf4N4WKibhIz0FS5K9I+dP3P+y3KkwwYC3L tEe4rwWcsr9gRvf6Ai05IFun6m7wwSB5zzI7HQ0j+Iv0gwNaWDWqizqMY1hEvwapmJ//fZEpoA kpt7VQsJgaKjyoIT0GxLV+QdSdjMf0Bz93NtshIGI+YzY7PHVDFwpVFdIZKUYa3R01333ppJcG jfEV5YUtnIPU/2lk5oIn8sZR5rbaX5sZ1oseFZBnEP2BTdeIqBCT39jI7AgQzD/rv5YNIWGK+J dIQ= X-IronPort-AV: E=Sophos;i="5.73,360,1583211600"; d="scan'208";a="10320174" Received: from unknown (HELO Lettre.gst.uqam.ca) ([132.208.216.71]) by mail6.uqam.ca with ESMTP; 06 May 2020 16:30:58 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Lettre.gst.uqam.ca ([169.254.6.239]) with mapi id 14.03.0439.000; Wed, 6 May 2020 16:30:57 -0400 From: =?Windows-1252?Q?Joyal=2C_Andr=E9?= To: Steve Awodey , Michael Shulman CC: "HomotopyT...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAA4SA///BbXI= Date: Wed, 6 May 2020 20:30:57 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F51F0@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> ,<35D53A79-56C0-42F7-A58F-6052CE26FA87@cmu.edu> In-Reply-To: <35D53A79-56C0-42F7-A58F-6052CE26FA87@cmu.edu> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Steve and Mike, Thank you for your reply. I guess we essentially agree. The idea that the equality relation a=3Db depends on a choice of identifica= tion of a with b is fundamental. In a sense, it has been around since a long time, but not formally recogniz= ed except in ML type theory and possibly in category theory. I am dreaming of a formal system in which the identity type Id(a,b) is so natural, that it disappear by not been problematic. How could we teach homotopy type theory to engineers? Andr=E9 ________________________________________ From: Steve Awodey [awo...@cmu.edu] Sent: Wednesday, May 06, 2020 3:31 PM To: Michael Shulman Cc: Joyal, Andr=E9; HomotopyT...@googlegroups.com Subject: Re: [HoTT] Identity versus equality I totally agree with you, Mike. But I think Thorsten was pointing out (he will correct me if I=92m wrong) that a =3D b meaning =93equals=94 is maybe not the same as =93identity=94? and I do think that the terminology =93identification=94 is good for the el= ements of this type, which traditionally was called the =93identity type". maybe the answer is to say that mathematics simply doesn=92t deal with the = =93metaphysical" notion of =93identity=94, as distinct from equality. we just use both words interchangeably for the single notion expressd by a = =3D b, which is short for Id(a,b). > On May 6, 2020, at 3:18 PM, Michael Shulman wrote: > > As I've said before, I strongly disagree that the standard > interpretation of "a=3Db" as meaning "a equals b" clashes in any way > with its use to denote the identity type. Almost without exception, > whenever a mathematican working informally says "equals", that *must* > be formalized as referring to the identity type. Ask any > mathematician on the street whether x+y=3Dy+x for all natural numbers x > and y, and they will say yes. But this is false if =3D means judgmental > equality. Judgmental equality is a technical object of type theory > that the "generic mathematician" is not aware of at all, so it cannot > co-opt the standard notation "=3D" or word "equals" if we want "informal > type theory" to be at all comprehensible to such readers. > > > On Wed, May 6, 2020 at 12:01 PM Steve Awodey wrote: >> >> Dear Andre=92 (and all), >> >> The sign a =3D b is pretty well established in mathematics as meaning = =93a equals b=94, >> which does indeed clash with our choice in the book to use it for the id= entity type, >> and to call the elements of this type =93identifications=94. >> Thorsten has rightly pointed out this clash. >> >> Although I am personally not eager to make any changes in our current te= rminology and/or notation, >> I=92m certainly glad to consider the possibiiy >> (we did agree to return to this question at some point, so maybe this is= it : - ). >> >> We need both symbols and words for two notions: >> >> - judgemental equality, currently a\equiv b, >> - propositional equality, currently a =3D b, short for Id(a,b). >> >> There seems to be a proposal to revise this to something like: >> >> - judgemental equality: written a =3D b and pronounced =93a equals b=94, >> - propositional equality, written maybe a \cong b, and pronunced =94a is= o b=94, >> (the elements of this type are called =93isos"). >> >> Another (partial) option would be: >> >> - judgemental equality: written a =3D b and pronounced =93a equals b=94, >> - propositional equality, written Id(a,b) and shortened somehow a ? b, >> and pronunced =94a idenitfied with b=94 >> (the elements of this type are called =93identifications"). >> >> Do either of these seem preferable? >> Are there other proposals? >> And how should one decide? >> >> Regards, >> >> Steve >> >> >> >> >> >> On May 6, 2020, at 12:02 PM, Joyal, Andr=E9 wrote: >> >> Dear all, >> >> A few more thoughts. >> We all agree that terminology and notation are important. >> >> I love the story of the equality sign =3D introduced by Robert Recorde (= 1512-1558). >> "because no two things can be more equal than a pair of parallel lines". >> It took more than a century before been universally adopted. >> Ren=E9 Descartes (1596-1650) used a different symbol in his work (somet= hing like \alpha). >> We may ask why Recorde's notation won over Descartes's notation? >> Of course, we may never know. >> I dare to say that Recorde's notation was *better*. >> Among other things, the equality sign =3D is symmetric: >> the expression a=3Db and b=3Da are mirror image of each other. >> Recorde's motive for introducing the notation was more about >> convenience and aesthetic than about philosophy and history. >> The notation was gradually adopted because it is simple and useful. >> It was not because Recorde was a powerful academic, >> since he eventually died in prison. >> >> There is something to learn from the history of the equality sign. >> I guess that it can also applied to terminology. >> A new notation or terminology has a good chance to be adopted universall= y >> if it is simple and useful, but it may take time. >> >> Andr=E9 >> ________________________________ >> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on b= ehalf of Ansten M=F8rch Klev [anste...@gmail.com] >> Sent: Tuesday, May 05, 2020 4:47 AM >> To: HomotopyT...@googlegroups.com >> Subject: [HoTT] Identity versus equality >> >> The discussion yesterday provides a good occasion for me to pose a quest= ion I have long wanted to put to this list: is there a convention generally= agreed upon in the HoTT-community for when (if ever) to use 'identity' ins= tead of 'equality'? >> >> Here are some relevant data. >> >> A Germanic equivalent for 'identity' is 'sameness'. >> A Germanic equivalent for 'equality' is 'likeness'. >> >> For Aristotle equality means sameness of quantity. This is how one must = understand 'equal' in Euclid's Elements, where a triangle may have all side= s equal (clearly, they cannot be identical). The axiom in the Elements that= has given rise to the term 'Euclidean relation' and which is appealed to i= n Elements I.1 is phrased in terms of 'equal' rather than 'identical'. >> >> In Diophantus's Arithmetica, on the other hand, the two terms of an equa= tion are said to be equal, not identical, and this would become the standar= d terminology in algebra. For instance, the sign '=3D' was introduced by Ro= bert Recorde as a sign of equality, not as a sign of identity. The explanat= ion for this apparent discrepancy with the Aristotelian/Euclidean terminolo= gy might be that when dealing with numbers, equality just is identity, sinc= e for two numbers to be identical as to magnitude just is for them to be th= e same number. Aristotle says as much in Metaphysics M.7. >> >> Hilbert and Bernays might be one of the few logic books in the modern er= a to distinguish equality from identity (volume I, chapter 5). 'Equality' i= s there used for any equivalence relation and glossed as the obtaining of "= irgendeine Art von =DCbereinstimmung". Identity, by contrast, is "=DCberein= stimmung in jeder Hinsicht", as expressed by indiscernibility within the gi= ven language. >> >> Frege, by contrast, explicitly identifies (sic!) equality with identity,= and glosses the latter as sameness or coincidence, in the first footnote t= o his paper on sense and reference. Kleene and Church do the same in their= famous textbooks: if one looks under 'identity' in the index to any of tho= se books one is referred to 'equality'. >> >> Clearly the two cannot be assumed to mean the same by analysts who speak= of two functions being identically equal! >> >> -- >> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN= 2A%40mail.gmail.com. >> >> -- >> 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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uq= am.ca. >> >> >> -- >> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu. > > -- > 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/msgi= d/HomotopyTypeTheory/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPe= f3w%40mail.gmail.com.