proposition: Lemma diag_functor_fmonoidal_laxlaws : fmonoidal_laxlaws diag_functor_fmonoidal_data.
proof: Proof. repeat split. - exact diag_functor_fmonoidal_nat_left. - exact diag_functor_fmonoidal_nat_right. - exact diag_functor_fmonoidal_assoc. - exact diag_functor_fmonoidal_leftunitality. - exact diag_functor_fmonoidal_rightunitality. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal