Commit 2021-03-18 13:48 744d59af

refactor(category_theory/limits): split file (#6751) This splits category_theory.limits.limits into category_theory.limits.is_limit and category_theory.limits.has_limits. It doesn't meaningfully reduce imports, as everything imports has_limits, but in principle it could, and hopefully it makes the content slightly easier to understand when separated. In any case, the file was certainly too large.