Definition monoidal_struct_to_monoidal_laws {C : category} (M : monoidal_struct C) : monoidal_laws (monoidal_struct_to_monoidal_data M). Proof. set (tuua := monoidal_struct_to_tensor_unit_unitors_associator M). set (tu := tensor_unit_unitors_associator_to_tensor_unit tuua). set (ui := (monoidal_struct_to_unitorsassociator_inverses M)). exists (pr2 (pr111 M)). exists (laxleftunitor_to_lunitor_nat _ ,, lax_monoidal_leftunitor_inverse_to_inverse_law _). exists (laxrightunitor_to_runitor_nat _ ,, lax_monoidal_rightunitor_inverse_to_inverse_law _). split. - exists (laxassociator_to_associator_nat_left _). exists (laxassociator_to_associator_nat_right _). exists (laxassociator_to_associator_nat_leftright _). do 3 intro ; apply lax_monoidal_associator_inverse_to_inverse_law. - apply monoidal_struct_to_pentagontriangle. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories.