proposition: Lemma TransportedAssociator_tensor_m_on_ob : ∏ x1 x2 x3 x4 : C, αD ((H x1, TD (H x2, H x3)), H x4) = assoc_left_tensor_m x1 x2 x3 x4 · #H (α ((x1, TC (x2,x3)),x4)) · assoc_right_tensor_m x1 x2 x3 x4.
proof: Proof. do 4 intro. unfold assoc_left_tensor_m. unfold assoc_right_tensor_m. etrans. 2: { rewrite assoc. apply maponpaths_2. do 2 rewrite assoc'. apply maponpaths. rewrite assoc. exact (TransportedAssociatorOnOb ((x1, TC (x2,x3)),x4)). } etrans. 2: { apply maponpaths_2. exact (! pr21 αD _ _ ((id H (pr11 ((x1, TC (x2, x3)), x4)) #, TransportedTensorComm Duniv H_eso H_ff TC (x2, x3)) #, id functor_identity D (pr2 (HHH ((x1, TC (x2, x3)), x4))))). } etrans. 2: { rewrite assoc'. apply maponpaths. etrans. 2: apply (functor_comp TD). etrans. 2: apply maponpaths, binprod_comp. rewrite id_left. do 2 apply maponpaths. etrans. 2: apply (functor_comp TD). apply maponpaths. etrans. 2: apply binprod_comp. apply maponpaths_2. exact (! pr12 (pr2 (TransportedTensorComm Duniv H_eso H_ff TC) (x2,x3))). } etrans. 2: { apply maponpaths. rewrite id_right. rewrite (functor_id TD). simpl. rewrite binprod_id. apply (! functor_id TD _). } apply (! id_right _). 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.Core.Univalence UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecompEquivalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit