Commit 2024-05-28 15:30 cec4919a

View on Github →

feat: oplax monoidal functors take comonoids to comonoids (#12858)

depends on: #12856
depends on: #10098

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def CategoryTheory.OplaxMonoidalFunctor.mapComon

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean