Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorwhatever
   • CommentTimeMay 8th 2016
   • PermaLink
   Author: whatever
   Format: TextCan someone perhaps rewrite https://ncatlab.org/nlab/show/identity%20type to define precisely what a canonically defined term is or to remove its usage completely (but replace it with something equivalent) as it does not add to better comprehension of the text. I would also be happy if someone would explain it here. It seems there is a wide confusion about what "canonical" means for various people, because it is sort of a loose term in many subfields. While I acknowledge that there might be some definition in the basement of Alpha Centauri, I don't think that's the best way forward.

   Can someone perhaps rewrite https://ncatlab.org/nlab/show/identity%20type to define precisely what a canonically defined term is or to remove its usage completely (but replace it with something equivalent) as it does not add to better comprehension of the text.
   
   I would also be happy if someone would explain it here. It seems there is a wide confusion about what "canonical" means for various people, because it is sort of a loose term in many subfields. While I acknowledge that there might be some definition in the basement of Alpha Centauri, I don't think that's the best way forward.
2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMay 8th 2016
   • (edited May 8th 2016)
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexJust a quick note: you can write `[[identity type]]` here to make a link to the page [[identity type]].

   Just a quick note: you can write [[identity type]] here to make a link to the page identity type.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeMay 8th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAs for the content of your question, I agree; I think that that usage of "canonical" on the page is actually borderline wrong. To me something is "canonical" when it has already been constructed or defined, and that construction is either unique or has some quality singling it out from other constructions of similar objects. But the J-term here is being *postulated*. From a semantic point of view one might say that it is being *specified* as part of an algebraic structure, but on the syntactic side it is being introduced as a new kind of syntactic entity, not being described or defined in terms of things that already exist. I'm not sure what the best phrasing to use there is, though.

   As for the content of your question, I agree; I think that that usage of “canonical” on the page is actually borderline wrong. To me something is “canonical” when it has already been constructed or defined, and that construction is either unique or has some quality singling it out from other constructions of similar objects. But the J-term here is being postulated. From a semantic point of view one might say that it is being specified as part of an algebraic structure, but on the syntactic side it is being introduced as a new kind of syntactic entity, not being described or defined in terms of things that already exist. I’m not sure what the best phrasing to use there is, though.

4. • CommentRowNumber4.
   • CommentAuthorwhatever
   • CommentTimeMay 8th 2016
   • PermaLink
   Author: whatever
   Format: TextMike, thanks for your reply. I read a part of one of the references and there it doesn't use the phrase. Instead, what it does is that it just defines "J" as a particular type of node in the proof tree, which is completely defined and has no vagueness whatsoever. (This is your "new kind of syntactic identity") I also understand mathematicians like using short identifiers for things, but from a software point of view, J is rather awful. I.e., if someone came to me with a patch introducing something like "J", I would tell them to take a hike. Who actually thinks it is a good idea to use "J"? Just because some dude every introduced "J" doesn't mean we should annoy every student or researcher of the future with this rather ill-conceived name. J should probably be called something like a PathCarrier or something like that, if I understand it correctly. I think "C" is also rather vague in the sense that there really is no such thing as "C", the way I understand it. "C" is a meta-variable, AFAICT. I am also not sure why the "C" (a fairly abstract construct) is being used in the first place. It seems that in the notation used "C" is not specifically marked as such, so technically it's also wrong. If I look at the defined rules, all rules mentioning "C" require a "C" to construct another "C". This would mean that there is actually no way to ever construct a "C". So, either there is some abuse of notation (which IMHO is just wrong) or it is logically flawed as just explained. Why do the people who write these formal systems write down such ... garbage? If I was grading a student who produced this (or the HoTT book for that matter), I would tell her/him to rewrite it, before wasting more of my time. In a properly written article, I would also like to see any reference to any symbol not introduced in the text being accompanied by a reference to a paper (preferably hypertext). For readability, that location would be another article provided by this community. I am happy with this initiative, btw. I can understand the whole "it's a free resource" thing, but at some point in time my tax money also goes towards people writing e.g. the HoTT book and I just think the quality is rather low. I.e., I am not really getting value for money. I don't think many researchers see themselves as providing a service to society, but I would like it if they would do that more. At the same time for every HoTT book there are 80 things produced which are even worse, but still.

   Mike, thanks for your reply.
   
   I read a part of one of the references and there it doesn't use the phrase. Instead, what it does is that it just defines "J" as a particular type of node in the proof tree, which is completely defined and has no vagueness whatsoever. (This is your "new kind of syntactic identity")
   
   I also understand mathematicians like using short identifiers for things, but from a software point of view, J is rather awful. I.e., if someone came to me with a patch introducing something like "J", I would tell them to take a hike. Who actually thinks it is a good idea to use "J"? Just because some dude every introduced "J" doesn't mean we should annoy every student or researcher of the future with this rather ill-conceived name.
   
   J should probably be called something like a PathCarrier or something like that, if I understand it correctly.
   
   I think "C" is also rather vague in the sense that there really is no such thing as "C", the way I understand it. "C" is a meta-variable, AFAICT. I am also not sure why the "C" (a fairly abstract construct) is being used in the first place. It seems that in the notation used "C" is not specifically marked as such, so technically it's also wrong.
   
   If I look at the defined rules, all rules mentioning "C" require a "C" to construct another "C". This would mean that there is actually no way to ever construct a "C". So, either there is some abuse of notation (which IMHO is just wrong) or it is logically flawed as just explained. Why do the people who write these formal systems write down such ... garbage? If I was grading a student who produced this (or the HoTT book for that matter), I would tell her/him to rewrite it, before wasting more of my time.
   
   In a properly written article, I would also like to see any reference to any symbol not introduced in the text being accompanied by a reference to a paper (preferably hypertext). For readability, that location would be another article provided by this community.
   
   I am happy with this initiative, btw. I can understand the whole "it's a free resource" thing, but at some point in time my tax money also goes towards people writing e.g. the HoTT book and I just think the quality is rather low. I.e., I am not really getting value for money. I don't think many researchers see themselves as providing a service to society, but I would like it if they would do that more. At the same time for every HoTT book there are 80 things produced which are even worse, but still.
5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeMay 8th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI agree with you that "J" is a poor name. I think the HoTT book uses $ind_{=}$. However, mathematicians do tend to be somewhat bound by tradition, even if it's suboptimal, and there are some good reasons for that; if everyone was always changing the names and notations then it would be impossible to read anything. Jaap van Oosten said that "the only thing worse than bad terminology is continually changing terminology", and I think he had a point. The type C in the identity elimination does actually exist. It is a metavariable, but that doesn't mean it doesn't exist. Its role is to specify the type of the term being defined. It is introduced by the first hypothesis of identity elimination "for any $x,y:A$ and any reason $p:Id_A(x,y)$ why they are the same, we have a type $C(x,y,p)$"; this is an implicit universal quantification over all such $C$. I don't understand your complaint about 'all rules mentioning "C" require a "C" to construct another "C".' Are you talking about type formation rules? It's true that many type formation rules do require types to make other types, but not all of them; for instance, the unit type, the booleans, the empty type, and the natural numbers are unconditional. If you can provide specific references to "references to symbols not introduced in the text" it would be much more helpful.

   I agree with you that “J” is a poor name. I think the HoTT book uses $ind_{=}$. However, mathematicians do tend to be somewhat bound by tradition, even if it’s suboptimal, and there are some good reasons for that; if everyone was always changing the names and notations then it would be impossible to read anything. Jaap van Oosten said that “the only thing worse than bad terminology is continually changing terminology”, and I think he had a point.

   The type C in the identity elimination does actually exist. It is a metavariable, but that doesn’t mean it doesn’t exist. Its role is to specify the type of the term being defined. It is introduced by the first hypothesis of identity elimination “for any $x,y:A$ and any reason $p:Id_A(x,y)$ why they are the same, we have a type $C(x,y,p)$”; this is an implicit universal quantification over all such $C$.

   I don’t understand your complaint about ’all rules mentioning “C” require a “C” to construct another “C”.’ Are you talking about type formation rules? It’s true that many type formation rules do require types to make other types, but not all of them; for instance, the unit type, the booleans, the empty type, and the natural numbers are unconditional. If you can provide specific references to “references to symbols not introduced in the text” it would be much more helpful.

6. • CommentRowNumber6.
   • CommentAuthorwhatever
   • CommentTimeMay 8th 2016
   • PermaLink
   Author: whatever
   Format: TextYes, I suspected it was a meta-variable (like I said above), but how can I know that by reading those rules (other than that's the only useful interpretation)? I think this stuff is already complicated enough without me having to guess anything. My complaint about "C" has no merit when indeed the meta-variable interpretation is being used. I would like to be able to efficiently consume the work of others such that I have more time to work on my extensions of those ideas.

   Yes, I suspected it was a meta-variable (like I said above), but how can I know that by reading those rules (other than that's the only useful interpretation)?
   
   I think this stuff is already complicated enough without me having to guess anything.
   
   My complaint about "C" has no merit when indeed the meta-variable interpretation is being used.
   
   I would like to be able to efficiently consume the work of others such that I have more time to work on my extensions of those ideas.
7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexActually, it doesn't *have* to be a metavariable: in a type theory with universes, it could be an actual variable that is a type family incarnated as a function into a universe. In fact, the notation $C(x,y,p)$ (rather than simply "$C$" containing variables $x,y,p$) suggests that this is what the author had in mind. The HoTT book is explicit about this (beginning of section 1.12.1). Probably the nLab entry would be improved by being more explicit too. (However, quite a lot of mathematical notation does depend on implicit assumptions and shared context.) If I may make a meta-comment: you are raising potentially valuable suggestions for improvements in exposition, but your entitled-sounding attitude makes it emotionally difficult for me to respond in a productive manner. Keep in mind that the nLab is not a polished exposition like a textbook, and was never intended to be; it's a public lab book. If you walk into a laboratory off the street and open the lab book, you would expect to find abbreviations and notes that wouldn't make sense unless you had the context of the people writing them. We do often try to write nLab pages to be as readable as possible, but that isn't the primary aim.

   Actually, it doesn’t have to be a metavariable: in a type theory with universes, it could be an actual variable that is a type family incarnated as a function into a universe. In fact, the notation $C(x,y,p)$ (rather than simply “$C$” containing variables $x,y,p$) suggests that this is what the author had in mind. The HoTT book is explicit about this (beginning of section 1.12.1). Probably the nLab entry would be improved by being more explicit too. (However, quite a lot of mathematical notation does depend on implicit assumptions and shared context.)

   If I may make a meta-comment: you are raising potentially valuable suggestions for improvements in exposition, but your entitled-sounding attitude makes it emotionally difficult for me to respond in a productive manner. Keep in mind that the nLab is not a polished exposition like a textbook, and was never intended to be; it’s a public lab book. If you walk into a laboratory off the street and open the lab book, you would expect to find abbreviations and notes that wouldn’t make sense unless you had the context of the people writing them. We do often try to write nLab pages to be as readable as possible, but that isn’t the primary aim.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI concur with Mike's last paragraph. We do want to hear about errors or where the nLab is not clear, but if we could put aside expressions of exasperation like "garbage", "wasting more of my time", "my tax money", etc., it would help a lot I think.

   I concur with Mike’s last paragraph. We do want to hear about errors or where the nLab is not clear, but if we could put aside expressions of exasperation like “garbage”, “wasting more of my time”, “my tax money”, etc., it would help a lot I think.