Commit 2025-07-28 06:06 29bdc6fc

chore(CategoryTheory/Monoidal): unify mkIso (#27126) Previously, mkIso and mkIso' meant different things across the various types of objects. Now:

• mkIso' takes in elements X, Y of the underlying category C, an isomorphism e : X ≅ Y and a typeclass assumption [IsMon_Hom e.hom] and returns mk X ≅ mk Y,
• mkIso is an abbrev for mkIso', taking in elements X, Y of Obj C, an isomorphism e : X.X ≅ Y.X and the proof fields of IsMon_Hom e.hom and returns X ≅ Y. From Toric