From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90a:730a:: with SMTP id m10mr11791840pjk.9.1588793475775; Wed, 06 May 2020 12:31:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:ac91:: with SMTP id h17ls3902463plr.3.gmail; Wed, 06 May 2020 12:31:14 -0700 (PDT) X-Received: by 2002:a17:902:8205:: with SMTP id x5mr10214559pln.82.1588793473929; Wed, 06 May 2020 12:31:13 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588793473; cv=none; d=google.com; s=arc-20160816; b=Hq6jXTjevdW0oGR/icdkVS1XLV42nXtVgQ9wRuoRkNcNc0TiiJDZ7DbQwcztt/rcyk mKhs65c2Y2JJnP9W3y+R9z3FnjYhiy+5lNa4cxKxrJSHnpv1HMAVCAsSeGiVS3dOkUht naSaJoSuTmivECwY9lvdtSSs6OBMeE3jfM2PwJjrn06PZJzaYxeY8ciHTKh5YzfpkEoG DnMpy+LRU2TTDuKcgvOxQsogTwx/8+LLH/2V4kU13h5m4ZV3ZKTxctTCtLtR6XER1AS6 fWF3TjBSCGQOJ7VMGpaSg/jjeM5JTNbPU5DOBuGkp4pADbFjtPfaNs13NWo8fUeQ3OnS MoKw== 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=dwVRZzszVQUxMpUeoQBW/HZ6BSJQSkbZhlxSIxLT7zU=; b=JROCht7vgY01gVJVBwFMW73sJ7DkL2nT94dNd+rvXS/gtprJj7Mve5CZeZVwvzt+QB nsBZAmQ3/ltszpjI2/Sjoca9Brml+tgGhiNuw7sH5NDje9+L/ePFH9FYPrVLO5VQug7G urdonTQsuV5//Ur+sK/fXBVh2nufHmqrkiNLf3pLlyA49BdJ8Mu4KYaKVODssvwsY+zB eUnERe0xBUHxDoD0U6aD4+qu7U1Sh/bkV079GJR9iGdpQm1+EUGXmhK0eYA31izM9T77 a7TyELyolGU83xmwJKaCJh2IA5wcqCS7xArvfcR0aGu6onpgsi58exS1nWu1vhjpg6Eo bszg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=vu6yozmX; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::832 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-x832.google.com (mail-qt1-x832.google.com. [2607:f8b0:4864:20::832]) by gmr-mx.google.com with ESMTPS id g23si108872pgi.5.2020.05.06.12.31.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 06 May 2020 12:31:13 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::832 as permitted sender) client-ip=2607:f8b0:4864:20::832; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=vu6yozmX; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::832 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-x832.google.com with SMTP id h26so2558818qtu.8 for ; Wed, 06 May 2020 12:31:13 -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=dwVRZzszVQUxMpUeoQBW/HZ6BSJQSkbZhlxSIxLT7zU=; b=vu6yozmX7daxvLr7zJv4csMXqAL1XYNTbwfzESRm6LyTQsDhRYc2ZGjLN35xINU0ZS WBTPbNBb61zzHmI6s6dUSQ2YwYW/+xKkxySTItcUVTGs+SZ30VRQuawNV/J7bfnX4Unm w2YMFf2ppJw4Hn6iP4r/5nsEGSvSkGgGQGVhBXj+fydJlvlfn5tsEx9iz+z8iU7zEVOt zpQZPL7LgI4vlig6xipGHIl8uiFV3r5lCg/fZm1ZqV9IwLwHn6A/49Vm579WwDMospTp EFPek8p/QZzU7PlWvWwbMC4BBQSL8mjHLY6BqM0k1EaZwhdQVx7ptOgjF19C/zjZrOeY VdzA== X-Gm-Message-State: AGi0PuaOur7/rL8WtzF/ommZA9MU4MWJ1KTNbOEjjrl/E+EqXGAjRZKd Ele+jFpwDInE3XxsQhj4zA7Ajg== X-Received: by 2002:aed:3ac3:: with SMTP id o61mr1594359qte.132.1588793472891; Wed, 06 May 2020 12:31:12 -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 h13sm2358921qti.32.2020.05.06.12.31.12 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 06 May 2020 12:31:12 -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] Identity versus equality From: Steve Awodey In-Reply-To: Date: Wed, 6 May 2020 15:31:11 -0400 Cc: =?utf-8?B?IkpveWFsLCBBbmRyw6ki?= , "HomotopyT...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <35D53A79-56C0-42F7-A58F-6052CE26FA87@cmu.edu> References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> To: Michael Shulman X-Mailer: Apple Mail (2.3445.9.5) I totally agree with you, Mike. But I think Thorsten was pointing out (he will correct me if I=E2=80=99m wr= ong)=20 that a =3D b meaning =E2=80=9Cequals=E2=80=9D is maybe not the same as =E2= =80=9Cidentity=E2=80=9D? and I do think that the terminology =E2=80=9Cidentification=E2=80=9D is goo= d for the elements of this type, which traditionally was called the =E2=80= =9Cidentity type". maybe the answer is to say that mathematics simply doesn=E2=80=99t deal wit= h the =E2=80=9Cmetaphysical" notion of =E2=80=9Cidentity=E2=80=9D, as disti= nct 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: >=20 > 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. >=20 >=20 > On Wed, May 6, 2020 at 12:01 PM Steve Awodey wrote: >>=20 >> Dear Andre=E2=80=99 (and all), >>=20 >> The sign a =3D b is pretty well established in mathematics as meaning = =E2=80=9Ca equals b=E2=80=9D, >> 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 =E2=80=9Cidentifications=E2=80=9D. >> Thorsten has rightly pointed out this clash. >>=20 >> Although I am personally not eager to make any changes in our current te= rminology and/or notation, >> I=E2=80=99m certainly glad to consider the possibiiy >> (we did agree to return to this question at some point, so maybe this is= it : - ). >>=20 >> We need both symbols and words for two notions: >>=20 >> - judgemental equality, currently a\equiv b, >> - propositional equality, currently a =3D b, short for Id(a,b). >>=20 >> There seems to be a proposal to revise this to something like: >>=20 >> - judgemental equality: written a =3D b and pronounced =E2=80=9Ca equals= b=E2=80=9D, >> - propositional equality, written maybe a \cong b, and pronunced =E2=80= =9Da iso b=E2=80=9D, >> (the elements of this type are called =E2=80=9Cisos"). >>=20 >> Another (partial) option would be: >>=20 >> - judgemental equality: written a =3D b and pronounced =E2=80=9Ca equals= b=E2=80=9D, >> - propositional equality, written Id(a,b) and shortened somehow a ? b, >> and pronunced =E2=80=9Da idenitfied with b=E2=80=9D >> (the elements of this type are called =E2=80=9Cidentifications"). >>=20 >> Do either of these seem preferable? >> Are there other proposals? >> And how should one decide? >>=20 >> Regards, >>=20 >> Steve >>=20 >>=20 >>=20 >>=20 >>=20 >> On May 6, 2020, at 12:02 PM, Joyal, Andr=C3=A9 wrote: >>=20 >> Dear all, >>=20 >> A few more thoughts. >> We all agree that terminology and notation are important. >>=20 >> 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=C3=A9 Descartes (1596-1650) used a different symbol in his work (so= mething 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. >>=20 >> 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. >>=20 >> Andr=C3=A9 >> ________________________________ >> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on b= ehalf of Ansten M=C3=B8rch Klev [anste...@gmail.com] >> Sent: Tuesday, May 05, 2020 4:47 AM >> To: HomotopyT...@googlegroups.com >> Subject: [HoTT] Identity versus equality >>=20 >> 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'? >>=20 >> Here are some relevant data. >>=20 >> A Germanic equivalent for 'identity' is 'sameness'. >> A Germanic equivalent for 'equality' is 'likeness'. >>=20 >> 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'. >>=20 >> 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. >>=20 >> 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 =C3=9Cbereinstimmung". Identity, by contrast, is "=C3=9C= bereinstimmung in jeder Hinsicht", as expressed by indiscernibility within = the given language. >>=20 >> 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'. >>=20 >> Clearly the two cannot be assumed to mean the same by analysts who speak= of two functions being identically equal! >>=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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN= 2A%40mail.gmail.com. >>=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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uq= am.ca. >>=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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu. >=20 > --=20 > 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.