Commit 2023-03-24 18:51 429abcae

View on Github →

feat: Port CategoryTheory.Monoidal.NaturalTransformation (#2466)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

added theorem CategoryTheory.MonoidalNatIso.ofComponents.hom_app

added theorem CategoryTheory.MonoidalNatIso.ofComponents.inv_app

added def CategoryTheory.MonoidalNatIso.ofComponents

added theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans

added theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans_lax

added def CategoryTheory.MonoidalNatTrans.hcomp

added def CategoryTheory.MonoidalNatTrans.id

added def CategoryTheory.MonoidalNatTrans.prod

added def CategoryTheory.MonoidalNatTrans.vcomp

added structure CategoryTheory.MonoidalNatTrans

added def CategoryTheory.monoidalCounit

added def CategoryTheory.monoidalUnit