Zulip Chat Archive

Stream: maths

Topic: reorganising category_theory/limits/limits.lean

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 25 2020 at 05:16):

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

view this post on Zulip 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 :)

view this post on Zulip 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