reorganising category_theory/limits/limits.lean

Stream: maths

[Scott Morrison]

I would like to slice category_theory/limits/limits.lean into smaller files, as it has become unwieldy. @Johan Commelin, @Bhavik Mehta, @Markus Himmel, @Reid Barton

The first thing I would like to do is separate out the is_limit stuff from the has_limit stuff (presumably into files with those names). There's also a variety of rarely used API (e.g. equivalent formulations of limit conditions in terms of yoneda) that I might just break into their own files.

The change I'm not sure about is whether to split everything to two sets of parallel files, once for limits, once for colimits.

advantages:

• better parallelism while compiling (or just faster if you only need one side)
• perhaps easier to keep thing in sync by opening the files side by side

disadvantages:

• perhaps harder to keep things in sync by forgetting about the other file...

Happy to follow any expressed preferences here.

[Johan Commelin]

I don't have strong reasons, but I slightly favour the two-files version, I think.

[Bhavik Mehta]

I slightly prefer the one-file version, partially because the splitting might need to happen for special shapes and anything else which uses limits, so I think the maintainability problem could get tough. That said opening the files side by side seems like a good way round this; so I'd be happy with either decision. Obviously though it would be great if we could automatically dualise :)

[Scott Morrison]

I think I might try a compromise: I'll split limits.lean into is_limit.lean, has_limit.lean, is_colimit.lean, has_colimit.lean, but not plan to split the special shapes files into dual pairs.