The doctrines for monoidal categories in the standard library are all expressed in multiplicative ("\otimes") rather than additive ("\oplus") notation. These doctrines should be supplemented with doctrines for "additive" monoidal categories, for two reasons:
Structures with two monoidal products, one "additive" and the other "multiplicative", show up fairly often, for example in distributive monoidal categories, including as a special case distributive bicategories of relations.
In certain situations, it is essential to use the additive notation. For instance, it would be abominable to write the monoidal product in graphical linear algebra (the direct sum) using the tensor product symbol.
A quick solution is to copy-paste the existing doctrine for monoidal categories and just change the notation. In defense of this hacky proposal, I will just say that dealing with context-dependent notation is trivial in pen-and-paper mathematics but not in mathematical software. For example, as Thomas Hales points out in his blunt review, the Lean theorem prover has the same problem of "structure depending on notation" (further discussion at the nForum).
epatters
commented
4 years ago
The doctrines for monoidal categories in the standard library are all expressed in multiplicative ("\otimes") rather than additive ("\oplus") notation. These doctrines should be supplemented with doctrines for "additive" monoidal categories, for two reasons:
Structures with two monoidal products, one "additive" and the other "multiplicative", show up fairly often, for example in distributive monoidal categories, including as a special case distributive bicategories of relations.
In certain situations, it is essential to use the additive notation. For instance, it would be abominable to write the monoidal product in graphical linear algebra (the direct sum) using the tensor product symbol.
A quick solution is to copy-paste the existing doctrine for monoidal categories and just change the notation. In defense of this hacky proposal, I will just say that dealing with context-dependent notation is trivial in pen-and-paper mathematics but not in mathematical software. For example, as Thomas Hales points out in his blunt review, the Lean theorem prover has the same problem of "structure depending on notation" (further discussion at the nForum).