Definition associators_equiv {C : category} (T : bifunctor C C C) : associator0 T ≃ associator (bifunctor_to_functorfromproductcat T). Proof. use weqtotal2. { use weqtotal2. - use weq_iso. { exact (λ ass xyz, ass (pr11 xyz) (pr21 xyz) (pr2 xyz)). } { exact (λ nt x y z, nt ((x,,y),,z)). } { intro ; apply idpath. } intro ; apply idpath. - intro ass. use weq_iso. + intro assnat. do 3 intro. cbn. unfold functoronmorphisms1. cbn. rewrite !assoc. rewrite (pr12 assnat). rewrite !assoc'. refine (!_). etrans. { apply maponpaths. rewrite (bifunctor_leftcomp T). rewrite !assoc. rewrite (pr22 assnat). apply idpath. } etrans. { apply cancel_precomposition. rewrite assoc'. apply cancel_precomposition. apply (pr1 assnat). } rewrite !assoc. apply cancel_postcomposition. apply pathsinv0. rewrite (bifunctor_rightcomp T). apply idpath. + abstract exact (λ assnattrans, (nat_trans_associator_leftwhisker assnattrans) ,, (nat_trans_associator_rightwhisker assnattrans) ,, (nat_trans_associator_leftrightwhisker assnattrans) ). + intro ; repeat (apply isapropdirprod) ; repeat (apply impred_isaprop ; intro) ; apply homset_property. + intro. repeat (apply impred_isaprop ; intro) ; apply homset_property. } intro ass. refine (weqtotaltoforall (X := precategory_binproduct_data (precategory_binproduct_data C C) C) _ _ ∘ _)%weq. use weqtotal2. { use weq_iso. { exact (λ assinv xyz, assinv (pr11 xyz) (pr21 xyz) (pr2 xyz)). } { exact (λ assinv x y z, assinv ((x,,y),,z)). } { intro ; apply idpath. } { intro ; apply idpath. } } intro assinv. apply weqimplimpl. - intros isolaw xyz. apply isolaw. - intros isolaw x y z. apply (isolaw ((x,,y),,z)). - repeat (apply impred_isaprop ; intro) ; apply isaprop_is_inverse_in_precat. - repeat (apply impred_isaprop ; intro) ; apply isaprop_is_inverse_in_precat. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered.