proposition: Lemma nat_trans_associator_leftrightwhisker {C : category} {T : bifunctor C C C} {ass : associator_data T} (assnattrans : is_nat_trans (assoc_left (bifunctor_to_functorfromproductcat T)) (assoc_right (bifunctor_to_functorfromproductcat T)) (λ xyz, ass (pr11 xyz) (pr21 xyz) (pr2 xyz))) : associator_nat_leftrightwhisker ass.
proof: Proof. intros x y1 y2 z g. set (t := ! assnattrans _ _ ((id x #, g) #, id z)). simpl in t. refine (_ @ t @ _). { etrans. 2: { do 2 apply maponpaths ; apply (! when_bifunctor_becomes_rightwhiskering _ _ _). } apply maponpaths. apply (! when_bifunctor_becomes_leftwhiskering _ _ _). } etrans. { do 2 apply maponpaths_2 ; apply when_bifunctor_becomes_leftwhiskering. } apply maponpaths_2. apply when_bifunctor_becomes_rightwhiskering. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered