Lemma nat_trans_associator_rightwhisker {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_rightwhisker ass. Proof. intros x1 x2 y z f. set (t := ! assnattrans _ _ ((f #, id y) #, id z)). 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. apply (! when_bifunctor_becomes_rightwhiskering _ _ _). } 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 _). } etrans. 2: { do 2 apply maponpaths ; apply (! bifunctor_leftid _ _ _). } etrans. 2: { apply maponpaths. apply (! bifunctor_leftid _ _ _). } apply (! id_right _). } etrans. { do 2 apply maponpaths_2. apply maponpaths. etrans. { apply maponpaths ; apply bifunctor_leftid. } apply id_right. } etrans. { apply maponpaths_2 ; apply maponpaths. apply bifunctor_leftid. } etrans. { apply assoc'. } apply maponpaths. apply id_left. Qed.
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.