Proposition smash_product_monoidal_cat_symmetric_laws : sym_mon_cat_laws_tensored smash_product_monoidal_cat smash_product_monoidal_cat_braiding. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal.