Commit 2025-07-25 19:55 67bb55a5

feat(CategoryTheory/Monoidal/Opposites): monoid objects internal to the monoidal opposite (#25854) We construct an equivalence between monoid objects internal to a monoidal category C, and monoid objects internal to its monoidal opposite Cᴹᵒᵖ. This is done by adding Mon_Class and IsMon_Hom instance to the relevant objects, as well as by recording an explicit equivalence of categories Mon_ C ≌ Mon_ Cᴹᵒᵖ.