# Commit 2020-07-28 15:30 7848f28d

View on Github →feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) Verifying that internal monoid objects in Type are the same thing as bundled monoid objects.

Mathlib v3 is deprecated. Go to Mathlib v4

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) Verifying that internal monoid objects in Type are the same thing as bundled monoid objects.