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