The natural monoidal structure on any category with finite (co)products. #
A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category, although this is also sometimes used to mean a finitely complete category. (See https://ncatlab.org/nlab/show/cartesian+category.)
As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.
We had previously chosen to rely on
HasBinaryProducts instead of
HasBinaryProducts, because we were later relying on the definitional form of the tensor product.
has_limit has been refactored to be a
this issue is irrelevant and we could simplify the construction here.
CategoryTheory.monoidalOfChosenFiniteProducts for a variant of this construction
which allows specifying a particular choice of terminal object and binary products.
A category with a terminal object and binary products has a natural monoidal structure.
A category with an initial object and binary coproducts has a natural monoidal structure.