Definition diag_functor_is_strong_fmonoidal : fmonoidal_stronglaws (fmonoidal_preservestensordata diag_functor_fmonoidal_lax) (fmonoidal_preservesunit diag_functor_fmonoidal_lax). Proof. unfold fmonoidal_stronglaws. split. - intro ; intro. apply inner_swap_is_z_isomorphism. - refine (_ ,, _). split ; apply (monoidal_leftunitorisolaw V I_{V}). Defined.
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.