Commit 2023-06-09 00:56 3b8ea355

View on Github →

feat: port CategoryTheory.Monoidal.Mod_ (#4866)

Estimated changes

added structure Mod_.Hom
added theorem Mod_.assoc_flip
added def Mod_.comap
added def Mod_.comp
added theorem Mod_.comp_hom'
added def Mod_.forget
added theorem Mod_.hom_ext
added def Mod_.id
added theorem Mod_.id_hom'
added def Mod_.regular
added structure Mod_