whiskeringRight

Stream: mathlib4

[Calle Sönne]

Should docs#CategoryTheory.whiskeringRight be called postcomposing? This is a lot less confusing to me (very clear even for a non category theory expert!). This is also what it is called for bicategories docs#CategoryTheory.Bicategory.postcomposing

[Calle Sönne]

If there are no objections I will try to get this changed

[Calle Sönne]

Actually even the description says "Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))"

[Robin Carlier]

I would say postcomposition or postcompose would be even better than postcomposing (for the latter, this would also align with CategoryTheory.Functor.postcompose₂ and CategoryTheory.Functor.postcompose₃), but I’m no maintainer.

[Joël Riou]

I personaly would not mind, especially as I defined CategoryTheory.Functor.postcompose₂ in the case of bifunctors. Still, that might induce a lot of name changes... I would like to know the opinion of @Kim Morrison!

[Kim Morrison]

Yes, happy if someone gets rid of all "whiskering" names.

[Calle Sönne]

Perfect! I will do that then :)

[Thomas Murrills]

If this is an appropriate place to discuss other potential changes to whiskering, I'm curious how people would feel about making the category arguments implicit.

It seems fairly common to see whiskeringRight _ _ _ in practice (especially outside of the base file with theorems about whiskeringRight itself), and when I do see whiskeringRight A B C, it's often not immediately obvious to me which role the categories A, B, and C have anyway. postcompose.obj F seems nicer if we can get away with it. :)

[Calle Sönne]

Thomas Murrills said:

If this is an appropriate place to discuss other potential changes to whiskering, I'm curious how people would feel about making the category arguments implicit.

It seems fairly common to see whiskeringRight _ _ _ in practice (especially outside of the base file with theorems about whiskeringRight itself), and when I do see whiskeringRight A B C, it's often not immediately obvious to me which role the categories A, B, and C have anyway. postcompose.obj F seems nicer if we can get away with it. :)

I am a bit skeptical since last year I went around making pullback.fst have explicit arguments (see #mathlib4 > Implicit parameters in `pullback.fst` and `pullback.snd`). Partly this was due to readability but I think there were quite a few awkward instances of (pullback.fst : pullback f g ⟶ _) as well.

I think for the order of the arguments I remember it as "the functors go from left to right". Then once the naming has been hanged to postcompose/ing I think this makes it easier to see what it is referring to.

[Calle Sönne]

Or possibly we could try making only one of the arguments explicit (i.e. the one not determined by F). Then we would have (postcompose A).obj F. This is more readable imo, although slightly more awkward to state.