Definition SET_cart_monoidal_data : monoidal_data SET. Proof. use make_monoidal_data. - exact SET_cart_tensor_data. - exact (unit,, isasetunit). - exact (λ _ y, pr2 y). - exact (λ _ y, (tt,, y)). - exact (λ _ y, pr1 y). - exact (λ _ y, (y,, tt)). - intros x y z a. induction a as [[xx yy] zz]. exact (xx,, (yy,,zz)). - intros x y z a. induction a as [xx [yy zz]]. exact ((xx,, yy),,zz). Defined.
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.