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.

Implementation #

We had previously chosen to rely on has_terminal and has_binary_products instead of has_finite_products, because we were later relying on the definitional form of the tensor product. Now that has_limit has been refactored to be a Prop, this issue is irrelevant and we could simplify the construction here.

See category_theory.monoidal.of_chosen_finite_products for a variant of this construction which allows specifying a particular choice of terminal object and binary products.