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