Commit 2020-10-21 00:42 857cbd52

chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717) Broken off from #4163 and #4716. While the diff of this PR is quite big, it actually doesn't do very much:

• I removed the definitions of preserves_(co)limits_iso from preserves/basic, since there's already a version in preserves/shapes which has lemmas about it. (I didn't keep them in preserves/basic since that file is already getting quite big, so I chose to instead put them into the smaller file.
• I split up preserves/shapes into two files: preserves/limits and preserves/shapes. From my other PRs my plan is for shapes to contain isomorphisms and constructions for special shapes, eg fan.mk and forks, some of which aren't already present, and limits 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.