proposition: Lemma SET_cart_monoidal_laws : monoidal_laws SET_cart_monoidal_data.
proof: Proof. split. - exact SET_cart_tensor_laws. - repeat split. + apply funextsec; intro a; induction a as [t a]; induction t; apply idpath. + apply funextsec; intro a; induction a as [a t]; induction t; apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Categories.HSET.All