Definition cmon_equiv_monreordered (C : category) : CurriedMonoidalCategories.mon_structure C ≃ MonoidalCategoriesReordered.monoidal_struct C. Proof. use weqtotal2. { apply tensor_unit_unitors_associator_equivalence. } intro. repeat (apply weqdirprodf). - apply weqimplimpl ; try (intro ; assumption) ; (try apply isaprop_triangle). - apply weqimplimpl ; try (intro ; assumption) ; (try apply isaprop_pentagon). - use weq_iso. + intro lui. exists (λ c, pr1 (lui c)). intro ; apply lui. + intro lui. intro c. exists ((pr1 lui) c). apply ((pr2 lui) c). + intro ; apply isaprop_lunitor_invertible. + intro ; apply isaprop_lax_monoidal_leftunitor_inverse. - use weq_iso. + intro rui. exists (λ c, pr1 (rui c)). intro ; apply rui. + intro rui. intro c. exists ((pr1 rui) c). apply ((pr2 rui) c). + intro ; apply isaprop_runitor_invertible. + intro ; apply isaprop_lax_monoidal_rightunitor_inverse. - use weq_iso. + intro ai. exists (λ c1 c2 c3, pr1 (ai c1 c2 c3)). intro ; apply ai. + intro ai. intros c1 c2 c3. exists ((pr1 ai) c1 c2 c3). apply ((pr2 ai) c1 c2 c3). + intro ; apply isaprop_associator_invertible. + intro ; apply isaprop_lax_monoidal_associator_inverse. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.