Lemma diag_functor_fmonoidal_laxlaws : fmonoidal_laxlaws diag_functor_fmonoidal_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Import BifunctorNotations. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal. Import MonoidalNotations.