*"Identifications" ?@ 2020-05-04 9:35 Thorsten Altenkirch2020-05-04 10:59 ` [HoTT] " stre... ` (2 more replies) 0 siblings, 3 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 9:35 UTC (permalink / raw) To: homotopyt...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 818 bytes --] I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal? Thorsten This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. [-- Attachment #2: Type: text/html, Size: 2286 bytes --] ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 9:35 "Identifications" ? Thorsten Altenkirch@ 2020-05-04 10:59 ` stre...2020-05-04 11:04 ` Steve Awodey 2020-05-04 11:17 ` Thorsten Altenkirch 2020-05-04 13:16 ` Michael Shulman 2020-05-07 19:43 ` Martín Hötzel Escardó 2 siblings, 2 replies; 26+ messages in thread From: stre... @ 2020-05-04 10:59 UTC (permalink / raw) To: Thorsten Altenkirch;+Cc:homotopyt...@googlegroups.com > I am just reading a paper which uses the word Ã¢Â€ÂœIdentificationÃ¢Â€Â instead > of equality. I think this has been proposed by Bob Harper. Can anybody > enlighten me what is the difference between identifications and equality? > Maybe there is an identification between them but they are not equal? Are > the real numbers 0.999Ã¢Â€Â¦ identified or are they equal? You may identify things which are not equal. So ''identify'' seems to mean consider as equal. In a sense this is very descriptive for what is going on in HoTT where one never performs quotients but rather widens equivalence relations. This is really different in the respective topos models as eg simplicial sets or already the topos of reflexive graphs as exemplified by N. Kraus's puzzling counterexample. Thomas ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 10:59 ` [HoTT] " stre...@ 2020-05-04 11:04 ` Steve Awodey2020-05-04 11:17 ` Thorsten Altenkirch 1 sibling, 0 replies; 26+ messages in thread From: Steve Awodey @ 2020-05-04 11:04 UTC (permalink / raw) To: stre...;+Cc:Thorsten Altenkirch, homotopyt...@googlegroups.com This terminology was first proposed by Dan Grayson in one of our discussions in Simonyi Hall, as a way of understanding the elements of identity types. It’s used occasionally in the book. Regards, Steve > On May 4, 2020, at 06:59, stre...@mathematik.tu-darmstadt.de wrote: > > >> >> I am just reading a paper which uses the word “Identification” instead >> of equality. I think this has been proposed by Bob Harper. Can anybody >> enlighten me what is the difference between identifications and equality? >> Maybe there is an identification between them but they are not equal? Are >> the real numbers 0.999… identified or are they equal? > > You may identify things which are not equal. So ''identify'' seems to mean > consider as equal. > In a sense this is very descriptive for what is going on in HoTT where one > never performs quotients but rather widens equivalence relations. > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > Thomas > > -- > 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/f23c7b1ada3c6fd99e47a70620c9e278.squirrel%40webmail.mathematik.tu-darmstadt.de. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 10:59 ` [HoTT] " stre... 2020-05-04 11:04 ` Steve Awodey@ 2020-05-04 11:17 ` Thorsten Altenkirch2020-05-04 11:42 ` Nicolai Kraus 2020-05-04 12:06 ` Thomas Streicher 1 sibling, 2 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 11:17 UTC (permalink / raw) To: stre...@mathematik.tu-darmstadt.de;+Cc:homotopyt...@googlegroups.com On 04/05/2020, 12:00, "stre...@mathematik.tu-darmstadt.de" <stre...@mathematik.tu-darmstadt.de> wrote: > I am just reading a paper which uses the word â€œIdentificationâ€ instead > of equality. I think this has been proposed by Bob Harper. Can anybody > enlighten me what is the difference between identifications and equality? > Maybe there is an identification between them but they are not equal? Are > the real numbers 0.999â€¦ identified or are they equal? You may identify things which are not equal. Hence my question wether 0.999... and 1 are equal or identified. My understanding is that 0.999... and 1 as real numbers are equal. That is what we mean by equality in Mathematics. The difference which is introduced here is intensional and doesn't make any sense. We may even ask whether 3+1 and 4 are identified or equal? So ''identify'' seems to mean consider as equal. In a sense this is very descriptive for what is going on in HoTT where one never performs quotients but rather widens equivalence relations. I don't understand this. Surely we quotient in HoTT even though the notion of a HIT or even a QIT (i.e. a set level HIT) are more general than ordinary set-quotients. This is really different in the respective topos models as eg simplicial sets or already the topos of reflexive graphs as exemplified by N. Kraus's puzzling counterexample. What puzzling counterexample is this? Thorsten On 04/05/2020, 12:00, "stre...@mathematik.tu-darmstadt.de" <stre...@mathematik.tu-darmstadt.de> wrote: > I am just reading a paper which uses the word â€œIdentificationâ€ instead > of equality. I think this has been proposed by Bob Harper. Can anybody > enlighten me what is the difference between identifications and equality? > Maybe there is an identification between them but they are not equal? Are > the real numbers 0.999â€¦ identified or are they equal? You may identify things which are not equal. So ''identify'' seems to mean consider as equal. In a sense this is very descriptive for what is going on in HoTT where one never performs quotients but rather widens equivalence relations. This is really different in the respective topos models as eg simplicial sets or already the topos of reflexive graphs as exemplified by N. Kraus's puzzling counterexample. Thomas This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 11:17 ` Thorsten Altenkirch@ 2020-05-04 11:42 ` Nicolai Kraus2020-05-04 12:04 ` Thorsten Altenkirch 2020-05-04 12:06 ` Thomas Streicher 1 sibling, 1 reply; 26+ messages in thread From: Nicolai Kraus @ 2020-05-04 11:42 UTC (permalink / raw) To: HomotopyTypeTheory On 04/05/2020 12:17, Thorsten Altenkirch wrote: > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? Thomas was referring to: https://homotopytypetheory.org/2013/10/28/ You may also have seen it in my thesis or the paper "Notions of Anonymous Existence in Martin-Löf Type Theory". :) Nicolai ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 11:42 ` Nicolai Kraus@ 2020-05-04 12:04 ` Thorsten Altenkirch0 siblings, 0 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 12:04 UTC (permalink / raw) To: nicolai.kraus, homotopyt...@googlegroups.com I always thought that the "magic trick" would just cause confusion. It is important to distinguish whether we talk about Mathematics or whether we do Mathematics. The magic trick example works because we confuse the two. Myst reduces to the secret but mathematically there is no inverse. What matters is the latter. Thorsten On 04/05/2020, 12:42, "Nicolai Kraus" <nicola...@gmail.com> wrote: On 04/05/2020 12:17, Thorsten Altenkirch wrote: > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? Thomas was referring to: https://homotopytypetheory.org/2013/10/28/ You may also have seen it in my thesis or the paper "Notions of Anonymous Existence in Martin-Löf Type Theory". :) Nicolai -- 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/a2504582-a7f5-6bcb-ebc6-17ae869ebaa8%40gmail.com. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 11:17 ` Thorsten Altenkirch 2020-05-04 11:42 ` Nicolai Kraus@ 2020-05-04 12:06 ` Thomas Streicher2020-05-04 12:12 ` Thorsten Altenkirch 1 sibling, 1 reply; 26+ messages in thread From: Thomas Streicher @ 2020-05-04 12:06 UTC (permalink / raw) To: Thorsten Altenkirch;+Cc:homotopyt...@googlegroups.com Hi Thorsten, > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? I learnt it from Nicolai when he gave a little talk at CSL 2017 when given a prize for his thesis. The counterexample or rather my appreciation of it I have made a little note on which I have put for convenience at https://www.mathematik.tu-darmstadt.de/~streicher/kraus.pdf The point is that interpreting HoTT in sSet is very different from the traditional interpretation of logic in sSet. The same happens already the topos of reflexive graphs. Propositions are connected reflexive graphs and thee are very man nonisomorphic such guys but HoTT identifies them all. But this has nothing to do with HoTT per se. For example you can interpret HOL in assemblies in two very different ways once `a la topos (proof irrelevant) and once `a la model of TT (proof relevant). In mathematics equality is a very relative notion. But one may perform quotients to reconcile them... Thomas ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 12:06 ` Thomas Streicher@ 2020-05-04 12:12 ` Thorsten Altenkirch2020-05-04 12:39 ` Thomas Streicher 0 siblings, 1 reply; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 12:12 UTC (permalink / raw) To: Thomas Streicher;+Cc:homotopyt...@googlegroups.com Hi Thomas But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics. Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities. Do you think of a model of set theory when you do set theory? Cheers, Thorsten On 04/05/2020, 13:06, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote: Hi Thorsten, > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? I learnt it from Nicolai when he gave a little talk at CSL 2017 when given a prize for his thesis. The counterexample or rather my appreciation of it I have made a little note on which I have put for convenience at https://www.mathematik.tu-darmstadt.de/~streicher/kraus.pdf The point is that interpreting HoTT in sSet is very different from the traditional interpretation of logic in sSet. The same happens already the topos of reflexive graphs. Propositions are connected reflexive graphs and thee are very man nonisomorphic such guys but HoTT identifies them all. But this has nothing to do with HoTT per se. For example you can interpret HOL in assemblies in two very different ways once `a la topos (proof irrelevant) and once `a la model of TT (proof relevant). In mathematics equality is a very relative notion. But one may perform quotients to reconcile them... Thomas This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 12:12 ` Thorsten Altenkirch@ 2020-05-04 12:39 ` Thomas Streicher0 siblings, 0 replies; 26+ messages in thread From: Thomas Streicher @ 2020-05-04 12:39 UTC (permalink / raw) To: Thorsten Altenkirch;+Cc:homotopyt...@googlegroups.com Hi Thorsten, > But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics. > > Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities. I am not sure what you really mean but I guess you refer to the distinction between what is provable in HoTT and what holds or exists in particular models. Of couse, Nicolai"s vexing example is model dependent (at least in my reconstruction!) But that is the same in set theory. Most of the time you are model independent, i.e. provable in ZFC or actually much weaker systems. But there are quite a few things which heavily depend on the model. Continuum Hypothesis for example but many other things as well. Modern set theory is essentially about independences... And if you consider ZF the notions of finite and Dedekind finite are different. That is in my opinion an example where incompleteness strikes already on a very basic level! Thomas PS But I agree that this is "metamathematical" but so what. Mathematics is not one fixed game but rather pluralist even classically. Even more so constructively where things branch much earlier. As a (categorical) logician one is interested in constructive mathematics precisely because of this excessive pluralism! I never understood why constructive math is used in the singular since it is even false for classical maths. And adding strong principles doesn't mean one gets nonalgorithmic. Adding to HA all true Pi^0_1 sentences doesn't allow you to construct functions on N which are not recursive (as follow from number realizability). ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 9:35 "Identifications" ? Thorsten Altenkirch 2020-05-04 10:59 ` [HoTT] " stre...@ 2020-05-04 13:16 ` Michael Shulman2020-05-04 14:17 ` Thorsten Altenkirch 2020-05-04 14:48 ` Stefan Monnier 2020-05-07 19:43 ` Martín Hötzel Escardó 2 siblings, 2 replies; 26+ messages in thread From: Michael Shulman @ 2020-05-04 13:16 UTC (permalink / raw) To: Thorsten Altenkirch;+Cc:homotopyt...@googlegroups.com I don't think using "identification" necessarily implies any difference between "identification" and "equality". I don't think of it that way. For me the point is just to have a word that refers to an *element* of an identity type. Calling it "an equality" can have the wrong connotation because classically, an equality is just a proposition (or a true proposition), whereas an element of an identity type carries information. Calling it "an identification" suggests exactly the information that it carries: a way of identifying two things. On Mon, May 4, 2020 at 2:35 AM Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal? > > > > Thorsten > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > -- > 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/BBC0B8F3-AB16-4196-B9B9-B1B3031B2D7D%40nottingham.ac.uk. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 13:16 ` Michael Shulman@ 2020-05-04 14:17 ` Thorsten Altenkirch2020-05-04 14:48 ` Stefan Monnier 1 sibling, 0 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 14:17 UTC (permalink / raw) To: Michael Shulman;+Cc:homotopyt...@googlegroups.com This seems reasonable. I usually say "equality proofs" but the word proof also has other conotations. Also what is an element of 3 <= 4, if not a proof or evidence? Maybe it is a inidentification? __ Thorsten On 04/05/2020, 14:17, "Michael Shulman" <shu...@sandiego.edu> wrote: I don't think using "identification" necessarily implies any difference between "identification" and "equality". I don't think of it that way. For me the point is just to have a word that refers to an *element* of an identity type. Calling it "an equality" can have the wrong connotation because classically, an equality is just a proposition (or a true proposition), whereas an element of an identity type carries information. Calling it "an identification" suggests exactly the information that it carries: a way of identifying two things. On Mon, May 4, 2020 at 2:35 AM Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal? > > > > Thorsten > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > -- > 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/BBC0B8F3-AB16-4196-B9B9-B1B3031B2D7D%40nottingham.ac.uk. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 13:16 ` Michael Shulman 2020-05-04 14:17 ` Thorsten Altenkirch@ 2020-05-04 14:48 ` Stefan Monnier2020-05-04 15:46 ` Nicolai Kraus 2020-05-04 15:59 ` Michael Shulman 1 sibling, 2 replies; 26+ messages in thread From: Stefan Monnier @ 2020-05-04 14:48 UTC (permalink / raw) To: Michael Shulman;+Cc:Thorsten Altenkirch, homotopyt...@googlegroups.com > I don't think using "identification" necessarily implies any > difference between "identification" and "equality". I don't think of > it that way. For me the point is just to have a word that refers to > an *element* of an identity type. Calling it "an equality" can have > the wrong connotation because classically, an equality is just a > proposition (or a true proposition), whereas an element of an identity > type carries information. Calling it "an identification" suggests > exactly the information that it carries: a way of identifying two > things. I thought that's what "path" was for? Stefan "who really doesn't know what he's talking about" ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 14:48 ` Stefan Monnier@ 2020-05-04 15:46 ` Nicolai Kraus2020-05-04 15:57 ` Thorsten Altenkirch 2020-05-04 15:59 ` Michael Shulman 1 sibling, 1 reply; 26+ messages in thread From: Nicolai Kraus @ 2020-05-04 15:46 UTC (permalink / raw) To: HomotopyTypeTheory For what it's worth, "identification" is much closer to Per Martin-Löf's original terminology ("identity type") than "equality" or "path" are. Nicolai On 04/05/2020 15:48, Stefan Monnier wrote: >> I don't think using "identification" necessarily implies any >> difference between "identification" and "equality". I don't think of >> it that way. For me the point is just to have a word that refers to >> an *element* of an identity type. Calling it "an equality" can have >> the wrong connotation because classically, an equality is just a >> proposition (or a true proposition), whereas an element of an identity >> type carries information. Calling it "an identification" suggests >> exactly the information that it carries: a way of identifying two >> things. > I thought that's what "path" was for? > > > Stefan "who really doesn't know what he's talking about" > ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 15:46 ` Nicolai Kraus@ 2020-05-04 15:57 ` Thorsten Altenkirch0 siblings, 0 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 15:57 UTC (permalink / raw) To: nicolai.kraus, homotopyt...@googlegroups.com Ok, I apologize discussions on names and syntax are at the same time very attractive and are also scoffed at because they seem not to have much content. I am quite happy with Mike's explanation to use the word "identifications" for inhabitants of equality types. "Paths" or "equality proofs" or "evidence for equality" are also good alternatives. However, I prefer to use the word "equality" even equality is not propositional. Two mathematical objects which share all properties we can talk about should be considered equal even if there is more than one reason / proof / identification that this is the case. Moreover, there is no other "equality" we can talk about in Type Theory. Thorsten On 04/05/2020, 16:47, "homotopyt...@googlegroups.com on behalf of Nicolai Kraus" <homotopyt...@googlegroups.com on behalf of nicola...@gmail.com> wrote: For what it's worth, "identification" is much closer to Per Martin-Löf's original terminology ("identity type") than "equality" or "path" are. Nicolai On 04/05/2020 15:48, Stefan Monnier wrote: >> I don't think using "identification" necessarily implies any >> difference between "identification" and "equality". I don't think of >> it that way. For me the point is just to have a word that refers to >> an *element* of an identity type. Calling it "an equality" can have >> the wrong connotation because classically, an equality is just a >> proposition (or a true proposition), whereas an element of an identity >> type carries information. Calling it "an identification" suggests >> exactly the information that it carries: a way of identifying two >> things. > I thought that's what "path" was for? > > > Stefan "who really doesn't know what he's talking about" > -- 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/b1b554b1-1c70-0bd6-5c09-cd5f0f2e48f9%40gmail.com. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 14:48 ` Stefan Monnier 2020-05-04 15:46 ` Nicolai Kraus@ 2020-05-04 15:59 ` Michael Shulman2020-05-04 16:07 ` Steve Awodey 2020-05-04 16:16 ` Joyal, André 1 sibling, 2 replies; 26+ messages in thread From: Michael Shulman @ 2020-05-04 15:59 UTC (permalink / raw) To: Stefan Monnier;+Cc:Thorsten Altenkirch, homotopyt...@googlegroups.com The word "path" is closely tied to the homotopy interpretation, and to the classical perspective of oo-groupoids presented via topological spaces, which has various problems. This is particularly an issue in cohesive type theory, where there is a separate "point-set level" notion of path that it is important to distinguish from identifications. On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: > > > I don't think using "identification" necessarily implies any > > difference between "identification" and "equality". I don't think of > > it that way. For me the point is just to have a word that refers to > > an *element* of an identity type. Calling it "an equality" can have > > the wrong connotation because classically, an equality is just a > > proposition (or a true proposition), whereas an element of an identity > > type carries information. Calling it "an identification" suggests > > exactly the information that it carries: a way of identifying two > > things. > > I thought that's what "path" was for? > > > Stefan "who really doesn't know what he's talking about" > ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 15:59 ` Michael Shulman@ 2020-05-04 16:07 ` Steve Awodey2020-05-04 16:17 ` Thorsten Altenkirch 2020-05-04 16:21 ` Peter LeFanu Lumsdaine 2020-05-04 16:16 ` Joyal, André 1 sibling, 2 replies; 26+ messages in thread From: Steve Awodey @ 2020-05-04 16:07 UTC (permalink / raw) To: Michael Shulman Cc: Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. : - ) > On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: > > The word "path" is closely tied to the homotopy interpretation, and to > the classical perspective of oo-groupoids presented via topological > spaces, which has various problems. This is particularly an issue in > cohesive type theory, where there is a separate "point-set level" > notion of path that it is important to distinguish from > identifications. > >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: >> >>> I don't think using "identification" necessarily implies any >>> difference between "identification" and "equality". I don't think of >>> it that way. For me the point is just to have a word that refers to >>> an *element* of an identity type. Calling it "an equality" can have >>> the wrong connotation because classically, an equality is just a >>> proposition (or a true proposition), whereas an element of an identity >>> type carries information. Calling it "an identification" suggests >>> exactly the information that it carries: a way of identifying two >>> things. >> >> I thought that's what "path" was for? >> >> >> Stefan "who really doesn't know what he's talking about" >> > > -- > 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. ^ permalink raw reply [flat|nested] 26+ messages in thread

*RE: [HoTT] "Identifications" ?2020-05-04 15:59 ` Michael Shulman 2020-05-04 16:07 ` Steve Awodey@ 2020-05-04 16:16 ` Joyal, André2020-05-04 20:38 ` Joyal, André 1 sibling, 1 reply; 26+ messages in thread From: Joyal, André @ 2020-05-04 16:16 UTC (permalink / raw) To: Michael Shulman, Stefan Monnier Cc: Thorsten Altenkirch, homotopyt...@googlegroups.com Dear all, I am tempted to add my grain of salt to this discussion. I like the word "identification". But what about "iso" ? It means "equal". As in "iso-morphism", "iso-tope", etc. https://wordinfo.info/unit/2795/page:9 Best, André ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu] Sent: Monday, May 04, 2020 11:59 AM To: Stefan Monnier Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com Subject: Re: [HoTT] "Identifications" ? The word "path" is closely tied to the homotopy interpretation, and to the classical perspective of oo-groupoids presented via topological spaces, which has various problems. This is particularly an issue in cohesive type theory, where there is a separate "point-set level" notion of path that it is important to distinguish from identifications. On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: > > > I don't think using "identification" necessarily implies any > > difference between "identification" and "equality". I don't think of > > it that way. For me the point is just to have a word that refers to > > an *element* of an identity type. Calling it "an equality" can have > > the wrong connotation because classically, an equality is just a > > proposition (or a true proposition), whereas an element of an identity > > type carries information. Calling it "an identification" suggests > > exactly the information that it carries: a way of identifying two > > things. > > I thought that's what "path" was for? > > > Stefan "who really doesn't know what he's talking about" > -- 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 16:07 ` Steve Awodey@ 2020-05-04 16:17 ` Thorsten Altenkirch2020-05-04 16:53 ` Steve Awodey 2020-05-04 16:21 ` Peter LeFanu Lumsdaine 1 sibling, 1 reply; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 16:17 UTC (permalink / raw) To: Steve Awodey, Michael Shulman Cc: Stefan Monnier, homotopyt...@googlegroups.com I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. : - ) One of our dogs gained access to my laptop - sorry. These animals can be very awkward. However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type. Thorsten On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> wrote: I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. : - ) > On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: > > The word "path" is closely tied to the homotopy interpretation, and to > the classical perspective of oo-groupoids presented via topological > spaces, which has various problems. This is particularly an issue in > cohesive type theory, where there is a separate "point-set level" > notion of path that it is important to distinguish from > identifications. > >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: >> >>> I don't think using "identification" necessarily implies any >>> difference between "identification" and "equality". I don't think of >>> it that way. For me the point is just to have a word that refers to >>> an *element* of an identity type. Calling it "an equality" can have >>> the wrong connotation because classically, an equality is just a >>> proposition (or a true proposition), whereas an element of an identity >>> type carries information. Calling it "an identification" suggests >>> exactly the information that it carries: a way of identifying two >>> things. >> >> I thought that's what "path" was for? >> >> >> Stefan "who really doesn't know what he's talking about" >> > > -- > 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 16:07 ` Steve Awodey 2020-05-04 16:17 ` Thorsten Altenkirch@ 2020-05-04 16:21 ` Peter LeFanu Lumsdaine1 sibling, 0 replies; 26+ messages in thread From: Peter LeFanu Lumsdaine @ 2020-05-04 16:21 UTC (permalink / raw) To: Steve Awodey Cc: Michael Shulman, Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 3489 bytes --] Ah, I just thought the whole system was having a clock malfunction and re-sending a discussion from 2016… :-P On the serious side: one motivation for “identification” not yet mentioned is that it’s more in line with traditional mathematical usage. Saying that the circle defined as R/Z or as a subset of R^2 are “equal” clashes badly with the traditional mathematical usage of words, and (for at least some mathematicians) their mental picture of mathematics — but saying that we can identify them, and that all nice properties respect such identifications, is completely consistent with traditional writing and worldviews. Also, the fact that we may identify things in multiple ways, and so have to be a little careful about how we make use of such identifications, fits with traditional intuition and practice. So saying “identifications” may require less rewiring in our brains than saying “equalities” or “paths”, at least in types of algebraic structures and similar. (For synthetic homotopy theory, of course, “paths” often fits closer to established usage.) –p. On Mon, May 4, 2020 at 6:07 PM Steve Awodey <steve...@gmail.com> wrote: > I’m afraid that someone may have hacked Thorsten’s email account. The real > Thorsten went through all this with us many years ago. > : - ) > > > > On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: > > > > The word "path" is closely tied to the homotopy interpretation, and to > > the classical perspective of oo-groupoids presented via topological > > spaces, which has various problems. This is particularly an issue in > > cohesive type theory, where there is a separate "point-set level" > > notion of path that it is important to distinguish from > > identifications. > > > >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> > wrote: > >> > >>> I don't think using "identification" necessarily implies any > >>> difference between "identification" and "equality". I don't think of > >>> it that way. For me the point is just to have a word that refers to > >>> an *element* of an identity type. Calling it "an equality" can have > >>> the wrong connotation because classically, an equality is just a > >>> proposition (or a true proposition), whereas an element of an identity > >>> type carries information. Calling it "an identification" suggests > >>> exactly the information that it carries: a way of identifying two > >>> things. > >> > >> I thought that's what "path" was for? > >> > >> > >> Stefan "who really doesn't know what he's talking about" > >> > > > > -- > > 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%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/E31B538B-E0C9-4D4F-A4F1-4335E59CAE0D%40gmail.com > . > [-- Attachment #2: Type: text/html, Size: 4841 bytes --] ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 16:17 ` Thorsten Altenkirch@ 2020-05-04 16:53 ` Steve Awodey2020-05-04 17:25 ` Thorsten Altenkirch 0 siblings, 1 reply; 26+ messages in thread From: Steve Awodey @ 2020-05-04 16:53 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com > On May 4, 2020, at 12:17 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > : - ) > > One of our dogs gained access to my laptop - sorry. These animals can be very awkward. > > However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type. I remember that conversation. I think we decided to put the question “what does x=y mean?” aside, until we had taken care of more important things. So is it time now? Steve > > Thorsten > > On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> wrote: > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > : - ) > > >> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: >> >> The word "path" is closely tied to the homotopy interpretation, and to >> the classical perspective of oo-groupoids presented via topological >> spaces, which has various problems. This is particularly an issue in >> cohesive type theory, where there is a separate "point-set level" >> notion of path that it is important to distinguish from >> identifications. >> >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: >>> >>>> I don't think using "identification" necessarily implies any >>>> difference between "identification" and "equality". I don't think of >>>> it that way. For me the point is just to have a word that refers to >>>> an *element* of an identity type. Calling it "an equality" can have >>>> the wrong connotation because classically, an equality is just a >>>> proposition (or a true proposition), whereas an element of an identity >>>> type carries information. Calling it "an identification" suggests >>>> exactly the information that it carries: a way of identifying two >>>> things. >>> >>> I thought that's what "path" was for? >>> >>> >>> Stefan "who really doesn't know what he's talking about" >>> >> >> -- >> 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > > -- > 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/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 16:53 ` Steve Awodey@ 2020-05-04 17:25 ` Thorsten Altenkirch2020-05-04 17:43 ` Michael Shulman 2020-05-04 17:55 ` Steve Awodey 0 siblings, 2 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-04 17:25 UTC (permalink / raw) To: Steve Awodey Cc: Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com Hi Steve, I remember that conversation. I think we decided to put the question “what does x=y mean?” aside, until we had taken care of more important things. I suppose this was just a way to move on without having to reach an agreement. I think it is more than a discussion about terms. What do we mean by equality? Does the equality type in HoTT is something fundamentally different? In a way yes, because it is proof relevant so some of the old terminology doesn't apply anymore. That is equality of structures is a structure not a proposition. But nevertheless I find it confusing to call it anything but equality. I would say two mathematical objects which share all the same properties, which behave the same, are equal. I don't like Leibniz's "equality of indiscernibles" because it uses a negative. I noticed that many people use type theory always as something we talk about. It is just a formalism. Hence the equality type just expresses an identification of things which are actually different. In the real world. However, I think when we talk in type theory then this is our real world (at least metaphorically) and then the metatheoretic perspective is just a confusion. Does this make sense? Sorry, I realize it is a bit philosophical but then you are in the department of philosophy... __ Thorsten On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote: > On May 4, 2020, at 12:17 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > : - ) > > One of our dogs gained access to my laptop - sorry. These animals can be very awkward. > > However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type. I remember that conversation. I think we decided to put the question “what does x=y mean?” aside, until we had taken care of more important things. So is it time now? Steve > > Thorsten > > On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> wrote: > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > : - ) > > >> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: >> >> The word "path" is closely tied to the homotopy interpretation, and to >> the classical perspective of oo-groupoids presented via topological >> spaces, which has various problems. This is particularly an issue in >> cohesive type theory, where there is a separate "point-set level" >> notion of path that it is important to distinguish from >> identifications. >> >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: >>> >>>> I don't think using "identification" necessarily implies any >>>> difference between "identification" and "equality". I don't think of >>>> it that way. For me the point is just to have a word that refers to >>>> an *element* of an identity type. Calling it "an equality" can have >>>> the wrong connotation because classically, an equality is just a >>>> proposition (or a true proposition), whereas an element of an identity >>>> type carries information. Calling it "an identification" suggests >>>> exactly the information that it carries: a way of identifying two >>>> things. >>> >>> I thought that's what "path" was for? >>> >>> >>> Stefan "who really doesn't know what he's talking about" >>> >> >> -- >> 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > > -- > 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/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 17:25 ` Thorsten Altenkirch@ 2020-05-04 17:43 ` Michael Shulman2020-05-04 17:55 ` Steve Awodey 1 sibling, 0 replies; 26+ messages in thread From: Michael Shulman @ 2020-05-04 17:43 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Steve Awodey, Stefan Monnier, homotopyt...@googlegroups.com I think "identification" is a nice middle-ground between "equality" and "path/isomorphism". On the one hand it signals that something more is meant than the thing traditionally called "equality" (even though I agree with Thorsten that inside of type theory this is the thing called "equality") -- and, I think, does a good job of suggesting precisely *what* more is meant. On the other hand, it still carries the meaning that two things are *the same* (in a particular way) -- two things that have been "identified" are now "identical" -- whereas "path" and "isomorphism" suggest their traditional meanings of two things that are *not* fundamentally the same but are related in some same-like-way. On Mon, May 4, 2020 at 10:25 AM Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > Hi Steve, > > I remember that conversation. > I think we decided to put the question “what does x=y mean?” aside, > until we had taken care of more important things. > > I suppose this was just a way to move on without having to reach an agreement. > > I think it is more than a discussion about terms. What do we mean by equality? Does the equality type in HoTT is something fundamentally different? In a way yes, because it is proof relevant so some of the old terminology doesn't apply anymore. That is equality of structures is a structure not a proposition. But nevertheless I find it confusing to call it anything but equality. I would say two mathematical objects which share all the same properties, which behave the same, are equal. I don't like Leibniz's "equality of indiscernibles" because it uses a negative. > > I noticed that many people use type theory always as something we talk about. It is just a formalism. Hence the equality type just expresses an identification of things which are actually different. In the real world. However, I think when we talk in type theory then this is our real world (at least metaphorically) and then the metatheoretic perspective is just a confusion. > > Does this make sense? Sorry, I realize it is a bit philosophical but then you are in the department of philosophy... __ > > Thorsten > > On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote: > > > > > On May 4, 2020, at 12:17 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > > > > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > > : - ) > > > > One of our dogs gained access to my laptop - sorry. These animals can be very awkward. > > > > However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type. > > I remember that conversation. > I think we decided to put the question “what does x=y mean?” aside, > until we had taken care of more important things. > > So is it time now? > > Steve > > > > > Thorsten > > > > On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> wrote: > > > > I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. > > : - ) > > > > > >> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: > >> > >> The word "path" is closely tied to the homotopy interpretation, and to > >> the classical perspective of oo-groupoids presented via topological > >> spaces, which has various problems. This is particularly an issue in > >> cohesive type theory, where there is a separate "point-set level" > >> notion of path that it is important to distinguish from > >> identifications. > >> > >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: > >>> > >>>> I don't think using "identification" necessarily implies any > >>>> difference between "identification" and "equality". I don't think of > >>>> it that way. For me the point is just to have a word that refers to > >>>> an *element* of an identity type. Calling it "an equality" can have > >>>> the wrong connotation because classically, an equality is just a > >>>> proposition (or a true proposition), whereas an element of an identity > >>>> type carries information. Calling it "an identification" suggests > >>>> exactly the information that it carries: a way of identifying two > >>>> things. > >>> > >>> I thought that's what "path" was for? > >>> > >>> > >>> Stefan "who really doesn't know what he's talking about" > >>> > >> > >> -- > >> 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. > > > > > > > > > > This message and any attachment are intended solely for the addressee > > and may contain confidential information. If you have received this > > message in error, please contact the sender and delete the email and > > 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. > > > > > > > > > > -- > > 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/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk. > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: [HoTT] "Identifications" ?2020-05-04 17:25 ` Thorsten Altenkirch 2020-05-04 17:43 ` Michael Shulman@ 2020-05-04 17:55 ` Steve Awodey1 sibling, 0 replies; 26+ messages in thread From: Steve Awodey @ 2020-05-04 17:55 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com > On May 4, 2020, at 1:25 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > Hi Steve, > > I remember that conversation. > I think we decided to put the question “what does x=y mean?” aside, > until we had taken care of more important things. > > I suppose this was just a way to move on without having to reach an agreement. yup > > I think it is more than a discussion about terms. What do we mean by equality? Does the equality type in HoTT is something fundamentally different? In a way yes, because it is proof relevant so some of the old terminology doesn't apply anymore. That is equality of structures is a structure not a proposition. But nevertheless I find it confusing to call it anything but equality. I would say two mathematical objects which share all the same properties, which behave the same, are equal. I don't like Leibniz's "equality of indiscernibles" because it uses a negative. you seem to prefer the term “equality” over “identity” - even when (mis)quoting Leibniz! maybe that’s part of the problem: if we talk about “identity types” instead of “equality types” then it’s easier to regard them as structures, the inhabitants of which are “identifications”, rather than “equality proofs” (which introduces an unwanted meta-perspective). Frege once considered equality as a relation between symbols, rather than what they denote — he later rejected that view, but I don’t think it's so bad. Definitional equality can be thought of like this — it’s a meta-statement about (pseudo-) syntactic things. The relation that we can reason about inside the system is called *identity*, and it’s a "proof relevant” relation — or better put, it’s a proper structure, not a mere proposition — its elements are identifications, and these we know admit an oo-groupoid structure. > > Does this make sense? Sorry, I realize it is a bit philosophical but then you are in the department of philosophy… __ to my everlasting regret — and thanks for not calling me a philosopher! Steve > > Thorsten > > On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote: > > > >> On May 4, 2020, at 12:17 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: >> >> >> I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. >> : - ) >> >> One of our dogs gained access to my laptop - sorry. These animals can be very awkward. >> >> However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type. > > I remember that conversation. > I think we decided to put the question “what does x=y mean?” aside, > until we had taken care of more important things. > > So is it time now? > > Steve > >> >> Thorsten >> >> On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> wrote: >> >> I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago. >> : - ) >> >> >>> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote: >>> >>> The word "path" is closely tied to the homotopy interpretation, and to >>> the classical perspective of oo-groupoids presented via topological >>> spaces, which has various problems. This is particularly an issue in >>> cohesive type theory, where there is a separate "point-set level" >>> notion of path that it is important to distinguish from >>> identifications. >>> >>>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: >>>> >>>>> I don't think using "identification" necessarily implies any >>>>> difference between "identification" and "equality". I don't think of >>>>> it that way. For me the point is just to have a word that refers to >>>>> an *element* of an identity type. Calling it "an equality" can have >>>>> the wrong connotation because classically, an equality is just a >>>>> proposition (or a true proposition), whereas an element of an identity >>>>> type carries information. Calling it "an identification" suggests >>>>> exactly the information that it carries: a way of identifying two >>>>> things. >>>> >>>> I thought that's what "path" was for? >>>> >>>> >>>> Stefan "who really doesn't know what he's talking about" >>>> >>> >>> -- >>> 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com. >> >> >> >> >> This message and any attachment are intended solely for the addressee >> and may contain confidential information. If you have received this >> message in error, please contact the sender and delete the email and >> 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. >> >> >> >> >> -- >> 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/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk. > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > ^ permalink raw reply [flat|nested] 26+ messages in thread

*RE: [HoTT] "Identifications" ?2020-05-04 16:16 ` Joyal, André@ 2020-05-04 20:38 ` Joyal, André0 siblings, 0 replies; 26+ messages in thread From: Joyal, André @ 2020-05-04 20:38 UTC (permalink / raw) To: Michael Shulman, Stefan Monnier Cc: Thorsten Altenkirch, homotopyt...@googlegroups.com Of course, the term "identification" has other meanings. As when the police is trying to identify the victim of a murder. An identification may require an identity document. A hacker may prefer to stay anonymous. The term "iso" could be better. Let f:a=b be an iso between the elements a and b of a type A. Let f:A=B be an isomorphism between the types A and B. The univalence principle state that every isomorphism is an iso. A ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Joyal, André [joyal...@uqam.ca] Sent: Monday, May 04, 2020 12:16 PM To: Michael Shulman; Stefan Monnier Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com Subject: RE: [HoTT] "Identifications" ? Dear all, I am tempted to add my grain of salt to this discussion. I like the word "identification". But what about "iso" ? It means "equal". As in "iso-morphism", "iso-tope", etc. https://wordinfo.info/unit/2795/page:9 Best, André ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu] Sent: Monday, May 04, 2020 11:59 AM To: Stefan Monnier Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com Subject: Re: [HoTT] "Identifications" ? The word "path" is closely tied to the homotopy interpretation, and to the classical perspective of oo-groupoids presented via topological spaces, which has various problems. This is particularly an issue in cohesive type theory, where there is a separate "point-set level" notion of path that it is important to distinguish from identifications. On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote: > > > I don't think using "identification" necessarily implies any > > difference between "identification" and "equality". I don't think of > > it that way. For me the point is just to have a word that refers to > > an *element* of an identity type. Calling it "an equality" can have > > the wrong connotation because classically, an equality is just a > > proposition (or a true proposition), whereas an element of an identity > > type carries information. Calling it "an identification" suggests > > exactly the information that it carries: a way of identifying two > > things. > > I thought that's what "path" was for? > > > Stefan "who really doesn't know what he's talking about" > -- 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%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/8C57894C7413F04A98DDF5629FEC90B1652F3F0F%40Pli.gst.uqam.ca. ^ permalink raw reply [flat|nested] 26+ messages in thread

*Re: "Identifications" ?2020-05-04 9:35 "Identifications" ? Thorsten Altenkirch 2020-05-04 10:59 ` [HoTT] " stre... 2020-05-04 13:16 ` Michael Shulman@ 2020-05-07 19:43 ` Martín Hötzel Escardó2020-05-08 10:41 ` [HoTT] " Thorsten Altenkirch 2 siblings, 1 reply; 26+ messages in thread From: Martín Hötzel Escardó @ 2020-05-07 19:43 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1161 bytes --] The meanings of "equal" and "identical" are the same. They both mean "same", and are equivalent to "equivalent" according to most dictionaries. Try not to be too judgmental, Thorsten. Best, Martin On Monday, 4 May 2020 10:35:53 UTC+1, Thorsten Altenkirch wrote: > > I am just reading a paper which uses the word “Identification” instead of > equality. I think this has been proposed by Bob Harper. Can anybody > enlighten me what is the difference between identifications and equality? > Maybe there is an identification between them but they are not equal? Are > the real numbers 0.999… identified or are they equal? > > > > Thorsten > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > 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. > > > > > [-- Attachment #1.2: Type: text/html, Size: 1661 bytes --] ^ permalink raw reply [flat|nested] 26+ messages in thread

*2020-05-07 19:43 ` Martín Hötzel EscardóRe: [HoTT] Re: "Identifications" ?@ 2020-05-08 10:41 ` Thorsten Altenkirch0 siblings, 0 replies; 26+ messages in thread From: Thorsten Altenkirch @ 2020-05-08 10:41 UTC (permalink / raw) To: Martín Hötzel Escardó;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 2671 bytes --] Sent from my iPhone On 7 May 2020, at 20:43, Martín Hötzel Escardó <escard...@gmail.com> wrote: The meanings of "equal" and "identical" are the same. They both mean "same", and are equivalent to "equivalent" according to most dictionaries. I know. My point was rather that there is no need to replace equality/identity by another word, eg identification to suggest that equality in HoTT is anything fundamentally different. My impression is that some people think that equality in HoTT is something different to true equality as it occurs in nature. Try not to be too judgmental, Thorsten. What do you mean? Maybe you shouldn’t jump to conclusions what you think I mean too quickly, Martin. Thorsten Best, Martin On Monday, 4 May 2020 10:35:53 UTC+1, Thorsten Altenkirch wrote: I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal? Thorsten This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. -- 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/994babd9-6067-41a1-b12a-17c149138fdb%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/994babd9-6067-41a1-b12a-17c149138fdb%40googlegroups.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and 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. [-- Attachment #2: Type: text/html, Size: 3996 bytes --] ^ permalink raw reply [flat|nested] 26+ messages in thread

end of thread, back to indexThread overview:26+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2020-05-04 9:35 "Identifications" ? Thorsten Altenkirch 2020-05-04 10:59 ` [HoTT] " stre... 2020-05-04 11:04 ` Steve Awodey 2020-05-04 11:17 ` Thorsten Altenkirch 2020-05-04 11:42 ` Nicolai Kraus 2020-05-04 12:04 ` Thorsten Altenkirch 2020-05-04 12:06 ` Thomas Streicher 2020-05-04 12:12 ` Thorsten Altenkirch 2020-05-04 12:39 ` Thomas Streicher 2020-05-04 13:16 ` Michael Shulman 2020-05-04 14:17 ` Thorsten Altenkirch 2020-05-04 14:48 ` Stefan Monnier 2020-05-04 15:46 ` Nicolai Kraus 2020-05-04 15:57 ` Thorsten Altenkirch 2020-05-04 15:59 ` Michael Shulman 2020-05-04 16:07 ` Steve Awodey 2020-05-04 16:17 ` Thorsten Altenkirch 2020-05-04 16:53 ` Steve Awodey 2020-05-04 17:25 ` Thorsten Altenkirch 2020-05-04 17:43 ` Michael Shulman 2020-05-04 17:55 ` Steve Awodey 2020-05-04 16:21 ` Peter LeFanu Lumsdaine 2020-05-04 16:16 ` Joyal, André 2020-05-04 20:38 ` Joyal, André 2020-05-07 19:43 ` Martín Hötzel Escardó 2020-05-08 10:41 ` [HoTT] " Thorsten Altenkirch

Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Example config snippet for mirrors Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/public-inbox.git