proposition: Lemma TransportedAssociator_tensor_l_on_ob : ∏ x1 x2 x3 x4 : C, αD ((TD (H x1, H x2), H x3), H x4) = assoc_left_tensor_l x1 x2 x3 x4 · #H (α ((TC (x1,x2) , x3),x4)) · assoc_right_tensor_l x1 x2 x3 x4.
proof: Proof. do 4 intro. unfold assoc_left_tensor_l. unfold assoc_right_tensor_l. etrans. 2: { rewrite assoc. apply maponpaths_2. do 2 rewrite assoc'. apply maponpaths. rewrite assoc. exact (TransportedAssociatorOnOb ((TC (x1,x2),x3),x4)). } etrans. 2: { apply maponpaths_2. exact (! pr21 αD _ _ ((TransportedTensorComm Duniv H_eso H_ff TC (x1, x2) #, id H (pr21 ((TC (x1, x2), x3), x4))) #, id functor_identity D (pr2 (HHH ((TC (x1, x2), x3), x4))))). } etrans. 2: { rewrite assoc'. apply maponpaths. etrans. 2: apply (functor_comp TD). apply maponpaths. etrans. 2: apply binprod_comp. etrans. 2: { apply maponpaths. etrans. 2: apply maponpaths_2, maponpaths, (! binprod_id _ _). rewrite functor_id. apply (! id_left _). } apply maponpaths_2. exact (! pr12 (pr2 (TransportedTensorComm Duniv H_eso H_ff TC) (x1,x2))). } etrans. 2: { apply maponpaths. 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