fact: Definition strict_monoidal_cat : UU := ∑ M : monoidal_cat, ∏ (eq_λ : I_pretensor (monoidal_cat_tensor M) (monoidal_cat_unit M) = functor_identity (pr1 M)), ∏ (eq_ρ : I_posttensor (monoidal_cat_tensor M) (monoidal_cat_unit M) = functor_identity (pr1 M)), ∏ (eq_α : assoc_left (monoidal_cat_tensor M) = assoc_right (monoidal_cat_tensor M)), is_strict (monoidal_cat_tensor M) (monoidal_cat_unit M) eq_λ (monoidal_cat_left_unitor M) eq_ρ (monoidal_cat_right_unitor M) eq_α (monoidal_cat_associator M).
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