proposition: Lemma SET_cart_tensor_laws : is_bifunctor SET_cart_tensor_data.
proof: Proof. repeat split. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Categories.HSET.All