Commit 2023-06-07 05:59 e95a1363

View on Github →

feat: port CategoryTheory.Monoidal.Mon_ (#4763)

Estimated changes

added structure Mon_.Hom
added theorem Mon_.assoc_flip
added def Mon_.comp
added theorem Mon_.comp_hom'
added theorem Mon_.ext
added def Mon_.forget
added def Mon_.id
added theorem Mon_.id_hom'
added def Mon_.isoOfIso
added theorem Mon_.mul_associator
added theorem Mon_.mul_leftUnitor
added theorem Mon_.mul_one_hom
added theorem Mon_.mul_rightUnitor
added theorem Mon_.one_associator
added theorem Mon_.one_leftUnitor
added theorem Mon_.one_mul_hom
added theorem Mon_.one_rightUnitor
added def Mon_.trivial
added structure Mon_