Naming conventions for category theory

anuyts commented 2 years ago

A few things for which there do not seem to be conventions:

How to name categories (in practice, their names currently generally seem to end in Category, although all-caps names are also found),
How to name functors (currently anything starting with a capital)
How to name natural transformations
How to name homomorphisms.

mortberg commented 2 years ago

Yes, we should have naming conventions for CategoryTheory similar to those we recently added for Algebra:

https://github.com/agda/cubical/blob/master/Cubical/Algebra/NAMING.md

mortberg commented 2 years ago

Anyone is very welcome to contribute a suggestion in a PR and we can then discuss it further

thomas-lamiaux commented 2 years ago

We were just talking about it. We have decided convention for Algebra and for some stuff in the general library but not for Category. The entire folder should also be cleaned. For instance there is a folder Functor and one called Functors. I think that @mzeuner have some comment about that ?

anuyts commented 2 years ago

We can discuss here, would a pull-request facilitate discussion?

I guess it would be in line with the rule

An instance of an algebraic structure should include the name of the structure. For example UnitGroup and ℤGroup.

to have functors end in Functor, natural transformations in NatTrans and algebra homomorphisms ending in Hom, e.g. group homomorphisms in GroupHom. On the other hand, this leads to very long names. I think the following exceptions are worthwhile:

Functors should simply have function-like names starting with a capital, adding Functor for clarity if needed (e.g. I called the Hom functor HomFunctor),
For natural transformations, we should allow lower case Greek letters e.g. η and μ for monadic unit and multiplication.
I haven't been working with the algebra libraries much. Is adding GroupHom, RingHom etc outrageous?

felixwellen commented 2 years ago

I haven't been working with the algebra libraries much. Is adding GroupHom, RingHom etc outrageous?

No - that is actually how types of Homs are named right now. So I would like it, when they are named the same in the Category-part of the library.

agda / cubical

Naming conventions for category theory #803