mathlib3

b4d483e2 - feat(colimits): arbitrary colimits in Mon and CommRing (#910)

feat(colimits): arbitrary colimits in Mon and CommRing (#910) * feat(category_theory): working in Sort rather than Type, as far as possible * missed one * adding a comment about working in Type * remove imax * removing `props`, it's covered by `types`. * fixing comment on `rel` * tweak comment * add matching extend_π lemma * remove unnecessary universe annotation * another missing s/Type/Sort/ * feat(category_theory/shapes): basic shapes of cones and conversions minor tweaks * Moving into src. Everything is borked. * investigating sparse * blech * maybe working again? * removing terrible square/cosquare names * returning to filtered colimits * colimits in Mon * rename * actually jump through the final hoop * experiments * fixing use of ext * feat(colimits): colimits in Mon and CommRing * fixes * removing stuff I didn't mean to have in here * minor * fixes * merge * update after merge * fix import