Definition monoidal_cat : UU := ∑ C : category, ∑ tensor : C ⊠ C ⟶ C, ∑ I : C, ∑ λ' : left_unitor tensor I, ∑ ρ' : right_unitor tensor I, ∑ α' : associator tensor, (triangle_eq tensor I λ' ρ' α') × (pentagon_eq tensor α').
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.