How to name functors

[Alizter]

Should we decide on a convention for functors and stick with it? In #1143 we are opting for X_2functor so naturally X_functor would make sense as a name. However, currently there are various things called functor_X.

Changing these to X_functor will have a few advantages:

• We have a homogeneous naming scheme so we don't have to recall which version is which
• We can easily search for things related to the underlying type. For instance, when chaining equivalences together I very often find myself writing equiv_sigma_ and expecting the functor lemmas to come up, but they won't since they are named equiv_functor_.
• Higher functorial actions can be named similarly as proposed in #1143. Notice that 2functor_X is not a valid name (accepted by coq).

[mikeshulman]

In equiv_functor_sigma the equiv was originally considered to go with the functor (it is "functoriality on sigmas"), so I'm not sure that splitting them up into equiv_sigma_functor makes sense. But I suppose you could view the latter as "an equivalence built from sigma_functor?

[Alizter]

Yes, when I read equiv_sigma_functor I see an equiv made from sigma_functor.

[mikeshulman]

Sure, I could live with that. But we could also regard "functoriality on equivalences" as another kind of functoriality, and write something like sigma_efunctor.