mathlib

1b4d1eaa - chore(algebra/category/*/colimits): remove unnecessary projections (#1588)

chore(algebra/category/*/colimits): remove unnecessary projections (#1588) * refactor(category_theory,algebra/category): make algebraic categories not [reducible] Adapted from part of #1438. * Update src/algebra/category/CommRing/basic.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * adding missing forget2 instances * Converting Reid's comment to a [Note] * adding examples testing coercions * chore(algebra/category/*/colimits): remove unnecessary projections