Lemma SET_cart_monoidal_laws : monoidal_laws SET_cart_monoidal_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Categories.HSET.All.