Commit 2019-08-20 23:38 26a3e31d
View on Github →chore(category_theory/monoidal): monoidal_category doesn't extend category (#1338)
- chore(category_theory/monoidal): monoidal_category doesn't extend category
- remove _aux file, simplifying
- make notations global, and add doc-strings