Add symmetric monoidal categories

[ScriptRaccoon]

This PR implements symmetric monoidal categories and thus resolves #318.

Features

As for other categorical structures, users can switch to symmetric monoidal categories, view examples and properties of symmetric monoidal categories, look for implications, and perform property combination searches and comparisons.

Added symmetric monoidal categories

• $(Set,\times,1)$
• $(Set,\sqcup,0)$
• $(Cat,\times,1)$
• $(Top,\times,1)$
• $(\mathbb{N},\leq,+,0)$
• $(Ab,\otimes,\mathbb{Z})$
• $(Ab_{fg},\otimes,\mathbb{Z})$
• $(R{-}Mod,\otimes,R)$ (when $R$ is a non-zero commutative ring)
• $(R{-}Mod,\otimes,R)$ (when $R$ is absolutely flat)
• $(R{-}Mod,\otimes,R)$ (when $R$ is not absolutely flat)
• $(FinVect_K,\otimes,K)$
• $(1,\times,0)$

There are the following parent-child relationships (cf. #323):

• $(Ab,\otimes,\mathbb{Z})$ is a child of $(R{-}Mod,\otimes,R)$ where $R$ is not absolutely flat
• $(R{-}Mod,\otimes,R)$ (where $R$ is absolutely flat) and $(R{-}Mod,\otimes,R)$ (where $R$ is not absolutely flat) are both children of $(R{-}Mod,\otimes,R)$ (where $R$ is a non-zero commutative ring)

Of course, more symmetric monoidal categories should be added in the future. This is just the first batch.

Added properties of symmetric monoidal categories

• cartesian / cocartesian
• closed / coclosed
• cocomplete* / complete
• finitely cocomplete / finitely complete
• distributive / codistributive
• infinitary distributive / infinitary codistributive
• well-pointed
• strict
• trivial
• self-dual

*This means that the underlying category is cocomplete and $\otimes$ preserves colimits in each variable. There is no overlap with the notion of a cocomplete category as long as we carefully distinguish between a symmetric monoidal category and its underlying category. Hence, there is no need for a more complicated term such as "monoidally cocomplete". (Technically, storing two properties with the same name but different types has been made possible by #263.)

Added implications

There are too many to list here. Just to mention three examples:

• finitely cocomplete ===> distributive
• closed + underlying category is cocomplete ===> cocomplete
• distributive + underlying category has biproducts ===> codistributive

Proofs

The mentioned properties have been determined for the symmetric monoidal categories listed above, either by direct proofs, implications, or inheritance from parent categories.

[ScriptRaccoon]

@dschepler Do you agree with my decision (and the reasoning in the PR and this file) that "cocomplete" suffices as a property of symmetric monoidal categories and that we do not need a term like "monoidally cocomplete"?