## Stream: maths

### Topic: refactor functor notation

#### Johan Commelin (Jan 17 2019 at 17:50):

Has anyone started the big functor notation search and replace?

#### Mario Carneiro (Jan 17 2019 at 19:25):

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 (Jan 17 2019 at 19:38):

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

#### Mario Carneiro (Jan 17 2019 at 19:40):

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 (Jan 19 2019 at 00:26):

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 (Jan 19 2019 at 00:26):

I don't particularly mind the current functor arrow.

Last updated: May 10 2021 at 06:13 UTC