Definition tensor_unit_unitors_associator_equivalence (C : category) : CurriedMonoidalCategories.tensor_unit_unitors_associator C ≃ MonoidalCategoriesReordered.tensor_unit_unitors_associator C. Proof. use weqtotal2. { exact (tensor_unit_equivalence C). } intro tu. repeat (use weqdirprodf) ; apply idweq. use weqtotal2. { apply idweq. } intro α. apply weqimplimpl. - intro αnat. repeat split. + intros x y z1 z2 h. refine (αnat x x y y z1 z2 (identity x) (identity y) h @ _). apply cancel_postcomposition. rewrite tensor_id. apply idpath. + intros x1 x2 y z f. refine (_ @ αnat x1 x2 y y z z f (identity y) (identity z)). apply cancel_precomposition. rewrite tensor_id. apply idpath. + intros x y1 y2 z g. apply (αnat x x y1 y2 z z (identity x) g (identity z)). - intro αnat. intro ; intros. etrans. { apply maponpaths. etrans. { etrans. { apply maponpaths_2. exact (!(id_left _)). } etrans. { apply maponpaths. exact (!(id_right _)). } apply tensor_comp. } apply maponpaths_2. etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (!(id_left _)). } etrans. { apply maponpaths. exact (!(id_right _)). } apply tensor_comp. } etrans. { apply maponpaths_2. exact (!(id_left _)). } apply tensor_comp. } rewrite !assoc. etrans. { do 2 apply maponpaths_2. exact (pr1 αnat x y z z' h). } cbn. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. apply (pr22 αnat x y y' z' g). } cbn. rewrite !assoc'. apply maponpaths. apply (pr12 αnat x x' y' z' f). } cbn. rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths_2. refine (!_). apply tensor_comp. } etrans. { refine (!_). apply tensor_comp. } rewrite !id_left, !id_right. apply maponpaths_2. etrans. { refine (!_). apply tensor_comp. } rewrite id_left, id_right. apply idpath. - repeat (apply isapropdirprod) ; repeat (apply impred_isaprop ; intro) ; apply homset_property. - repeat (apply isapropdirprod) ; repeat (apply impred_isaprop ; intro) ; apply homset_property. 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.