Braided and symmetric monoidal natural transformations (and isomorphisms) are really just monoidal natural transformations (and isomorphisms). But the extra wrappers in this PR seem necessary if one wants to define e.g. symmetric monoidal natural transformations without Agda going into some unification rabbit hole where it takes ages to type check even quire simple definitions. Even with the wrapper performance has been bad in some of my WIP code. I'm not sure what exactly is causing the problem though. See some of the comments in the code of this PR for (possibly?) related issues.
More boilerplate.
Braided and symmetric monoidal natural transformations (and isomorphisms) are really just monoidal natural transformations (and isomorphisms). But the extra wrappers in this PR seem necessary if one wants to define e.g. symmetric monoidal natural transformations without Agda going into some unification rabbit hole where it takes ages to type check even quire simple definitions. Even with the wrapper performance has been bad in some of my WIP code. I'm not sure what exactly is causing the problem though. See some of the comments in the code of this PR for (possibly?) related issues.