Develop/implement consistent naming conventions for `Categories` and `Algebra`

[barrettj12]

The Algebra and Categories libraries are expanding, with many different authors adding new structures and instances thereof. This presents a problem of inconsistent naming between different structures and instances.

@mortberg says in #636:

... the name of Set and functor categories currently doesn't follow any convention either. We also have instances for algebraic structures that follow different conventions... We should decide for a convention and rename all of these consistently.

I think this problem is probably more severe in the Categories library.

• There doesn't seem to be an established convention for instances (in Categories.Instances). We have CommRingsCategory as well as SET and FUNCTOR.
• There's also a mismatch between module names and the main definitions they export, e.g. the NaturalTransformation module exports NatTrans and NatIso.

But, for example, there doesn't seem to be a convention for instances of algebraic structures either.

Personally, I'm in favour of using the short, conventional, boldface names of categories where they exist (Set, Grp, Ring, Cat, Ab, etc). I think the CommRingsCategory convention is unnecessarily verbose - I'd rather see it called CRing as it usually is in writing. Though maybe for categories of algebraic structures, there should be a connection to the name of the structure in Algebra.

Also, is Cat an acceptable abbreviation of Category? E.g. AbelianCat, MonoidalCat, EnrichedCat. How much abbreviation do we allow - if I define strict monoidal categories, should this be called StrictMonoidalCategory, StrictMonoidalCat, StrictMonCat, StrMonCat, ...?

[kangrongji]

My opinion is that abbreviation in library could cause confusion and naming conflict. So I prefer Mörtberg‘s suggestion that we should not use too much abbreviation and anyone needing short names can rename them in their own files.

Maybe we can use other fonts to emphasize being a category like we do in math texts. Does 𝒢𝓇ℴ𝓊𝓅 look better or not？

[barrettj12]

My opinion is that abbreviation in library could cause confusion and naming conflict.

Sure, that's a valid concern. Although, we already use a lot of abbreviations and I don't think this causes ambiguity or conflict - see AbGroup, CommRing, NatTrans, isIso. Also I can't imagine Cat being used as an abbreviation for anything but Category.

Maybe we can use other fonts to emphasize being a category like we do in math texts. Does 𝒢𝓇ℴ𝓊𝓅 look better or not？

Nice idea, but unfortunately I think that cursive font is barely readable. Unicode does provide some mathematical bold fonts e.g. 𝗚𝗿𝗼𝘂𝗽, but I'm not sure if digging so deep into Unicode is a good idea.

[mortberg]

I agree, let's not go down the rabbit hole of Unicode fonts... I already have trouble reading some symbols in the library in my browser (yes, I can probably sort that out, but I don't have time or energy to deal with font issues...)