proposition: Proposition smash_product_monoidal_cat_symmetric_laws : sym_mon_cat_laws_tensored smash_product_monoidal_cat smash_product_monoidal_cat_braiding.
proof: Proof. repeat split. - intros X Y. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros xy. induction xy as [ x y ]. use iscompsetquotpr ; cbn. apply hinhpr. exact (inl (idpath _)). - intros X₁ X₂ Y₁ Y₂ f g. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros xy. induction xy as [ x y ]. use iscompsetquotpr ; cbn. apply hinhpr. exact (inl (idpath _)). - intros X Y Z. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros xyz. induction xyz as [ xy z ]. revert xy. use setquotunivprop'. { intro. apply setproperty. } intros xy. induction xy as [ x y ]. use iscompsetquotpr ; cbn. apply hinhpr. exact (inl (idpath _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal