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. 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.
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.