mathlib3

02b492ab - feat(category_theory/Mon): Mon_ C has limits when C does (#4133)

feat(category_theory/Mon): Mon_ C has limits when C does (#4133) If `C` has limits, so does `Mon_ C`. (This could potentially replace many individual constructions for concrete categories, in particular `Mon`, `SemiRing`, `Ring`, and `Algebra R`.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>