fact: 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 α').
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering