proposition: Lemma nat_trans_associator_leftwhisker {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_leftwhisker ass.
proof: Proof. intros x y z1 z2 h. set (t := ! assnattrans _ _ ((id x #, id y) #, h)). simpl in t. unfold functoronmorphisms1 in t. refine (_ @ t @ _). { etrans. 2: { apply maponpaths ; apply maponpaths_2 ; apply when_bifunctor_becomes_rightwhiskering. } etrans. 2: { apply maponpaths ; apply maponpaths_2 ; use (! bifunctor_distributes_over_id _ _ _ _) ; apply T. } apply maponpaths. etrans. 2: { do 2 apply maponpaths ; apply maponpaths_2 ; apply when_bifunctor_becomes_rightwhiskering. } etrans. 2: { do 2 apply maponpaths ; apply maponpaths_2 ; use (! bifunctor_distributes_over_id _ _ _ _) ; apply T. } etrans. 2: { do 2 apply maponpaths ; apply (! id_left _). } apply (! id_left _). } etrans. { do 2 apply maponpaths_2. etrans. { apply maponpaths. etrans. { apply maponpaths ; apply bifunctor_leftid. } etrans. { apply id_right. } apply bifunctor_rightid. } apply bifunctor_rightid. } etrans. { apply assoc'. } apply id_left. 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