mathlib

7848f28d - feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562)

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) Verifying that internal monoid objects in Type are the same thing as bundled monoid objects. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>