Definition SET_cart_tensor_data : bifunctor_data SET SET SET. Proof. repeat (use tpair). - intros x y. exact (((pr1 x × pr1 y),, isaset_dirprod (pr2 x) (pr2 y))). - intros x y1 y2 g a. exact (pr1 a,, g (pr2 a)). - intros y x1 x2 f b. exact (f (pr1 b),, pr2 b). 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.