Spelling and style changes

[patrick-nicodemus]

This is a pretty boring and mundane PR which entirely deals with comments. We:

• fix some typos
• make some stylistic changes to comments
• change some comments to Coqdoc comments
• add [-] around some identifiers in comments so that Coqdoc renders them properly
• adds a few new comments

My apologies if reviewing a bunch of typos seems more work than it's worth.

There are a few issues which I didn't want to put in this PR because it's already very large and these issues are more subjective and require some discussion. However if they are requested I can do these things too.

• In some files (like Truncations/Core.v), paper abbreviations (like CORS) are used without explanation. Maybe there should be a comment at the top of each file introducing the acronyms used? I did this in one file.
• I feel that this comment is unclear and needs to be rewritten. I don't think the term "homwise" is helpful for me.

  Coq-HoTT/theories/WildCat/Core.v

  Line 245 in 239bcf4

  (** Generalizing function extensionality, "Morphism extensionality" states that homwise [GpdHom_path] is an equivalence. *)

• Should funext be capitalized everywhere?
• Spelling: hprop, hProp or HProp? Is it a big deal if this is consistent? Similarly with hset/hSet
• Stylistically, should we capitalize objects named after people? Abelian group vs abelian group, Cartesian product vs cartesian product. In both of these cases I prefer the capital style.
• A few references in the code to "Homomorphic properties", "homomorphic image", etc. I think the word "homomorphic" is uncommon. Does it mean something other than "relating to homomorphisms"? I think we could use a better word here.
• The file on ring ideals refers to "coprimeness" and "coprimality". It would be better to pick one term and stick to it, maybe?
• I have no idea what this comment means.

  Coq-HoTT/theories/HIT/Flattening.v

  Line 149 in 239bcf4

  (** ...but if we define it diindly, then it's easier to reason about. *)

• The terms "coherentification, coherentified, coherentifiable" appear in the comments in a few places and I think this is vague enough that it needs some explication.
• Is "typally" a common term, as in "typal computation"? It's not a bad coinage but maybe we should use a more common word.

Some American / British spelling inconsistencies I saw in the code: should these be standardized?

• cancelling vs canceling (American English)
• axiomatisation / axiomatization
• specialised / specialized
• hypothesise / hypothesize
• characterize / characterise
• generaliz* / generalis* (generalize, generalization)
• fiber / fibre
• flavour / flavor
• among / amongst
• behavior / behaviour
• normalised / normalized
• judgemental equality / judgmental equality
• uniqueness / unicity (I'm not even sure this is British, unicity is a very obscure word to me)
• parameterize / parametrize

Redundancy issues: Some comment blocks are copypasted several times across many files. I can understand why you would want the documentation to be right there when you're reading the file, but block copypasting the same comment across several files or lines in the same file doesn't seem good. Could we centralize some of this documentation in a README or other file and just point back to it? Just a couple quotes I noticed appearing more than once, if you search for these you'll see a few files that contain the same paragraph:

• We don't want to make UTF-8 notations the default, so we don't export them.
• that's Unicode.
• Quoting David Spivak
• work around bug #5567
• Dwyer and Spalinski
• Coq produces phantom universes

I think some comments are Coqdoc comments which should not be Coqdoc comments. I think TODO's or complaints like 'This is broken because of Coq bug so-and-so, so I had to do this weird hack to get around it.' are better off as inline comments than doc comments because they're not relevant to you unless you're actively working on the code and trying to understand it or maintain it.

Last, there is a good amount of dead, commented-out-code in the library which could be deleted if it is no longer being used as an illustrative example or planning to be uncommented soon.

[Alizter]

My apologies if reviewing a bunch of typos seems more work than it's worth.

Not at all. Such improvements are always welcome.

There are a few issues which I didn't want to put in this PR because it's already very large and these issues are more subjective and require some discussion. However if they are requested I can do these things too.

• In some files (like Truncations/Core.v), paper abbreviations (like CORS) are used without explanation. Maybe there should be a comment at the top of each file introducing the acronyms used? I did this in one file.

Yes, this is something we can sort out in perhaps another PR since there are a few ways to go about this. One option is to write a description in the header and yet another is do collect a bibliography. As time goes on, we will formalise more and more papers and not just the HoTT book, so it might make sense to keep track of extra reading material.

• I feel that this comment is unclear and needs to be rewritten. I don't think the term "homwise" is helpful for me.

  Coq-HoTT/theories/WildCat/Core.v

  Line 245 in 239bcf4

  (** Generalizing function extensionality, "Morphism extensionality" states that homwise [GpdHom_path] is an equivalence. *)

Pointwise = between points so homwise is between homs. Feel free to suggest an improvement however.

• Should funext be capitalized everywhere?

I think in HoTT vernacular funext is pretty standard. The reason we might capitalize it is to literally mean the term.

• Spelling: hprop, hProp or HProp? Is it a big deal if this is consistent? Similarly with hset/hSet

I prefer hprop in vernacular. I don't know if we use hProp anywhere. The type of hprops is called HProp.

• Stylistically, should we capitalize objects named after people? Abelian group vs abelian group, Cartesian product vs cartesian product. In both of these cases I prefer the capital style.

Abel is a funny one in mathematics since it is one of those names that is commonly not capitlised. I think maybe the same for "cartesian". I think for types we have a clear captilisation convention in STYLE.md, but in everyday mathematical vernacular, especially in comments, I would prefer being closer to source material. So if a paper writes Abelian or abelian, then its fine to keep convention with that.

• A few references in the code to "Homomorphic properties", "homomorphic image", etc. I think the word "homomorphic" is uncommon. Does it mean something other than "relating to homomorphisms"? I think we could use a better word here.

I think "homomorphic image" is really "image of a homomorphism". Not sure about the other usage however. I will need to look up some literature on that usage, I think it is a bit old-fashioned.

• The file on ring ideals refers to "coprimeness" and "coprimality". It would be better to pick one term and stick to it, maybe?

I think the latter is the correct one to pick.

• I have no idea what this comment means.

  Coq-HoTT/theories/HIT/Flattening.v

  Line 149 in 239bcf4

  (** ...but if we define it diindly, then it's easier to reason about. *)

This file is essentially in a cemetery now. The results on flattening have all been moved to their appropriate files. I wouldn't spend time improving it.

As for the meaning, I can't grok what it was meant to be. I would guess "non-dependently" fits better.

• The terms "coherentification, coherentified, coherentifiable" appear in the comments in a few places and I think this is vague enough that it needs some explication.

I think it would depend on the context. If you can point to some uses, maybe we can give some better comments.

• Is "typally" a common term, as in "typal computation"? It's not a bad coinage but maybe we should use a more common word.

I've seen it used in type theoretic literature. It's not super common. Something like "computes at the type level" or "computation at the type level" is perhaps clearer.

Some American / British spelling inconsistencies I saw in the code: should these be standardized?

• cancelling vs canceling (American English)
• axiomatisation / axiomatization
• specialised / specialized
• hypothesise / hypothesize
• characterize / characterise
• generaliz* / generalis* (generalize, generalization)
• fiber / fibre
• flavour / flavor
• among / amongst
• behavior / behaviour
• normalised / normalized
• judgemental equality / judgmental equality
• uniqueness / unicity (I'm not even sure this is British, unicity is a very obscure word to me)
• parameterize / parametrize

We always prefer American English spellings, but due to being British, some of my Britishisms (and others) may have slipped in. Feel free to fix as you see them. Unicity is an uncommon word, but I think it might be old-fashioned. I don't mind using "uniqueness" instead.

Redundancy issues: Some comment blocks are copypasted several times across many files. I can understand why you would want the documentation to be right there when you're reading the file, but block copypasting the same comment across several files or lines in the same file doesn't seem good. Could we centralize some of this documentation in a README or other file and just point back to it? Just a couple quotes I noticed appearing more than once, if you search for these you'll see a few files that contain the same paragraph:

We need to tackle these on a case-by-case basis.

• We don't want to make UTF-8 notations the default, so we don't export them.

These are specific to the category theory library. I think its fine to keep them as it is to remind the reader why a certain choice was made. Having this consolidated elsewhere would be difficult to see or find.

• that's Unicode.

This seems to be a different comment in both places.

• work around bug #5567
  I think this is fine to keep around, especially if it appears in multiple places. When we check bugs are fixed, find can find all the places we included a workaround.

• Quoting David Spivak
• Dwyer and Spalinski

I think this is fine, since it is paraphrasing a specific book. Again with the bibliography idea above, it might be worth including the book in a bibliography too. Not a top priority.

• Coq produces phantom universes

I prefer to keep this comment, as it is really a TODO for cleaning up these workarounds. At some point we need to remove these universe workarounds as they should have long been fixed.

I think some comments are Coqdoc comments which should not be Coqdoc comments. I think TODO's or complaints like 'This is broken because of Coq bug so-and-so, so I had to do this weird hack to get around it.' are better off as inline comments than doc comments because they're not relevant to you unless you're actively working on the code and trying to understand it or maintain it.

I may be wrong, but I think at the moment, bot inline and coqdoc comments appear in the documentation. It may be better for TODOs to be inline, but then again sometimes its important for the reader of the docs too.

Last, there is a good amount of dead, commented-out-code in the library which could be deleted if it is no longer being used as an illustrative example or planning to be uncommented soon.

This needs to be handled on a case-by-case basis. Some code was ported from elsewhere and is dead, that can be removed. Some code is unfinished and is really a TODO with rich information. Others are just workaround due to some Coq bug that need to be addressed and readded. It really depends.

[Alizter]

Wow! Thanks for taking this on. It really shows how easy it is to miss blatant spelling mistakes.

I think around 60% of them were mine, which isn't surprising.

I've left some comments, but there is a lot to go through. Once you've finished addressing them I'll try to do another pass.

[Alizter]

I did not know this was a word and a common spelling mistake.

[Alizter]

As I mentioned before, I'm unsure about how the name should be. Just so we can keep track of that I'll mention it.

[jdchristensen]

yet another is to collect a bibliography.

I like this idea (in another PR).

• Stylistically, should we capitalize objects named after people? Abelian group vs abelian group, Cartesian product vs cartesian product. In both of these cases I prefer the capital style.

Both forms are commonly used, and I don't think it's necessary to enforce a standard form.

• A few references in the code to "Homomorphic properties", "homomorphic image", etc. I think the word "homomorphic" is uncommon. Does it mean something other than "relating to homomorphisms"? I think we could use a better word here.

I agree that it's uncommon and old fashioned, and can be removed. "image" is fine. "Properties of homomorphisms". Etc. But not a big deal.

• Is "typally" a common term, as in "typal computation"? It's not a bad coinage but maybe we should use a more common word.

I've seen it used in type theoretic literature. It's not super common. Something like "computes at the type level" or "computation at the type level" is perhaps clearer.

"Typal" was introduced to replace "propositional equality" with "typal equality", since the equality types aren't necessarily propositions. I don't think it really caught on, but that's probably the source of this work in the library. It's fine to replace it with something more clear.

Some American / British spelling inconsistencies I saw in the code: should these be standardized?

To make it worse, Canadian spelling is a mix of the two... I don't think we need to go through and standardize. That's just work without little benefit. But I think we should standardize on American English for identifiers.

• uniqueness / unicity (I'm not even sure this is British, unicity is a very obscure word to me)

I've seen "unicity" used more and more lately, but I don't like it.

Redundancy issues: Some comment blocks are copypasted several times across many files.

I agree with Ali that this would depend on the situation. I don't might duplicated comments now and then, as they can be very helpful to the reader.

I think some comments are Coqdoc comments which should not be Coqdoc comments. I think TODO's or complaints like 'This is broken because of Coq bug so-and-so, so I had to do this weird hack to get around it.' are better off as inline comments than doc comments because they're not relevant to you unless you're actively working on the code and trying to understand it or maintain it.

I may be wrong, but I think at the moment, bot inline and coqdoc comments appear in the documentation.

Ali is right, all comments appear in the documentation. And I think that's fine. But it's probably best to use (* for TODO items, so they are less highlighted.

For things I didn't comment on, I agree completely with Ali.

I haven't looked at the PR changes, but I think it's most important to fix actual errors, and not worry about being too pedantic about consistency. The library has had many authors, and will hopefully have many more.

[jdchristensen]

• I have no idea what this comment means.

  Coq-HoTT/theories/HIT/Flattening.v

  Line 149 in 239bcf4

  (** ...but if we define it diindly, then it's easier to reason about. *)

"but if we define it diindly ..." should be "but if we define it directly ..." Someone did a search and replace "rect" -> "ind" that went awry.

[jdchristensen]

Thanks for this! I approve, once the minor suggestions are taken in to account.

[patrick-nicodemus]

All comments directly relating to the changes have been addressed. I have not taken any actions regarding the miscellaneous other items I brought up in the original post.