proposition: Lemma sym_mon_cat_laws_tensored_from_sym_mon : sym_mon_cat_laws_tensored V sym_mon_braiding.
proof: Proof. repeat split. - apply sym_mon_braiding_inv. - intros; apply tensor_sym_mon_braiding. - apply sym_mon_hexagon_lassociator. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories