proposition: Lemma TransportedAssocRightInvOnOb (x y z : C) : nat_z_iso_inv TransportedAssocRight ((x,y),z) = nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC) (x, TC (y,z)) · # TD (# H (id x) #, (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC) (y, z))).
proof: Proof. use (z_iso_inv_to_left _ _ _ (_,,pr2 (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC)) (x, TC (y,z)))). use (z_iso_inv_to_right _ _ _ _ (_,, pr2 (nat_z_iso_inv TransportedAssocRight) ((x, y), z))). set (t := TransportedAssocRightOnOb x y z). etrans. 2: { apply maponpaths. apply (! t). } etrans. 2: { rewrite assoc. apply maponpaths_2. apply (functor_comp TD). } etrans. 2: { apply maponpaths_2. apply maponpaths. apply binprod_comp. } etrans. 2: { apply maponpaths_2. apply maponpaths. rewrite (functor_id H). rewrite id_right. apply maponpaths. apply (! pr22 ((pr2 (TransportedTensorComm Duniv H_eso H_ff TC)) (y, z))). } etrans. 2: { apply maponpaths_2. rewrite binprod_id. apply (! functor_id TD _). } apply (! id_left _). 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