From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:7c0f:: with SMTP id x15mr11559997pll.263.1588831877155; Wed, 06 May 2020 23:11:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:5457:: with SMTP id e23ls3598234pgm.4.gmail; Wed, 06 May 2020 23:11:15 -0700 (PDT) X-Received: by 2002:a17:90a:5648:: with SMTP id d8mr13862639pji.163.1588831875040; Wed, 06 May 2020 23:11:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588831875; cv=none; d=google.com; s=arc-20160816; b=kzd9ipDINNt2DAcXi+4N+2UxG6dYOofO4h/iaBKHS2C2Vi5gWDHCkF0K6oY5i2/uf2 RiqaX2s0kgXKTTeVnJbFtiHm1n2h4J2eOCiJU83Tgva8vQSJSLkp+Xih/n4EztmCRbsU pvNrkr4+DAvdpsiy+h1juomVW+5zIUFVLCmk+1/7FBF/y2df4HYZOBEKmg+tb7BjGRwQ umybmBbUPLrMgOTlTYgtFrKFpZQ6pyyd+zbZa4rMLAdIRfEYqJIews6UptVoaH8hMMLl Ta1PNB7PROU959ZaHf5/k1yCP2mbfAXXMhQbScgt2cASJ1Z34X5NQ+VsgsNYFcSmpFlV FJ7g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=cEP//NlplLrJZa7A2EURP6bdhaIB4Tpxh/DJ2uFLHoc=; b=vsCJE37FxP3fACeCDjv8WO3q5OxhL+ZjnBDuk9z2eJvhHNbTNLUvnUpTfAWISrSni1 sNbJDF75R3XTVDLx6X+s/WU7JSiH46VViBbI2q0erNEjFPTF2B2mQYuLr0A3CvVgkr5F QSZoyJTre+ZSRUkAIBWG+bSdBoGpA35ApbRw8Q44YI7QZDeFyw9ua0wuMscuonWb+mSQ WED9S/y1/SREp/f5c0AVl8F+3BPZnnPUhQQomLhs863rHUt1p9oMVBTST395fMp6olHk DvhcbY+igqmFYGdCSUW4bOPkGst0fjXQXQcGFiXOttylPVWZXsFDNBRQDV/htndJDqso pwEA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=hrroAdWQ; spf=pass (google.com: domain of e.m...@gmail.com designates 2607:f8b0:4864:20::e31 as permitted sender) smtp.mailfrom=e.m...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vs1-xe31.google.com (mail-vs1-xe31.google.com. [2607:f8b0:4864:20::e31]) by gmr-mx.google.com with ESMTPS id a3si309647pfr.4.2020.05.06.23.11.14 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 06 May 2020 23:11:15 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m...@gmail.com designates 2607:f8b0:4864:20::e31 as permitted sender) client-ip=2607:f8b0:4864:20::e31; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=hrroAdWQ; spf=pass (google.com: domain of e.m...@gmail.com designates 2607:f8b0:4864:20::e31 as permitted sender) smtp.mailfrom=e.m...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vs1-xe31.google.com with SMTP id s11so2650777vsm.3 for ; Wed, 06 May 2020 23:11:14 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=cEP//NlplLrJZa7A2EURP6bdhaIB4Tpxh/DJ2uFLHoc=; b=hrroAdWQ2M2x2vqr5LufMWnhQOCgdzSLCDp2eqEottEHIoPvG7z9627mF31Ag69VqY VYp/3pWtTp7tQc8fXKOioauTt0OS7KXuq1qUFwgJQXVb5a7MzD6XeVxcnzCGa7BYOotU khOe5EAA5tydDIxlq/GlHVFUS01Xs6YQ5iNddn4NfOJB6zW0M5bgLnHIEd8tl+fGDLXi HCpImLXDgK6MujK2jHleuDu7knQu46mqSOoQiZaOqCaCobUjd4A1IB2PBQzzLUVVCmXc 0uZNp3zv+lnB9WHRYW1OIwHkU4m+N9SMrnriHH8VqpJyjaVkSq6y8gx++M1uICIWq2Cv lSVw== X-Gm-Message-State: AGi0PuYLCaGzdOQ4d64LZMLVmalW+mDfr45frdwAWvpyVmDPZ6HxwgQD 7NOq06UMnJbdWDTGwjtaxxO2VmdSodZJQg0KHC4= X-Received: by 2002:a67:42c6:: with SMTP id p189mr11553159vsa.9.1588831873928; Wed, 06 May 2020 23:11:13 -0700 (PDT) MIME-Version: 1.0 References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> <952EF822-FD92-404C-A279-89502238BCDC@nottingham.ac.uk> <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> From: Egbert Rijke Date: Thu, 7 May 2020 08:11:03 +0200 Message-ID: Subject: Re: [HoTT] Identity versus equality To: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= Cc: Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="0000000000007412c805a508bf44" --0000000000007412c805a508bf44 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, Perhaps I would say that judgmental equality is even more on the semantic side than the identity type. We can reason about the identity type within type theory, but we can only reason about judgmental equality when we're considering semantics for type theory. For example, when you study dependent type theory as an essentially algebraic theory, and want to know what equalities hold in the algebras for that theory, then you're studying judgmental equality. It has been said a few times that we cannot talk about judgmental equality in mathematics, but I disagree. When we do semantics of type theory we *have to* talk about judgmental equality, and of course there is nothing that stops us from doing so. With kind regards, Egbert On Thu, May 7, 2020 at 1:29 AM Joyal, Andr=C3=A9 wrote: > Dear Thorsten, > > I have naive question for experts. > > I believe that judgemental equality is on the syntactic side of type > theory, > while propositional equality is on the semantical side. > The homotopical interpretation of type theory is mainly > concerned with propositional equality. > What is the semantic of judgemental equality? > (independantly of the semantic of propositional equality). > Could we reverse the role of the two equalities? > Could we regard judgemental equality as the true meaning > of type theory, while regarding propositional equality > as a purely formal game? > > Andr=C3=A9 > > > > > > ________________________________________ > From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk] > Sent: Wednesday, May 06, 2020 6:54 PM > To: Michael Shulman; Steve Awodey > Cc: Joyal, Andr=C3=A9; homotopyt...@googlegroups.com > Subject: Re: [HoTT] Identity versus equality > > I agree but let me try to make this more precise. We cannot talk about > judgemental equality within Mathematics it is not a proposition. > Judgemental equality is important when we talk about Mathematics, it is a > property of a mathematical text. The same applies to typing: we cannot ta= lk > about typing because it is not a proposition it is a part of the structur= e > of our argument. > > This becomes clear in the example: we talk about numbers but x+y is an > expression, hence talking about judgemental equality only makes sense whe= n > we talk about Mathematics. To say that x+y is not judgemental equal to y+= x > doesn't make any sense within our argument it is a sentence about it. > > When I say that 0+x is definitionally equal to x I don't prove anything > but I just point out a fact that follows from the definition of +. That i= s > I draw attention to it. > > Hence clearly there is no reason to use any other word that equality to > mean that two objects are equal which means that the equality type is > inhabited which is signified by using =3D. There is the issue that we may > have a more that one way in which two objects can be equal which creates > the need to talk about elements of an equality type. I don't like the > word "identifications" because it seems to suggest that the two objects a= re > not properly equal but just "identified" artificially. > > Thorsten > > =EF=BB=BFOn 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf o= f > Michael Shulman" shu...@sandiego.edu> 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 judgmen= tal > 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 "infor= mal > type theory" to be at all comprehensible to such readers. > > > On Wed, May 6, 2020 at 12:01 PM Steve Awodey wrote: > > > > Dear Andre=E2=80=99 (and all), > > > > The sign a =3D b is pretty well established in mathematics as meani= ng > =E2=80=9Ca equals b=E2=80=9D, > > which does indeed clash with our choice in the book to use it for > the identity type, > > and to call the elements of this type =E2=80=9Cidentifications=E2= =80=9D. > > Thorsten has rightly pointed out this clash. > > > > Although I am personally not eager to make any changes in our > current terminology 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 : - ). > > > > 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 =E2=80=9Ca e= quals 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"). > > > > Another (partial) option would be: > > > > - judgemental equality: written a =3D b and pronounced =E2=80=9Ca e= quals 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"). > > > > 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=C3=A9 > 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 Reco= rde > (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 wor= k > (something 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 > universally > > if it is simple and useful, but it may take time. > > > > Andr=C3=A9 > > ________________________________ > > From: homotopyt...@googlegroups.com [ > homotopyt...@googlegroups.com] on behalf 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 > > > > The discussion yesterday provides a good occasion for me to pose a > question 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' instead 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 a= ll > sides equal (clearly, they cannot be identical). The axiom in the Element= s > that has given rise to the term 'Euclidean relation' and which is appeale= d > to in 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 > equation are said to be equal, not identical, and this would become the > standard terminology in algebra. For instance, the sign '=3D' was introdu= ced > by Robert Recorde as a sign of equality, not as a sign of identity. The > explanation for this apparent discrepancy with the Aristotelian/Euclidean > terminology might be that when dealing with numbers, equality just is > identity, since for two numbers to be identical as to magnitude just is f= or > them to be the same number. Aristotle says as much in Metaphysics M.7. > > > > Hilbert and Bernays might be one of the few logic books in the > modern era to distinguish equality from identity (volume I, chapter 5). > 'Equality' is there used for any equivalence relation and glossed as the > obtaining of "irgendeine Art von =C3=9Cbereinstimmung". Identity, by cont= rast, > is "=C3=9Cbereinstimmung in jeder Hinsicht", as expressed by indiscernibi= lity > within the given language. > > > > Frege, by contrast, explicitly identifies (sic!) equality with > identity, and glosses the latter as sameness or coincidence, in the first > footnote to his paper on sense and reference. Kleene and Church do the > same in their famous textbooks: if one looks under 'identity' in the inde= x > to any of those 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 > 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/CAJHZuqYLY-_DB9uh-0F= W0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com > . > > > > -- > > 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/8C57894C7413F04A98DD= F5629FEC90B1652F515E%40Pli.gst.uqam.ca > . > > > > > > -- > > 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/05375057-883F-4487-8= 919-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, sen= d > an email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQwTR4qK094%2Bk= mgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com > . > > > > > 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. > > > > > -- > 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/8C57894C7413F04A98DD= F5629FEC90B1652F526C%40Pli.gst.uqam.ca > . > --0000000000007412c805a508bf44 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

Perhaps I would say that judg= mental equality is even more on the semantic side than the identity type. W= e can reason about the identity type within type theory, but we can only re= ason about judgmental equality when we're considering semantics for typ= e theory. For example, when you study dependent type theory as an essential= ly algebraic theory, and want to know what equalities hold in the algebras = for that theory, then you're studying judgmental equality. It has been = said a few times that we cannot talk about judgmental=C2=A0equality in math= ematics, but I disagree. When we do semantics of type theory we *have to* t= alk about judgmental equality, and of course there is nothing that stops us= from doing so.

With kind regards,
Egber= t

On Thu, May 7, 2020 at 1:29 AM Joyal, Andr=C3=A9 <joyal...@uqam.ca> wrote:
Dear Thorsten,

I have naive question for experts.

I believe that judgemental equality is on the syntactic side of type theory= ,
while propositional equality is on the semantical side.
The homotopical interpretation of type theory is mainly
concerned with propositional equality.
What is the semantic of judgemental equality?
(independantly of the semantic of propositional equality).
Could we reverse the role of the two equalities?
Could we regard judgemental equality as the true meaning
of type theory, while regarding propositional equality
as a purely formal game?

Andr=C3=A9





________________________________________
From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
Sent: Wednesday, May 06, 2020 6:54 PM
To: Michael Shulman; Steve Awodey
Cc: Joyal, Andr=C3=A9; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

I agree but let me try to make this more precise. We cannot talk about judg= emental equality within Mathematics it is not a proposition. Judgemental eq= uality is important when we talk about Mathematics, it is a property of a m= athematical text. The same applies to typing: we cannot talk about typing b= ecause it is not a proposition it is a part of the structure of our argumen= t.

This becomes clear in the example: we talk about numbers but x+y is an expr= ession, hence talking about judgemental equality only makes sense when we t= alk about Mathematics. To say that x+y is not judgemental equal to y+x does= n't make any sense within our argument it is a sentence about it.

When I say that 0+x is definitionally equal to x I don't prove anything= but I just point out a fact that follows from the definition of +. That is= I draw attention to it.

Hence clearly there is no reason to use any other word that equality to mea= n that two objects are equal which means that the equality type is inhabite= d which is signified by using =3D. There is the issue that we may have a mo= re that one way in which two objects can be equal which creates the need to= talk about elements of an equality type.=C2=A0 =C2=A0 =C2=A0I don't li= ke the word "identifications" because it seems to suggest that th= e two objects are not properly equal but just "identified" artifi= cially.

Thorsten

=EF=BB=BFOn 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf of= Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu&g= t; wrote:

=C2=A0 =C2=A0 As I've said before, I strongly disagree that the standar= d
=C2=A0 =C2=A0 interpretation of "a=3Db" as meaning "a equals= b" clashes in any way
=C2=A0 =C2=A0 with its use to denote the identity type.=C2=A0 Almost withou= t exception,
=C2=A0 =C2=A0 whenever a mathematican working informally says "equals&= quot;, that *must*
=C2=A0 =C2=A0 be formalized as referring to the identity type.=C2=A0 Ask an= y
=C2=A0 =C2=A0 mathematician on the street whether x+y=3Dy+x for all natural= numbers x
=C2=A0 =C2=A0 and y, and they will say yes.=C2=A0 But this is false if =3D = means judgmental
=C2=A0 =C2=A0 equality.=C2=A0 Judgmental equality is a technical object of = type theory
=C2=A0 =C2=A0 that the "generic mathematician" is not aware of at= all, so it cannot
=C2=A0 =C2=A0 co-opt the standard notation "=3D" or word "eq= uals" if we want "informal
=C2=A0 =C2=A0 type theory" to be at all comprehensible to such readers= .


=C2=A0 =C2=A0 On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Dear Andre=E2=80=99 (and all),
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > The sign a =3D b is pretty well established in mathemati= cs as meaning =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 > which does indeed clash with our choice in the book to u= se it for the identity type,
=C2=A0 =C2=A0 > and to call the elements of this type =E2=80=9Cidentific= ations=E2=80=9D.
=C2=A0 =C2=A0 > Thorsten has rightly pointed out this clash.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Although I am personally not eager to make any changes i= n our current terminology and/or notation,
=C2=A0 =C2=A0 > I=E2=80=99m certainly glad to consider the possibiiy
=C2=A0 =C2=A0 > (we did agree to return to this question at some point, = so maybe this is it : - ).
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > We need both symbols and words for two notions:
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > - judgemental equality, currently a\equiv b,
=C2=A0 =C2=A0 > - propositional equality, currently a =3D b, short for I= d(a,b).
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > There seems to be a proposal to revise this to something= like:
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > - judgemental equality: written a =3D b and pronounced = =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 > - propositional equality, written maybe a \cong b, and p= ronunced =E2=80=9Da iso b=E2=80=9D,
=C2=A0 =C2=A0 > (the elements of this type are called =E2=80=9Cisos"= ;).
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Another (partial) option would be:
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > - judgemental equality: written a =3D b and pronounced = =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 > - propositional equality, written Id(a,b) and shortened = somehow a ? b,
=C2=A0 =C2=A0 > and pronunced =E2=80=9Da idenitfied with b=E2=80=9D
=C2=A0 =C2=A0 > (the elements of this type are called =E2=80=9Cidentific= ations").
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Do either of these seem preferable?
=C2=A0 =C2=A0 > Are there other proposals?
=C2=A0 =C2=A0 > And how should one decide?
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Regards,
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Steve
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > On May 6, 2020, at 12:02 PM, Joyal, Andr=C3=A9 <joyal...@uqam.ca> w= rote:
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Dear all,
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > A few more thoughts.
=C2=A0 =C2=A0 > We all agree that terminology and notation are important= .
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > I love the story of the equality sign =3D introduced by = Robert Recorde (1512-1558).
=C2=A0 =C2=A0 > "because no two things can be more equal than a pai= r of parallel lines".
=C2=A0 =C2=A0 > It took more than a century before been universally adop= ted.
=C2=A0 =C2=A0 > Ren=C3=A9 Descartes (1596-1650) used a different symbol= =C2=A0 in his work (something like \alpha).
=C2=A0 =C2=A0 > We may ask why Recorde's notation won over Descartes= 's notation?
=C2=A0 =C2=A0 > Of course, we may never know.
=C2=A0 =C2=A0 > I dare to say that Recorde's notation was *better*.<= br> =C2=A0 =C2=A0 > Among other things, the equality sign =3D is symmetric:<= br> =C2=A0 =C2=A0 > the expression a=3Db and b=3Da are mirror image of each = other.
=C2=A0 =C2=A0 > Recorde's motive for introducing the notation was mo= re about
=C2=A0 =C2=A0 > convenience and aesthetic than about philosophy and hist= ory.
=C2=A0 =C2=A0 > The notation was gradually adopted because it is simple = and useful.
=C2=A0 =C2=A0 > It was not because Recorde was a powerful academic,
=C2=A0 =C2=A0 > since he eventually died in prison.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > There is something to learn from the history of the equa= lity sign.
=C2=A0 =C2=A0 > I guess that it can also applied to terminology.
=C2=A0 =C2=A0 > A new notation or terminology has a good chance to be ad= opted universally
=C2=A0 =C2=A0 > if it is simple and useful, but it may take time.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Andr=C3=A9
=C2=A0 =C2=A0 > ________________________________
=C2=A0 =C2=A0 > From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten M=C3=B8rch Klev [anste...@gmail.com]
=C2=A0 =C2=A0 > Sent: Tuesday, May 05, 2020 4:47 AM
=C2=A0 =C2=A0 > To: HomotopyT...@googlegroups.com
=C2=A0 =C2=A0 > Subject: [HoTT] Identity versus equality
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > The discussion yesterday provides a good occasion for me= to pose a question I have long wanted to put to this list: is there a conv= ention generally agreed upon in the HoTT-community for when (if ever) to us= e 'identity' instead of 'equality'?
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Here are some relevant data.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > A Germanic equivalent for 'identity' is 'sam= eness'.
=C2=A0 =C2=A0 > A Germanic equivalent for 'equality' is 'lik= eness'.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > For Aristotle equality means sameness of quantity. This = is how one must understand 'equal' in Euclid's Elements, where = a triangle may have all sides equal (clearly, they cannot be identical). Th= e axiom in the Elements that has given rise to the term 'Euclidean rela= tion' and which is appealed to in Elements I.1 is phrased in terms of &= #39;equal' rather than 'identical'.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > In Diophantus's Arithmetica, on the other hand, the = two terms of an equation are said to be equal, not identical, and this woul= d become the standard terminology in algebra. For instance, the sign '= =3D' was introduced by Robert Recorde as a sign of equality, not as a s= ign of identity. The explanation for this apparent discrepancy with the Ari= stotelian/Euclidean terminology might be that when dealing with numbers, eq= uality just is identity, since for two numbers to be identical as to magnit= ude just is for them to be the same number. Aristotle says as much in Metap= hysics M.7.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Hilbert and Bernays might be one of the few logic books = in the modern era to distinguish equality from identity (volume I, chapter = 5). 'Equality' is there used for any equivalence relation and gloss= ed as the obtaining of "irgendeine Art von =C3=9Cbereinstimmung".= Identity, by contrast, is "=C3=9Cbereinstimmung in jeder Hinsicht&quo= t;, as expressed by indiscernibility within the given language.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Frege, by contrast, explicitly identifies (sic!) equalit= y with identity, and glosses the latter as sameness or coincidence, in the = first footnote to his paper on sense and reference.=C2=A0 Kleene and Church= do the same in their famous textbooks: if one looks under 'identity= 9; in the index to any of those books one is referred to 'equality'= .
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > Clearly the two cannot be assumed to mean the same by an= alysts who speak of two functions being identically equal!
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > --
=C2=A0 =C2=A0 > You received this message because you are subscribed to = the Google Groups "Homotopy Type Theory" group.
=C2=A0 =C2=A0 > To unsubscribe from this group and stop receiving emails= from it, send an email to HomotopyT...@googlegroups.com.
=C2=A0 =C2=A0 > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY= -_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > --
=C2=A0 =C2=A0 > You received this message because you are subscribed to = the Google Groups "Homotopy Type Theory" group.
=C2=A0 =C2=A0 > To unsubscribe from this group and stop receiving emails= from it, send an email to HomotopyT...@googlegroups.com.
=C2=A0 =C2=A0 > To view this discussion on the web visit http= s://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629F= EC90B1652F515E%40Pli.gst.uqam.ca.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > --
=C2=A0 =C2=A0 > You received this message because you are subscribed to = the Google Groups "Homotopy Type Theory" group.
=C2=A0 =C2=A0 > To unsubscribe from this group and stop receiving emails= from it, send an email to HomotopyT...@googlegroups.com.
=C2=A0 =C2=A0 > To view this discussion on the web visit https://groups.g= oogle.com/d/msgid/HomotopyTypeTheory/05375057-883F-4487-8919-2579F5771AFC%4= 0cmu.edu.

=C2=A0 =C2=A0 --
=C2=A0 =C2=A0 You received this message because you are subscribed to the G= oogle Groups "Homotopy Type Theory" group.
=C2=A0 =C2=A0 To unsubscribe from this group and stop receiving emails from= it, send an email to HomotopyT...@googlegroups.com.
=C2=A0 =C2=A0 To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQwTR4qK09= 4%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.




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.




--
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 HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F526C%40Pl= i.gst.uqam.ca.
--0000000000007412c805a508bf44--