Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
From: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
To: "Joyal, André" <"joyal..."@uqam.ca>,
"Michael Shulman" <"shu..."@sandiego.edu>,
"Steve Awodey" <"awo..."@cmu.edu>
Subject: Re: [HoTT] Identity versus equality
Date: Thu, 7 May 2020 06:58:51 +0000	[thread overview]
Message-ID: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> (raw)

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 and 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, indeed 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

﻿On 07/05/2020, 00:29, "Joyal, André" <joyal...@uqam.ca> wrote:

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é

________________________________________
From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
Sent: Wednesday, May 06, 2020 6:54 PM
To: Michael Shulman; Steve Awodey
Subject: Re: [HoTT] Identity versus equality

I agree but let me try to make this more precise. We cannot talk about 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 talk about typing because it is not a proposition it is a part of the structure of our argument.

This becomes clear in the example: we talk about numbers but x+y is an expression, hence talking about judgemental equality only makes sense when 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 =. 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 are not properly equal but just "identified" artificially.

Thorsten

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

As I've said before, I strongly disagree that the standard
interpretation of "a=b" 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=y+x for all natural numbers x
and y, and they will say yes.  But this is false if = 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 "=" 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 <awo...@cmu.edu> wrote:
>
> Dear Andre’ (and all),
>
> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
> 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 “identifications”.
> 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’m 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 = b, short for Id(a,b).
>
> There seems to be a proposal to revise this to something like:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
> (the elements of this type are called “isos").
>
> Another (partial) option would be:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written Id(a,b) and shortened somehow a ? b,
> and pronunced ”a idenitfied with b”
> (the elements of this type are called “identifications").
>
> 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é <joyal...@uqam.ca> wrote:
>
> 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é
> ________________________________
> Sent: Tuesday, May 05, 2020 4:47 AM
> 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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%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-8919-2579F5771AFC%40cmu.edu.

--
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/CAOvivQwTR4qK094%2Bkmgj%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
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
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.



next prev parent reply	other threads:[~2020-05-07  6:58 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  [HoTT] " Joyal, André
2020-05-06 19:01    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 [this message]
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,

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

switches of git-send-email(1):

git send-email \
--to="thorsten...."@nottingham.ac.uk \
--cc="awo..."@cmu.edu \

This is a public inbox, see mirroring instructions
as well as URLs for NNTP newsgroup(s).`