Commit 2019-05-04 20:01 b4d483e2

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