Expliciteness of binders in `Functor.associator`

Stream: mathlib4

[Robin Carlier]

With the discussion in #mathlib4 > whiskeringRight, today seems to be a good day to raise some questions about the notations in mathlib’s category theory corner.

I have the feeling that I always write Functor.associator _ _ _ and leave it to lean to fill in the blanks, and that’s a pattern I’ve also seen lot in the library. At some point, I even had a register in neovim dedicated to storing Functor.associator _ _ _ to avoid typing it all the time.

So I tried to run a quick count, and if my unix-fu is correct, running

$rg "Functor.associator _ _ _" -co | awk -F ":" '{ sum +=$2} END {print sum}'

in Mathlib/CategoryTheory should count how many time this pattern appears, and running

rg "Functor.associator (\S+) (\S+) (\S+)" -co | awk -F ":" '{ sum +=$2} END {print sum}'

should give a rough estimate of how many time we call an associator.

179/200 Functor.associator calls are of the form Functor.associator _ _ _. Maybe this means we might want to reconsider expliciteness of the binders? or introduce a macro/abbrev that would save us from typing this all the time?

[Joël Riou]

If we do this, we should do it also for monoidal categories and bicategories... (Three refactors for the price of one!)

[Christian Merten]

I personally find it occasionally useful to see the arguments of the various associators (and unitors) in the infoview and I find typing _ _ _ not very burdensome. Alternatively there could be a delaborator that can be switched on during development that shows the arguments.

[Yuma Mizuno]

Personally, I sometimes find it annoying at output in the sense that arguments of associators shown on the right panel in VS Code could be very long but is not very helpful.