From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aed:3b0b:: with SMTP id p11mr12669099qte.109.1588842327060; Thu, 07 May 2020 02:05:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:620a:1237:: with SMTP id v23ls5119649qkj.11.gmail; Thu, 07 May 2020 02:05:25 -0700 (PDT) X-Received: by 2002:a05:620a:914:: with SMTP id v20mr6165483qkv.107.1588842325641; Thu, 07 May 2020 02:05:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588842325; cv=none; d=google.com; s=arc-20160816; b=w6NWW6SyzIEAo8d2Gk0pUNg3ZcKU3f6cC9SNm1W7nnzhibLiEGtOu1tCxdDyURs+Mq w8yT2ikiUml1TJFQHb12NEtJs5Sa8dQ78rxEwcXfnefDnrL8c0hnMf0BVmC8xTcnYUq3 5JvranOdRJ0KohFCxkhaMtpng34oH1cVLTxS2c2YvUAePVzVaq4IWbUwULwXbcdA6Tuh wpbUiDAlip2kP0qG/nVLoqpOORrZ9tbdRkSBw8x3HoZbtnIz/q1y7Jz2r9pHyYCnJQFz IwudPCtiRRU6KLVd033KY4VddIyXEFe0b/edUnGFAvpf4yVL9pFGAM0VieAojjT6L+VH gUeA== 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=YiyMRl8cwnV4KXXMxYxDTt47zlSLIVGebMiJlZkpVCY=; b=xVBT6N2tTWvGX+uTTs+Nk5g1IXsSKfaYQorkat+eZCbFiWgPYY+SRAvyzfvhvFTJwE 7RaEotuwc3GLN7wxINymDAhu5htGgetpvaM5iy5kHF84+dVGo2YLOvhPtqcFm63z59je r5WMlx45fwflndqz0klqFjIpMwUH3bcyTq6sr0rUoSLTOyr6ksX8YFQgyiFTLVCO98Oz ro9GYHz8Z0yUHr4HjtO4IDDzpNy9RNw33mk9ktBF9SNtaC/7SVowYppz9TxpgccbBeBD d7CFPhccrO9cpVR6iulrHO7txe9EmmSbDgQ26FPWJcomB1IeBH54tUtUfgA1nuSyA7AN uGOQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jiML48oS; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::135 as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-il1-x135.google.com (mail-il1-x135.google.com. [2607:f8b0:4864:20::135]) by gmr-mx.google.com with ESMTPS id h33si319157qtd.2.2020.05.07.02.05.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 07 May 2020 02:05:25 -0700 (PDT) Received-SPF: pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::135 as permitted sender) client-ip=2607:f8b0:4864:20::135; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jiML48oS; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::135 as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-il1-x135.google.com with SMTP id s10so2030588iln.11 for ; Thu, 07 May 2020 02:05:25 -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=YiyMRl8cwnV4KXXMxYxDTt47zlSLIVGebMiJlZkpVCY=; b=jiML48oSXFrSrCBm+fnGaZv2jCa2w+2OHk3WKGuoGnrQCuEppRbsLvqzUnNemaG12P gYpxyYgM/nS9Y0q8eha35fDrwABtFv1JaMw7cElYskQl6TNjwEcwdmnBbehAlVt14+xt PNLlQO/DFlU629TkVVfBEJTNABdAVhfkO4JhnHBX99GJYp+amUmbAJPCmNCw47PB633K WufxHu7eOd3CYphjpDg5jCEs3SAv+CkuMBmFNNoJkEEHAOM13WEjF6upbjx16LRTjMws gMVAJEBszipYnUz1lW9XSbCf8fWrLYVSJUQ25JTJHlqaSJv1/UplSlwtLghgzOdJ6KmC QiiQ== X-Gm-Message-State: AGi0PuaQ6hcaggI8+obj6qdyt4rTGfKsF/7Mhe4F9yYDZG3L6aRPV0gd M645jfCEBszUIgcryU7c0exNZcBxUH2GrLX8/sU= X-Received: by 2002:a05:6e02:111:: with SMTP id t17mr3292404ilm.59.1588842324879; Thu, 07 May 2020 02:05:24 -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> <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> In-Reply-To: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> From: =?UTF-8?Q?Ansten_M=C3=B8rch_Klev?= Date: Thu, 7 May 2020 11:04:58 +0200 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Thorsten Altenkirch Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000060edac05a50b2e25" --00000000000060edac05a50b2e25 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, Thank you for your answers and for the stimulating discussion so far. I agree that identity, to the extent that it is distinguished from equality, is more of a philosopher's concept. One could perhaps say that in mathematical logic there is an overlap of two terminological traditions: a philosophical one, in which "identity" and "equality" are distinguished, and a mathematical one, where they are not. Regarding judgemental equality/identity: if by this one understands definitional identity, then a case can be made that it is found also outside type theory. Namely, instead of saying that a and b are definitionally identical, we can also say that they are identical by definition. And this phrase, "identical by definition", could well be used by a "generic mathematician", could it not? There is also the common practice of using a special identity sign when writing definitions. One might say that the notion of definitional identity captures the semantics of this special sign. With kind regards, Ansten Klev On Thu, May 7, 2020 at 8:58 AM Thorsten Altenkirch < Thorsten....@nottingham.ac.uk> wrote: > Dear Andre, > > It seems that Egbert already gave the perfect answer. When we about Type > Theory we don't only talk about syntax but about the relation of syntax a= nd > semantics. And then judgemental equality is modelled by propositional > equality in the metatheory. Not a reversal but a level shift. > > I wouldn't say that propositional equality is a purely formal game, indee= d > we explain the nature of equality by modelling it. In a set theoretic > setting it is enough to say that equality is a congruence, i.e. an > equivalence relation that is preserved by all functions. But this is not > sufficient to explain structural equality which is not propositional. As > you know best (because you have invented many of the important notions) a > better explanation of equality is that is an omega groupoid and that all > functions are modelled as functors on these groupoids. > > Cheers, > Thorsten > > =EF=BB=BFOn 07/05/2020, 00:29, "Joyal, Andr=C3=A9" wro= te: > > 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 abou= t > 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 a= n > 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 is 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 > > On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf > of 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 > judgmental > equality. Judgmental equality is a technical object of type theo= ry > 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=E2=80=99 (and all), > > > > 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 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 mayb= e > 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 equals > b=E2=80=9D, > > - propositional equality, written maybe a \cong b, and pronunce= d > =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 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"= ). > > > > 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 > Recorde (1512-1558). > > "because no two things can be more equal than a pair of paralle= l > lines". > > It took more than a century before been universally adopted. > > Ren=C3=A9 Descartes (1596-1650) used a different symbol in his= work > (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 pos= e > 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 ha= ve > all sides equal (clearly, they cannot be identical). The axiom in the > Elements that has given rise to the term 'Euclidean relation' and which i= s > appealed 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 o= f > an equation are said to be equal, not identical, and this would become th= e > 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 Googl= e > 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/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. > > > > > > > > > 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/67E9DCCA-F9CA-45B7-9= AC8-E5A7E94FE9A9%40nottingham.ac.uk > . > --00000000000060edac05a50b2e25 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

Thank you for your answers an= d for the stimulating discussion so far. I agree that identity, to the exte= nt that it is distinguished from equality, is more of a philosopher's c= oncept. One could perhaps say that in mathematical logic there is an overla= p of two terminological traditions: a philosophical one, in which "ide= ntity" and "equality" are distinguished, and a mathematical = one, where they are not.=C2=A0

Regarding judgement= al equality/identity: if by this one understands definitional identity, the= n a case can be made that it is found also outside type theory. Namely, ins= tead of saying that a and b are definitionally identical, we can also say t= hat they are identical by definition. And this phrase, "identical by d= efinition", could well be used by a "generic mathematician",= could it not?
There is also the common practice of using a speci= al identity sign when writing definitions. One might say that the notion of= definitional identity captures the semantics of this special sign.=C2=A0

With kind regards,
Ansten Klev

On Th= u, May 7, 2020 at 8:58 AM Thorsten Altenkirch <Thorsten....@nottingham.ac.uk= > wrote:
Dear= Andre,

It seems that Egbert already gave the perfect answer. When we about Type Th= eory we don't only talk about syntax but about the relation of syntax a= nd semantics. And then judgemental equality is modelled by propositional eq= uality in the metatheory. Not a reversal but a level shift.

I wouldn't say that propositional equality is a purely formal game, ind= eed we explain the nature of equality by modelling it. In a set theoretic s= etting it is enough to say that equality is a congruence, i.e. an equivalen= ce relation that is preserved by all functions. But this is not sufficient = to explain structural equality which is not propositional. As you know best= (because you have invented many of the important notions) a better explana= tion of equality is that is an omega groupoid and that all functions are mo= delled as functors on these groupoids.

Cheers,
Thorsten

=EF=BB=BFOn 07/05/2020, 00:29, "Joyal, Andr=C3=A9" <joyal...@uqam.ca> wrote:=

=C2=A0 =C2=A0 Dear Thorsten,

=C2=A0 =C2=A0 I have naive question for experts.

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

=C2=A0 =C2=A0 Andr=C3=A9





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

=C2=A0 =C2=A0 I agree but let me try to make this more precise. We cannot t= alk about judgemental equality within Mathematics it is not a proposition. = Judgemental equality is important when we talk about Mathematics, it is a p= roperty of a mathematical text. The same applies to typing: we cannot talk = about typing because it is not a proposition it is a part of the structure = of our argument.

=C2=A0 =C2=A0 This becomes clear in the example: we talk about numbers but = x+y is an expression, hence talking about judgemental equality only makes s= ense when we talk about Mathematics. To say that x+y is not judgemental equ= al to y+x doesn't make any sense within our argument it is a sentence a= bout it.

=C2=A0 =C2=A0 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.

=C2=A0 =C2=A0 Hence clearly there is no reason to use any other word that e= quality to mean that two objects are equal which means that the equality ty= pe 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 creat= es the need to talk about elements of an equality type.=C2=A0 =C2=A0 =C2=A0= I don't like the word "identifications" because it seems to s= uggest that the two objects are not properly equal but just "identifie= d" artificially.

=C2=A0 =C2=A0 Thorsten

=C2=A0 =C2=A0 On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on beha= lf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 As I've said before, I strongly disagree th= at the standard
=C2=A0 =C2=A0 =C2=A0 =C2=A0 interpretation of "a=3Db" as meaning = "a equals b" clashes in any way
=C2=A0 =C2=A0 =C2=A0 =C2=A0 with its use to denote the identity type.=C2=A0= Almost without exception,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 whenever a mathematican working informally says= "equals", that *must*
=C2=A0 =C2=A0 =C2=A0 =C2=A0 be formalized as referring to the identity type= .=C2=A0 Ask any
=C2=A0 =C2=A0 =C2=A0 =C2=A0 mathematician on the street whether x+y=3Dy+x f= or all natural numbers x
=C2=A0 =C2=A0 =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 =C2=A0 =C2=A0 equality.=C2=A0 Judgmental equality is a techni= cal object of type theory
=C2=A0 =C2=A0 =C2=A0 =C2=A0 that the "generic mathematician" is n= ot aware of at all, so it cannot
=C2=A0 =C2=A0 =C2=A0 =C2=A0 co-opt the standard notation "=3D" or= word "equals" if we want "informal
=C2=A0 =C2=A0 =C2=A0 =C2=A0 type theory" to be at all comprehensible t= o such readers.


=C2=A0 =C2=A0 =C2=A0 =C2=A0 On Wed, May 6, 2020 at 12:01 PM Steve Awodey &l= t;awo...@cmu.edu>= ; wrote:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Dear Andre=E2=80=99 (and all),
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > The sign a =3D b is pretty well establishe= d in mathematics as meaning =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > which does indeed clash with our choice in= the book to use it for the identity type,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > and to call the elements of this type =E2= =80=9Cidentifications=E2=80=9D.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Thorsten has rightly pointed out this clas= h.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Although I am personally not eager to make= any changes in our current terminology and/or notation,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > I=E2=80=99m certainly glad to consider the= possibiiy
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > (we did agree to return to this question a= t some point, so maybe this is it : - ).
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > We need both symbols and words for two not= ions:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - judgemental equality, currently a\equiv = b,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - propositional equality, currently a =3D = b, short for Id(a,b).
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > There seems to be a proposal to revise thi= s to something like:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - judgemental equality: written a =3D b an= d pronounced =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - propositional equality, written maybe a = \cong b, and pronunced =E2=80=9Da iso b=E2=80=9D,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > (the elements of this type are called =E2= =80=9Cisos").
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Another (partial) option would be:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - judgemental equality: written a =3D b an= d pronounced =E2=80=9Ca equals b=E2=80=9D,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > - propositional equality, written Id(a,b) = and shortened somehow a ? b,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > and pronunced =E2=80=9Da idenitfied with b= =E2=80=9D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > (the elements of this type are called =E2= =80=9Cidentifications").
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Do either of these seem preferable?
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Are there other proposals?
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > And how should one decide?
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Regards,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=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 >
=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...@u= qam.ca> wrote:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Dear all,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > A few more thoughts.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > We all agree that terminology and notation= are important.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=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 =C2=A0 =C2=A0 > "because no two things can be more eq= ual than a pair of parallel lines".
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > It took more than a century before been un= iversally adopted.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Ren=C3=A9 Descartes (1596-1650) used a dif= ferent symbol=C2=A0 in his work (something like \alpha).
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > We may ask why Recorde's notation won = over Descartes's notation?
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Of course, we may never know.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > I dare to say that Recorde's notation = was *better*.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Among other things, the equality sign =3D = is symmetric:
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > the expression a=3Db and b=3Da are mirror = image of each other.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Recorde's motive for introducing the n= otation was more about
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > convenience and aesthetic than about philo= sophy and history.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > The notation was gradually adopted because= it is simple and useful.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > It was not because Recorde was a powerful = academic,
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > since he eventually died in prison.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > There is something to learn from the histo= ry of the equality sign.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > I guess that it can also applied to termin= ology.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > A new notation or terminology has a good c= hance to be adopted universally
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > if it is simple and useful, but it may tak= e time.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Andr=C3=A9
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > ________________________________
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > From: homotopyt...@googlegroups.com [homotopyt...@go= oglegroups.com] on behalf of Ansten M=C3=B8rch Klev [anste...@gmail.com]
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Sent: Tuesday, May 05, 2020 4:47 AM
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > To: HomotopyT...@googlegroups.com
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Subject: [HoTT] Identity versus equality =C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > The discussion yesterday provides a good o= ccasion for me to pose a question I have long wanted to put to this list: i= s there a convention generally agreed upon in the HoTT-community for when (= if ever) to use 'identity' instead of 'equality'?
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Here are some relevant data.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > A Germanic equivalent for 'identity= 9; is 'sameness'.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > A Germanic equivalent for 'equality= 9; is 'likeness'.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > For Aristotle equality means sameness of q= uantity. This is how one must understand 'equal' in Euclid's El= ements, where a triangle may have all sides 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 in Elements I.1 is phrased= in terms of 'equal' rather than 'identical'.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > In Diophantus's Arithmetica, on the ot= her 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, t= he sign '=3D' was introduced by Robert Recorde as a sign of equalit= y, not as a sign of identity. The explanation for this apparent discrepancy= with the Aristotelian/Euclidean terminology might be that when dealing wit= h numbers, equality just is identity, since for two numbers to be identical= as to magnitude just is for them to be the same number. Aristotle says as = much in Metaphysics M.7.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Hilbert and Bernays might be one of the fe= w logic books in the modern era to distinguish equality from identity (volu= me I, chapter 5). 'Equality' is there used for any equivalence rela= tion and glossed as the obtaining of "irgendeine Art von =C3=9Cbereins= timmung". Identity, by contrast, is "=C3=9Cbereinstimmung in jede= r Hinsicht", as expressed by indiscernibility within the given languag= e.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Frege, by contrast, explicitly identifies = (sic!) equality with identity, and glosses the latter as sameness or coinci= dence, in the first footnote to his paper on sense and reference.=C2=A0 Kle= ene and Church do the same in their famous textbooks: if one looks under &#= 39;identity' in the index to any of those books one is referred to '= ;equality'.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 > Clearly the two cannot be assumed to mean = the same by analysts who speak of two functions being identically equal! =C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=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 =C2=A0 =C2=A0 > To unsubscribe from this group and stop re= ceiving emails from it, send an email to HomotopyT...@googlegroups.com.<= br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 > To view this discussion on the web visit <= a href=3D"https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_= DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com" rel=3D"norefe= rrer" target=3D"_blank">https://groups.google.com/d/msgid/HomotopyTypeTheor= y/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com<= /a>.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=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 =C2=A0 =C2=A0 > To unsubscribe from this group and stop re= ceiving emails from it, send an email to HomotopyT...@googlegroups.com.<= br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 > To view this discussion on the web visit <= a href=3D"https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413= F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca" rel=3D"noreferrer" target= =3D"_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C74= 13F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=C2=A0 =C2=A0 =C2=A0 =C2=A0 >
=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 =C2=A0 =C2=A0 > To unsubscribe from this group and stop re= ceiving emails from it, send an email to HomotopyT...@googlegroups.com.<= br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 > To view this discussion on the web visit <= a href=3D"https://groups.google.com/d/msgid/HomotopyTypeTheory/05375057-883= F-4487-8919-2579F5771AFC%40cmu.edu" rel=3D"noreferrer" target=3D"_blank">ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/05375057-883F-4487-8919-= 2579F5771AFC%40cmu.edu.

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




=C2=A0 =C2=A0 This message and any attachment are intended solely for the a= ddressee
=C2=A0 =C2=A0 and may contain confidential information. If you have receive= d this
=C2=A0 =C2=A0 message in error, please contact the sender and delete the em= ail and
=C2=A0 =C2=A0 attachment.

=C2=A0 =C2=A0 Any views or opinions expressed by the author of this email d= o not
=C2=A0 =C2=A0 necessarily reflect the views of the University of Nottingham= . Email
=C2=A0 =C2=A0 communications with the University of Nottingham may be monit= ored
=C2=A0 =C2=A0 where permitted by law.








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.com/= d/msgid/HomotopyTypeTheory/67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9%40nottingha= m.ac.uk.
--00000000000060edac05a50b2e25--