Setting source and target to the underlying categories of the corresponding monoidal structures leads to issues, whose description is too long to fit here. Monoidal functors should instead have source and target free (with bound AnyCategory), and the monoidal structures be defined on them.
Setting source and target to the underlying categories of the corresponding monoidal structures leads to issues, whose description is too long to fit here. Monoidal functors should instead have source and target free (with bound AnyCategory), and the monoidal structures be defined on them.