Commit 2023-10-17 07:52 1323ee53

feat: MonoidalCategory (QuadraticModuleCat R) (#7244) Together with #7130, this now results in a CommMonoid (Skeleton (QuadraticModuleCat R)), which is similar to the multiplicative part of the Grothendieck-Witt ring of quadratic forms. (Strictly the Grothendieck-Witt ring would introduce a subcategory of QuadraticModuleCat for the non-singular forms) This is largely a copy-and-paste from #7598 (though it was written first)