From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a92:c845:: with SMTP id b5mr9746282ilq.63.1588791712062; Wed, 06 May 2020 12:01:52 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:80a:: with SMTP id u10ls2225641ilm.9.gmail; Wed, 06 May 2020 12:01:48 -0700 (PDT) X-Received: by 2002:a92:bb01:: with SMTP id w1mr10892427ili.233.1588791708157; Wed, 06 May 2020 12:01:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588791708; cv=none; d=google.com; s=arc-20160816; b=wwabu9459Hwz6xW6slJFfBU5pUzrruiGKPfJu6oNyMn1sOcZ4NOcSKZqR/pwBcpjLr X5A+RBx5dm+ybYVAC4vkGKc6RDL/bJCTy7Y1sttul9JjLwd6AcuNQSiZIvj05AbCWnWp UxVbhOvnY/7SQS2XjchJmaDUtBaJUjjigUm8FpOEgrLu4nmL6GNOKmHzb/xjGKRMnGbL OnBQCao0wHCrim8Mb+dR6xjo+5xz2bmK8qSj5c0SMMkkkOhnaXJfbBgRk+phXibm2+0d Og1+/FuCxvXHxJgwHwNFI5/wb6YJQdR05qVIz+upicfkSRZe6I9XQagw5YU4bpjpxPB1 eYFw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature; bh=eilApby5VUQ6wEsc+C/GFtF6dSgWN/8qLk03rnCt5UI=; b=vYcxcFo4bDQ1g9igABQreaGyg7HyeKJPlZOjBT5oU+YJ1FNm1jEgtamVd8X+Lv2/Hr jYzvNG/t8vP4kNNZX1u1rEjhsSVOsGBfCKK+k4bG1VPOCkgpY7fzL8600nJUInpVBwhA /kY2YE3gP6x71G9+Zk8n1smVH7THDM9DEcXILQ08VUDWqzwzKeyl5xW+tsBsKh8kHg08 UJVEPkwWXddKI7G3XFo+ZBvh9KWanIlqWdsWAn5pbRGgd0+9xoAfauFNfHBmdtIIy/9S zwolNNvl8gVYaeC6WL79vFYvzhJaw7Sd27dyS4ZMEmsUtq9j4fgVHnAuwu7QsGJzPZrZ qzKg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="LFcK/0vh"; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::82e 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-x82e.google.com (mail-qt1-x82e.google.com. [2607:f8b0:4864:20::82e]) by gmr-mx.google.com with ESMTPS id t16si164080ilj.3.2020.05.06.12.01.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 06 May 2020 12:01:48 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::82e as permitted sender) client-ip=2607:f8b0:4864:20::82e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="LFcK/0vh"; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::82e 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-x82e.google.com with SMTP id h26so2464383qtu.8 for ; Wed, 06 May 2020 12:01:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=eilApby5VUQ6wEsc+C/GFtF6dSgWN/8qLk03rnCt5UI=; b=LFcK/0vhfXPMK8gZr174lB5rtydmGC+OgxZrmvPHSDEn2iSC6wiCoRx+Ox8KV3MPRj JMJ5pFIWLhqoyfziWMDTmcJMm/8O4jCMbYg771kM7qqVument1g+5Dp0j9aVVifZy3+Z smDvUStcUO/D9URTbYoIrNavvrUkuxcnPFyBUY/e+kTLuXeVhXF1URgC1LBPhCxOn0cJ kdCVNtXBraugIBihlVN67HCGF8GP1yT6QTiYYOgx0gZlzlqRsu4KLkZO6l0VHgRP+/PU 7y2booVAmOU86oMIogugRkOwNyj0GpxqgdV2nuSMKRG+RyLPJZPpPCjTLVaMdDce2GeF 9XKw== X-Gm-Message-State: AGi0PuZ/oK/zj8coh9TO2rkTppeUUC54fEwK19jep/oF+2dlw/TAGdXQ 9DhlPprOzsKqbbMSzodC+Ru//sNROvE= X-Received: by 2002:ac8:5645:: with SMTP id 5mr9801714qtt.151.1588791707391; Wed, 06 May 2020 12:01:47 -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 c4sm2429761qkf.120.2020.05.06.12.01.46 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 06 May 2020 12:01:47 -0700 (PDT) From: Steve Awodey Message-Id: <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_EB4CD982-1A27-402F-907D-22646DFEBAF7" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.5\)) Subject: Re: [HoTT] Identity versus equality Date: Wed, 6 May 2020 15:01:45 -0400 In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> Cc: "HomotopyT...@googlegroups.com" To: =?utf-8?B?IkpveWFsLCBBbmRyw6ki?= References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> X-Mailer: Apple Mail (2.3445.9.5) --Apple-Mail=_EB4CD982-1A27-402F-907D-22646DFEBAF7 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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,=20 which does indeed clash with our choice in the book to use it for the ident= ity type,=20 and to call the elements of this type =E2=80=9Cidentifications=E2=80=9D. = =20 Thorsten has rightly pointed out this clash. Although I am personally not eager to make any changes in our current termi= nology and/or notation,=20 I=E2=80=99m certainly glad to consider the possibiiy=20 (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,=20 - 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 pronunced =E2=80=9Da= iso b=E2=80=9D, =09(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,=20 =09and pronunced =E2=80=9Da idenitfied with b=E2=80=9D=20 =09(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: >=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 (1= 512-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 (som= ething 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 universally= =20 > if it is simple and useful, but it may take time. >=20 > 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 >=20 > The discussion yesterday provides a good occasion for me to pose a questi= on 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' inst= ead 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 u= nderstand 'equal' in Euclid's Elements, 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'.=20 >=20 > In Diophantus's Arithmetica, on the other hand, the two terms of an equat= ion are said to be equal, not identical, and this would become the standard= terminology in algebra. For instance, the sign '=3D' was introduced by Rob= ert Recorde as a sign of equality, not as a sign of identity. The explanati= on for this apparent discrepancy with the Aristotelian/Euclidean terminolog= y might be that when dealing with 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.=20 >=20 > 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 "i= rgendeine Art von =C3=9Cbereinstimmung". Identity, by contrast, is "=C3=9Cb= ereinstimmung in jeder Hinsicht", as expressed by indiscernibility within t= he given language.=20 >=20 > 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 index to any of thos= e books one is referred to 'equality'. =20 >=20 > Clearly the two cannot be assumed to mean the same by analysts who speak = of two functions being identically equal! >=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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2= A%40mail.gmail.com . >=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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqa= m.ca . --Apple-Mail=_EB4CD982-1A27-402F-907D-22646DFEBAF7 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Dear Andre=E2=80=99 (and a= ll),

The sign a =3D b i= s 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,&= nbsp;
I=E2=80=99m certainly glad to consider the possi= biiy 
(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 equalit= y, 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 somet= hing like:

- judg= emental 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,
=09(the elements of th= is 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, 
=09and pronunced =E2=80=9Da idenitfied with b=E2=80=9D=  
=09(the elements of this type are called =E2=80=9Cidentifi= cations").

= Do either of these seem preferable?
Are there other pr= oposals?
And how should one decide?

Regards,

Steve

<= /div>




On May 6, 2020, at 1= 2:02 PM, Joyal, Andr=C3=A9 <joyal...@uqam.ca> wrote:

<= div class=3D"">Dear all,

A few more thoughts.
We all agr= ee that terminology and notation are important.

I love the story of the equality sign =3D in= troduced by Robert Recorde (1512-1558).
"because no tw= o 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 (something like \alpha).
We may ask why Re= corde's notation won over Descartes's notation?
Of cou= rse, we may never know.
I dare to say that Recorde's n= otation was *better*.
Among other things, the equality= sign =3D is symmetric:
the expression = a=3Db and b=3Da are mirror image of each other.
Record= e's motive for introducing the notation was more about
=
convenience and aesthetic than about philosophy and history= .
The notation was gradually adopted be= cause it is simple and useful.
It was not because Reco= rde 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<= span class=3D"Apple-converted-space"> 
if it is simple and useful, but it may take time.

Andr=C3=A9
From: homotopyt...@googlegro= ups.com [homotopyt...@googlegroups.c= om] on behalf of Ansten M=C3=B8rch Klev [anste...@gmail.com]
Sent= : Tuesday, May 05, 20= 20 4:47 AM
To: HomotopyT...@googlegroups.com
Subjec= t: [HoTT] Identity ve= rsus equality

The discussion yesterday pro= vides a good occasion for me to pose a question I have long wante= d to put to this list: is there a convention generally agreed upon in the H= oTT-community for when (if ever) to use 'identity' instead of 'equality'?
Here are some relevant d= ata.

A Germanic e= quivalent for 'identity' is 'sameness'.
A Germanic equ= ivalent for 'equality' is 'likeness'.

<= /div>
For Aristotle equality means sameness of quantity. Thi= s is how one must understand 'equal' in Euclid's Elements, 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 whic= h is 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 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 term= inology might be that when dealing with 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. 
<= div class=3D"">
Hilbert and Bernays mig= ht 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 equiv= alence relation and glossed as the obtaining of "irgendeine Art von =C3=9Cb= ereinstimmung". Identity, by contrast, is "=C3=9Cbereinstimmung in jeder Hi= nsicht", as expressed by indiscernibility within the given language. <= /div>

Frege, by contras= t, explicitly identifies (sic!) equality with identity, and glosses the lat= ter as sameness or coincidence, in the first footnote to his paper on sense= and reference.  Kleene and Church do the same in their famous textboo= ks: if one looks under 'identity' in the index to any of those books one is= referred to 'equality'.  

Clearly the two cannot be assumed to mean the same by a= nalysts who speak of two functions being identically equal!

-- 
You received this message= because you are subscribed to the Google Groups "Homotopy Type Theory" gro= up.
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/Homot= opyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mai= l.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 receivi= ng emails from it, send an email to&n= bsp;HomotopyT...@googlegroups.com.
To view this discu= ssion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC9= 0B1652F515E%40Pli.gst.uqam.ca.
--Apple-Mail=_EB4CD982-1A27-402F-907D-22646DFEBAF7--