Given monoidal categories $(\mathcal{C}, \otimes, I_{\mathcal{C}})$ and $(\mathcal{D}, \bullet, I_{\mathcal{D}})$. A bifunctor $F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}$ is Semigroupal if it supports a natural transformation $\phi_{ABC,XYZ} : F\ A\ B\ C \bullet F\ X\ Y\ Z \to F\ (A \otimes X)\ (B \otimes Y)\ (C \otimes Z)$, which we call combine.

Laws

Associativity:

$$\require{AMScd} \begin{CD} (F A B C \bullet F X Y Z) \bullet F P Q R @>>{\alpha_{\mathcal{D}}}> F A B C \bullet (F X Y Z \bullet F P Q R) \\ @VV{\phi_{ABC,XYZ} \bullet 1}V @VV{1 \bullet \phi_{XYZ,PQR}}V \\ F (A \otimes X) (B \otimes Y) (C \otimes Z) \bullet F P Q R @. F A B C \bullet (F (X \otimes P) (Y \otimes Q) (Z \otimes R) \\ @VV{\phi_{(A \otimes X)(B \otimes Y)(C \otimes Z),PQR}}V @VV{\phi_{ABC,(X \otimes P)(Y \otimes Q)(Z \otimes R)}}V \\ F ((A \otimes X) \otimes P) ((B \otimes Y) \otimes Q) ((C \otimes Z) \otimes R) @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}\alpha_{\mathcal{C_3}}> F (A \otimes (X \otimes P)) (B \otimes (Y \otimes Q)) (C \otimes (Z \otimes R)) \\ \end{CD}$$

combine . grmap combine . bwd assoc ≡ fmap (bwd assoc) . combine . glmap combine

Given monoidal categories $(\mathcal{C}, \otimes, I_{\mathcal{C}})$ and $(\mathcal{D}, \bullet, I_{\mathcal{D}})$. A bifunctor $F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}$ is Unital if it supports a morphism $\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\ I_{\mathcal{C_3}}$, which we call introduce.

Given monoidal categories $(\mathcal{C}, \otimes, I_{\mathcal{C}})$ and $(\mathcal{D}, \bullet, I_{\mathcal{D}})$. A bifunctor $F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}$ is Monoidal if it maps between $\mathcal{C_1} \times \mathcal{C_2}\ \times \mathcal{C_3}$ and $\mathcal{D}$ while preserving their monoidal structure. Eg., a homomorphism of monoidal categories.

See NCatlab for more details.

Laws

Right Unitality:

$$\require{AMScd} \begin{CD} F A B C \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} I_{\mathcal{C_{3}}}\\ @VV{\rho_{\mathcal{D}}}V @VV{\phi ABC,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}I_{\mathcal{C_{3}}}}V \\ F A B C @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}} \rho_{\mathcal{C_{3}}}}< F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}}) (C \otimes I_{\mathcal{C_{3}}}) \end{CD}$$

combine . grmap introduce ≡ bwd unitr . fwd unitr

Left Unitality:

$$\begin{CD} I_{\mathcal{D}} \bullet F A B C @>{\phi \bullet 1}>> F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B C\\ @VV{\lambda_{\mathcal{D}}}V @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}I_{\mathcal{C_{3}}},\phi ABC}V \\ F A B C @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}} \lambda_{\mathcal{C_{3}}}}< F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B) (I_{\mathcal{C_{3}}} \otimes C) \end{CD}$$

combine . glmap introduce ≡ fmap (bwd unitl) . fwd unitl