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. 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.
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.