Commit 2019-10-22 08:36 1b4d1eaa
View on Github →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