Definition monoidalcategory_data (C : category): UU := ∑ T : tensor_data C, ∑ I : C, (leftunitor_data T I) × (rightunitor_data T I) × (associator_data T).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.