Short Names or Long Names?

[kangrongji]

Recently I realized that there are many concepts in category theory that they have long names, and they become even longer if one combines them, such as isUnivalentFullSubcategory or isFaithful+isFull→isFullyFaithful. Short names or abbreviations look cleaner at first sight, but abuse of them may cause confusion and make proofs hard to understand. Especially when the names contains several abbreviations, it becomes very difficult to read.

Soon or later one will encounter such problems, and it's definitely not restricted to category theory. The current naming convention does not fully address this problem. In Cubical/NAMING.md, it encourages using of abbreviations but only involves simple words. In Cubical/Algebra/NAMING.md, it only settles abbreviations for some common properties for algebra. So what is your opinion? Do we need to set up standards on using of short/long names and abbreviations?

Relevant to #646.

[thomas-lamiaux]

For Algebra, this du to a recent effort that is not finished to clean it.
For instance the naming is a few months ald and was just enforced last week. for algebraic structure
Also there is still an issue about reorganizing the inner structure of Algebra folders to do.

The same would be needed for Category, so naming + organization.
I think we talked about doing once Algebra is done ?
So maybe two issues should be opened for those two specific and larger subject ?

[kangrongji]

Do you mean to deal with Algebra and Category separately? That's Ok. But also I hope there could be a general standard for the whole (at least most of the) library, since it's a problem beyond just Algebra or Category.

[thomas-lamiaux]

No I meant having an issue about refactoring Category and one about defining naming conventions or category.

It don't really see how it is possible to define a general standard on naming convention for different part of mathematics.

For instance long names, sometimes there are better sometimes not, I personally think it should be left to the author with possible convention depending on the folder / subject

[kangrongji]

All right. Btw, there has been an issue about naming for Category #803.

[anuyts]

I would prefer to use long names. Shorter names can be assigned locally in files that use a concept extensively.
Most important is consistency.