Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "Joyal, André" <"joyal..."@uqam.ca>
To: "Ansten Mørch Klev" <"anste..."@gmail.com>,
	"HomotopyT...@googlegroups.com" <"HomotopyT..."@googlegroups.com>
Subject: RE: [HoTT] Identity versus equality
Date: Wed, 6 May 2020 16:02:27 +0000	[thread overview]
Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> (raw)
In-Reply-To: <CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ+pwRGD0PPjq+xyQvaJFN2A@mail.gmail.com>

[-- Attachment #1: Type: text/plain, Size: 4252 bytes --]

Dear all,

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

I love the story of the equality sign = 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é 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 = is symmetric:
the expression a=b and b=a 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é
________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch 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 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'.

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 '=' was introduced 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 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 Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility 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 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 email to HomotopyT...@googlegroups.com<mailto: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<https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com?utm_medium=email&utm_source=footer>.

[-- Attachment #2: Type: text/html, Size: 5657 bytes --]

  reply	other threads:[~2020-05-06 16:02 UTC|newest]

Thread overview: 61+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-05-05  8:47 Ansten Mørch Klev
2020-05-06 16:02 ` Joyal, André [this message]
2020-05-06 19:01   ` [HoTT] " Steve Awodey
2020-05-06 19:18     ` Michael Shulman
2020-05-06 19:31       ` Steve Awodey
2020-05-06 20:30         ` Joyal, André
2020-05-06 22:52         ` Thorsten Altenkirch
2020-05-06 22:54       ` Thorsten Altenkirch
2020-05-06 23:29         ` Joyal, André
2020-05-07  6:11           ` Egbert Rijke
2020-05-07  6:58           ` Thorsten Altenkirch
2020-05-07  9:04             ` Ansten Mørch Klev
2020-05-07 10:09             ` Thomas Streicher
2020-05-07 16:13               ` Joyal, André
2020-05-07 21:41                 ` David Roberts
2020-05-07 23:43                   ` Joyal, André
2020-05-07 23:56                     ` David Roberts
2020-05-08  6:40                       ` Thomas Streicher
2020-05-08 21:06                         ` Joyal, André
2020-05-08 23:44                           ` Steve Awodey
2020-05-09  2:46                             ` Joyal, André
2020-05-09  3:09                               ` Jon Sterling
     [not found]                             ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
2020-05-09  2:50                               ` Steve Awodey
2020-05-09  8:28                           ` Thomas Streicher
2020-05-09 15:53                             ` Joyal, André
2020-05-09 18:43                               ` Thomas Streicher
2020-05-09 20:18                                 ` Joyal, André
2020-05-09 21:27                                   ` Jon Sterling
2020-05-10  2:19                                     ` Joyal, André
2020-05-10  3:04                                       ` Jon Sterling
2020-05-10  9:09                                         ` Thomas Streicher
2020-05-10 11:59                                           ` Thorsten Altenkirch
2020-05-10 11:46                                     ` Thorsten Altenkirch
2020-05-10 14:01                                       ` Michael Shulman
2020-05-10 14:20                                         ` Nicolai Kraus
2020-05-10 14:34                                           ` Michael Shulman
2020-05-10 14:52                                             ` Nicolai Kraus
2020-05-10 15:16                                               ` Michael Shulman
2020-05-10 15:23                                                 ` Nicolai Kraus
2020-05-10 16:13                                                   ` Nicolai Kraus
2020-05-10 16:28                                                     ` Michael Shulman
2020-05-10 18:18                                                       ` Nicolai Kraus
2020-05-10 19:15                                             ` Thorsten Altenkirch
2020-05-10 19:20                                         ` Thorsten Altenkirch
2020-05-10 12:53                                   ` Ulrik Buchholtz
2020-05-10 14:01                                     ` Michael Shulman
2020-05-10 14:27                                       ` Nicolai Kraus
2020-05-10 15:35                                         ` Ulrik Buchholtz
2020-05-10 16:30                                           ` Michael Shulman
2020-05-10 18:56                                           ` Nicolai Kraus
2020-05-10 18:04                                     ` Joyal, André
2020-05-11  7:33                                       ` Thomas Streicher
2020-05-11 14:54                                         ` Joyal, André
2020-05-11 16:37                                           ` stre...
2020-05-11 16:42                                             ` Michael Shulman
2020-05-11 17:27                                               ` Thomas Streicher
2020-05-10 16:51                                   ` Nicolai Kraus
2020-05-10 18:57                                     ` Michael Shulman
2020-05-10 19:18                                     ` Nicolai Kraus
2020-05-10 20:22                                       ` Michael Shulman
2020-05-10 22:08                                         ` Joyal, André

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca \
    --to="joyal..."@uqam.ca \
    --cc="HomotopyT..."@googlegroups.com \
    --cc="anste..."@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).