From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a37:a98c:: with SMTP id s134mr11045082qke.259.1588792731404; Wed, 06 May 2020 12:18:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aed:3b32:: with SMTP id p47ls2024505qte.4.gmail; Wed, 06 May 2020 12:18:49 -0700 (PDT) X-Received: by 2002:ac8:65d4:: with SMTP id t20mr10123917qto.358.1588792729894; Wed, 06 May 2020 12:18:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588792729; cv=none; d=google.com; s=arc-20160816; b=uKM5sOLbEnw2SeiiiZ1CYyrCn19oMNkA7bUhpurV0J/H+/AUiGbC7FqU430KoXztRy hQbZVoKkWtE1O0iu11EwhegXSQVvc5wZw3UBwsJ3SyN9YTm6wCkyeP6xiOUJBfpTW3Dl sJFJAMVrQeK0Bt15q3OPz8z0GgsrVv9kTWcFXRs8UJZHixpw4v93IlK20Brz293tuueb +1+M2R72jrk+nc1n4xVjCxZJiiqORZJY+7N67jvaJURVm4bpzDm3pyIz4pH/I/T76WB4 1xvG963q+78PgMoR8JbXbGvQoD7LdOU7/ymr2iI6yI5/jpv7IcpjTco00x2arlMfIlvQ rjHw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=jee8zkKVvC3PaMBG5f458hl49Lj1IQE4CYZCkYB4cpc=; b=zdlMdw/jW/CFf6HrcVzNB3nYdJ/ARmhUl3w8leM0lgIowWTUAM3MbJR5ObiDtf3VCo TfE1TZM/0F3mSCQIy+5YlVIDqHbYtC2WvMDcX2sm/kynLrJ/Wg4Gw0Ta5mWG/LUAJKwx c/JQwEG2O4aONBaPGDxjZPvXsksY8Ow1gzbTrQdy+MPZ2YnK4QvHcOb24fUFAPBWsCib byFTCShNfxedL4o0ymXcQ/UVF1H4KeE4BDFFku3C9JKn3NTVfqrwLpWedszR8p/ml5pA dIZiPrT3nCDsAoW3wjiQCFy4rndu835r3+Yk+K7sCSho4u/Rua21mh7Z33Wi2boiR8OE 5spg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=YdluavTr; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x330.google.com (mail-ot1-x330.google.com. [2607:f8b0:4864:20::330]) by gmr-mx.google.com with ESMTPS id c186si136636qkb.7.2020.05.06.12.18.49 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 06 May 2020 12:18:49 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::330 as permitted sender) client-ip=2607:f8b0:4864:20::330; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=YdluavTr; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x330.google.com with SMTP id j4so2304980otr.11 for ; Wed, 06 May 2020 12:18:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=jee8zkKVvC3PaMBG5f458hl49Lj1IQE4CYZCkYB4cpc=; b=YdluavTrFKEe2X7IkbdYeHOhxQybh5jg5yHzPh/K3Rsb12HMDMrGBMmqV2RKO1OPVo yMXv9h2m+73JumFd+GCxml1k1SvI5wiYobxFqG9Zc9vz/BAYyKg1G0supsOotnQPxYzC CXqkBZcqBZhm5zVKINPY+XDlTbSsck8xkWSL3q+oT+zf+64zrcMZFfAbY0zHQLAInniv 3K1IyFU3NgmymNm3MLWNOT+3O2Z+tL1TQ3orZhV19hlblE9VIO6RP/4n18NVaNkQVp/G u98bT7U+Bk4zpdmOEk99Ah2PIJl7Oxy0P/bGYqtROKqD6PWhBzNlRLIoTPlojruHg64D 5x7w== X-Gm-Message-State: AGi0PubUgmYw6HiugkKADRQM67b/XnSqF9UCah3BfXma1iWO2xQZcVA8 HEG/Oj+Gom333340tV4VOBlECcamAQfAhUFO/9iic1hiZ8eaXCL5JcNb9GF+ppJKle09zh/0Nxg xtBdFvJLS1dmwhhu9dJC+wofbsSpQutYZ6gkwyy+t1iVd+fRi8mPQujqhly95Gy7U964+3QDz7k eNMJL3kU0R X-Received: by 2002:a9d:5784:: with SMTP id q4mr7459996oth.309.1588792729099; Wed, 06 May 2020 12:18:49 -0700 (PDT) Return-Path: Received: from mail-oi1-f176.google.com (mail-oi1-f176.google.com. [209.85.167.176]) by smtp.gmail.com with ESMTPSA id k16sm756446otb.5.2020.05.06.12.18.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 06 May 2020 12:18:48 -0700 (PDT) Received: by mail-oi1-f176.google.com with SMTP id i13so2776503oie.9 for ; Wed, 06 May 2020 12:18:48 -0700 (PDT) X-Received: by 2002:aca:f541:: with SMTP id t62mr3767485oih.148.1588792727766; Wed, 06 May 2020 12:18:47 -0700 (PDT) MIME-Version: 1.0 References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> In-Reply-To: <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> From: Michael Shulman Date: Wed, 6 May 2020 12:18:36 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Steve Awodey Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 "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 ide= ntity 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 ter= minology 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 equals = 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 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 (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. > > 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 be= half 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 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'? > > 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 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'. > > 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. > > 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. > > 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'. > > 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/msgi= d/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2= A%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/msgi= d/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqa= m.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/msgi= d/HomotopyTypeTheory/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.