## Stream: maths

### Topic: reorganising category_theory/limits/limits.lean

#### Scott Morrison (Sep 25 2020 at 04:46):

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.

• 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

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

Happy to follow any expressed preferences here.

#### Johan Commelin (Sep 25 2020 at 05:16):

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

#### Bhavik Mehta (Sep 25 2020 at 13:30):

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 (Sep 26 2020 at 01:29):

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.

Last updated: May 18 2021 at 06:15 UTC