refactor functor notation

Stream: maths

[Johan Commelin]

Has anyone started the big functor notation search and replace?

[Mario Carneiro]

I'm not sure this is a good idea. The big arrow seems to be used in multiple contexts, so perhaps we shouldn't have any global notation for it at all, and use local notations instead. The broken right arrow has the advantage that it is an unusual arrow, so I'm more okay with stealing it as a global notation (making it unusable for other purposes).

[Patrick Massot]

Why do we need to have any global notation for this?

[Mario Carneiro]

We don't, I guess, but then we would have to preface lots of category theory files with local notation declarations, and the category theory library has quite a few notations. @Reid Barton @Scott Morrison ?

[Scott Morrison]

I'm not too concerned. I'd prefer a tiny bit that we don't use local notations in every file, just because this seems likely to result in fragmentation as different people start to use different arrows.

[Scott Morrison]

I don't particularly mind the current functor arrow.