Lemma TransportedAssociator_tensor_r_on_ob : ∏ x1 x2 x3 x4 : C, αD ((H x1, H x2), TD (H x3, H x4)) = assoc_left_tensor_r x1 x2 x3 x4 · #H (α ((x1,x2) , TC (x3,x4))) · assoc_right_tensor_r x1 x2 x3 x4. Proof. do 4 intro. unfold assoc_left_tensor_r. unfold assoc_right_tensor_r. etrans. 2: { rewrite assoc. apply maponpaths_2. do 2 rewrite assoc'. apply maponpaths. rewrite assoc. exact (TransportedAssociatorOnOb (((x1,x2), TC (x3,x4)))). } etrans. 2: { apply maponpaths_2. rewrite <- (functor_id TD). exact (! pr21 αD _ _ (id (pr1 (HHH ((x1, x2), TC (x3, x4)))) #, TransportedTensorComm Duniv H_eso H_ff TC (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. exact (! pr12 (pr2 (TransportedTensorComm Duniv H_eso H_ff TC) (x3,x4))). } etrans. 2: { apply maponpaths. rewrite id_right. rewrite (functor_id TD). simpl. 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.