Definition monoidal_struct_to_monoidal_data {C : category} (M : monoidal_struct C) : monoidal_data C. 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 (tensor_unit_to_tensor tu). exists (tensor_unit_to_unit tu). exists (tensor_unit_unitors_associator_laxleftunitor tuua). exists (unitorsassociator_inverses_to_leftunitorinverse ui). exists (pr1 (tensor_unit_unitors_associator_laxrightunitor tuua)). exists (unitorsassociator_inverses_to_rightunitorinverse ui). exists (tensor_unit_unitors_associator_laxassociator tuua). exact (unitorsassociator_inverses_to_associatorinverse ui). 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.