Definition monoidal_laws {C : category} (MD : monoidalcategory_data C) : UU := (tensorfunctor_id MD) × (tensorfunctor_comp MD) × (associator_naturality MD) × (associator_is_natiso MD) × (leftunitor_naturality MD) × (leftunitor_is_natiso MD) × (rightunitor_naturality MD) × (rightunitor_is_natiso MD) × (triangle_identity MD MD MD) × (pentagon_identity MD).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.