cubical icon indicating copy to clipboard operation
cubical copied to clipboard

Published 20 hours ago • verified publisher icon agda

Naming conventions for category theory

Open anuyts opened this issue 2 years ago • 5 comments

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.

anuyts avatar May 17 '22 14:05 anuyts

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 avatar May 21 '22 15:05 mortberg

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

mortberg avatar May 21 '22 15:05 mortberg

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 ?

thomas-lamiaux avatar May 21 '22 23:05 thomas-lamiaux

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?

anuyts avatar May 23 '22 09:05 anuyts

  • 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.

felixwellen avatar May 23 '22 09:05 felixwellen