fact: Definition make_monoidal_cat (C: category)(tensor: C ⊠ C ⟶ C)(I: C) (λ': left_unitor tensor I)(ρ': right_unitor tensor I)(α': associator tensor) (eq1: triangle_eq tensor I λ' ρ' α')(eq2: pentagon_eq tensor α'): monoidal_cat := (C,, (tensor,, (I,, (λ',, (ρ',, (α',, (eq1,, eq2))))))).
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