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).
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.