Commit 2025-06-15 16:58 30eb8769

View on Github →

refactor(CategoryTheory/Monoidal): define Mon_.Hom using type class IsMon_Hom (#25826) This PR changes

structure Mon_.Hom (M N : Mon_ C) where
  hom : M.X ⟶ N.X
  one_hom : η ≫ hom = η := by aesop_cat
  mul_hom : μ ≫ hom = (hom ⊗ hom) ≫ μ := by aesop_cat

to

structure Mon_.Hom (M N : Mon_ C) where
  hom : M.X ⟶ N.X
  [is_mon_hom : IsMon_Hom hom]

and similarly for Comon_.Hom. The discussion on Zulip: #mathlib4 > Refactoring Mod_? @ 💬

Estimated changes

modified def Mon_.id