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. 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.
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.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit.