[Merged by Bors] - chore(category_theory/limits/preserves): split up files and remove redundant defs #4717
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Broken off from #4163 and #4716.
While the diff of this PR is quite big, it actually doesn't do very much:
preserves_(co)limits_iso
frompreserves/basic
, since there's already a version inpreserves/shapes
which has lemmas about it. (I didn't keep them inpreserves/basic
since that file is already getting quite big, so I chose to instead put them into the smaller file.preserves/shapes
into two files:preserves/limits
andpreserves/shapes
. From my other PRs my plan is forshapes
to contain isomorphisms and constructions for special shapes, egfan.mk
andfork
s, some of which aren't already present, andlimits
to have things for the general case. In this PR I don't change the situation for special shapes (other than simplifying some proofs), other than moving it into a separate file for clarity.