From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a92:cd01:: with SMTP id z1mr9199891iln.182.1588780951430; Wed, 06 May 2020 09:02:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:6a2a:: with SMTP id l42ls777391jac.8.gmail; Wed, 06 May 2020 09:02:30 -0700 (PDT) X-Received: by 2002:a02:9a0d:: with SMTP id b13mr9025420jal.60.1588780949909; Wed, 06 May 2020 09:02:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588780949; cv=none; d=google.com; s=arc-20160816; b=W3kI4eGToFgq8NjCkoE7otVNRgksd573ujnt4Bi/eTcBw31uaYcoTZLBWw7Xsi91x+ EZiDYer/JLkg2CCiich78LcxcHHVQcxygfvHmtZ07MaJ4DDhMhY1xA7HQBFAgamorjpT qmDYryV2kjjCyxdr2LfaQ/Utmrwn28W7vB4cfFK3CVv39BNcAg3X58MVtZwywiIYRRzB 2oPsQtGpHe4q+GQYNGLhry+3JSnp3BifWTABu+M/eGo81nmbeDh5QSXDqNt/VcrYp6sl JMsg4ELOtshmiEtnjn7Hlp3+s9rB7oVmBvn09ZdI7R5jIrK8m25UFd0w3C/REYi8+pBt DItg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from:ironport-sdr; bh=JKoT8C5hWCtAIT2iHH4wXL0B4P+qZVMUBrjQXy3D4Kg=; b=qq5O15Mi0qcaroA9dhiywseRo/XC82i1pRVPSn9hk7fF9LvEdanjZS9U1hdMcCBTxY BwEPxWMBU6PIMJD5e+9hXJlVEsG0rYdku5U+7L4W26a4TvefNICz2vb8CqDjsz//no1v XoeBoGCb50XUzPvYuc6ssWcjXqywGNJrWftdYGBQAo0Nr44kgb79DBs3O8V67F3Oes7v cTqeCtup619Ylc4p7T8f6JjFL8IogV4hUcZZfSurX9n44vn4ycf6nPJdtuS/eWgpU5ul /I//BN69ApVIuMmW42FAdOaiSMP92wJJE9dL71BeqYlo2aF0Qo/uAg1TDMzYgdy8x5O1 qLaA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail5.uqam.ca (vra-uqam.uqam.ca. [132.208.246.108]) by gmr-mx.google.com with ESMTP id t16si129226ilj.3.2020.05.06.09.02.29 for ; Wed, 06 May 2020 09:02:29 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) client-ip=132.208.246.108; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: XuB6kWCUGhrf+81euo6V+iVdWkYRrHrul8WN4Ms3QiydarVxXxQ+wIKBj6+Z7jLrUGuSqRkZQC nfqC+fjFaWJ1ZdRW7COP4uOTtusSot3D7lnvHhZ1zqHK8hMrMQLLH8x6dffRwiZx+0IB4q22JW YCUQrFW2f9FTWjdq6oX+UxC5ws4NFXde58+Tyy3pHsmJzunEV3DljBYwOdX6my88ZoZfVyfoZb rFT2DLPK9XX+GJ9ByyQvsGAHqcMSgqSloiU+M9hHokcTQrE3skwzFMf9so/O45t67W3QcaQmfh nao= X-IronPort-AV: E=Sophos;i="5.73,359,1583211600"; d="scan'208,217";a="11614980" Received: from unknown (HELO Avis.gst.uqam.ca) ([132.208.216.75]) by mail7.uqam.ca with ESMTP; 06 May 2020 12:02:29 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Avis.gst.uqam.ca ([169.254.2.247]) with mapi id 14.03.0439.000; Wed, 6 May 2020 12:02:28 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: =?iso-8859-1?Q?Ansten_M=F8rch_Klev?= , "HomotopyT...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGO Date: Wed, 6 May 2020 16:02:27 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> References: In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B1652F515EPligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B1652F515EPligstuqamca_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable 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 (151= 2-1558). "because no two things can be more equal than a pair of parallel lines". It took more than a century before been universally adopted. Ren=E9 Descartes (1596-1650) used a different symbol in his work (somethin= g 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=E9 ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Ansten M=F8rch Klev [anste...@gmail.com] Sent: Tuesday, May 05, 2020 4:47 AM To: HomotopyT...@googlegroups.com Subject: [HoTT] Identity versus equality The discussion yesterday provides a good occasion for me to pose a question= I have long wanted to put to this list: is there a convention generally ag= reed upon in the HoTT-community for when (if ever) to use 'identity' instea= d 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 und= erstand 'equal' in Euclid's Elements, where a triangle may have all sides e= qual (clearly, they cannot be identical). The axiom in the Elements that ha= s given rise to the term 'Euclidean relation' and which is appealed to in E= lements I.1 is phrased in terms of 'equal' rather than 'identical'. In Diophantus's Arithmetica, on the other hand, the two terms of an equatio= n are said to be equal, not identical, and this would become the standard t= erminology in algebra. For instance, the sign '=3D' was introduced by Rober= t 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 f= or two numbers to be identical as to magnitude just is for them to be the s= ame number. Aristotle says as much in Metaphysics M.7. Hilbert and Bernays might be one of the few logic books in the modern era t= o distinguish equality from identity (volume I, chapter 5). 'Equality' is t= here used for any equivalence relation and glossed as the obtaining of "irg= endeine Art von =DCbereinstimmung". Identity, by contrast, is "=DCbereinsti= mmung in jeder Hinsicht", as expressed by indiscernibility within the given= language. Frege, by contrast, explicitly identifies (sic!) equality with identity, an= d glosses the latter as sameness or coincidence, in the first footnote to h= is paper on sense and reference. Kleene and Church do the same in their fa= mous textbooks: 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 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 e= mail to HomotopyT...@googlegroups.com= . To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%= 40mail.gmail.com. --_000_8C57894C7413F04A98DDF5629FEC90B1652F515EPligstuqamca_ Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable
Dear all,

A few more thoughts.
We all agree that terminology and notation are important.

I love the story of the equality sign =3D introduced by Robert Recorde= (1512-1558).
"because no two things can be more equal than a pair of parallel = lines".
It took more than a century before been universally adopted.
Ren=E9 Descartes (1596-1650) used a different symbol  in his work= (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 <= br>
if it is simple and useful, but it may take time.

Andr=E9
From: homotopyt...@googlegroups.com [homo= topyt...@googlegroups.com] on behalf of Ansten M=F8rch Klev [anste...@gmail= .com]
Sent: Tuesday, May 05, 2020 4:47 AM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Identity versus equality

The discussion yesterday provides a good occasion for= me to pose a question I have long wanted to put to this list: is ther= e a convention generally agreed upon in the HoTT-community for when (if eve= r) 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 mus= t understand 'equal' in Euclid's Elements, where a triangle may have all si= des equal (clearly, they cannot be identical). The axiom in the Elements th= at 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'. 

In Diophantus's Arithmetica, on the other hand, the two terms of an eq= uation are said to be equal, not identical, and this would become the stand= ard terminology in algebra. For instance, the sign '=3D' was introduced by = Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepa= ncy with the Aristotelian/Euclidean terminology might be that when dealing = with numbers, equality just is identity, since for two numbers to be identi= cal as to magnitude just is for 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 =DCbereinstimmung". Identity, by contrast, is "=DCbereinstimmung in jeder Hinsicht",= as expressed by indiscernibility within the given language. 

Frege, by contrast, explicitly identifies (sic!) equality with identit= y, 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 i= n their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'eq= uality'.  

Clearly the two cannot be assumed to mean the same by analysts who spe= ak of two functions being identically equal!

--
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 HomotopyTypeTheory+unsu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0= jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com.
--_000_8C57894C7413F04A98DDF5629FEC90B1652F515EPligstuqamca_--