proposition: Lemma TransportedTriangleEq : triangle_eq TD (H I) luD ruD αD.
proof: Proof. intros y1 y2. use factor_through_squash. { exact (∑ a : C, z_iso (H a) y1). } { apply homset_property. } 2: exact (H_eso y1). intros [x1 xx1]. induction (isotoid _ Duniv xx1). clear xx1. use factor_through_squash. { exact (∑ a : C, z_iso (H a) y2). } { apply homset_property. } 2: exact (H_eso y2). intros [x2 xx2]. induction (isotoid _ Duniv xx2). clear xx2. etrans. { apply maponpaths. apply maponpaths_2. exact (TransportedRightUnitorOnOb Duniv H_eso H_ff TC I ru x1). } etrans. 2: { do 3 apply maponpaths. exact (! TransportedLeftUnitorOnOb Duniv H_eso H_ff TC I lu x2). } etrans. 2: { apply maponpaths_2. exact (! TransportedAssociatorOnOb Duniv H_eso H_ff TC α ((x1,I),x2)). } rewrite (! id_right (id H x2)). rewrite (! id_right (id H x1)). do 2 rewrite binprod_comp. rewrite (functor_comp TD). rewrite <- functor_id. assert (p0 : #TD (#H (ru x1) #, #H (id x2)) = (pr11 (TransportedTensorComm Duniv H_eso H_ff TC)) (I_posttensor TC I x1, x2) · # (TC ∙ H) (ru x1 #, id x2) · (pr1 (pr2 (TransportedTensorComm Duniv H_eso H_ff TC) (x1, x2)))). { apply pathsinv0. use (z_iso_inv_to_right _ _ _ _ (_,,(pr2 (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC)) (x1, x2)))). exact (! pr21 (TransportedTensorComm Duniv H_eso H_ff TC) _ _ (ru x1 #, id x2)). } etrans. { apply maponpaths. exact p0. } clear p0. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. exact (maponpaths #H (tri x1 x2)). } rewrite (functor_comp H). assert (p0 : # TD (LiftPreservesPostTensor Duniv H_eso H_ff TC I x1 #, # H (id x2)) · ((pr11 (TransportedTensorComm Duniv H_eso H_ff TC)) (I_posttensor TC I x1, x2)) = TransportedAssocLeft Duniv H_eso H_ff TC ((x1, I), x2)). { symmetry. refine (TransportedAssocLeftOnOb Duniv H_eso H_ff TC x1 I x2 @ _). apply maponpaths_2. unfold LiftPreservesPostTensor. rewrite functor_id. apply maponpaths. apply maponpaths_2. unfold TransportedTensorComm. simpl. rewrite ! id_left. rewrite ! id_right. rewrite (functor_id (lift_functor_along (D,, Duniv) (pair_functor H H) (pair_functor_eso H H H_eso H_eso) (pair_functor_ff H H H_ff H_ff) (TC ∙ H))). rewrite functor_id. rewrite id_right. apply (! id_left _). } rewrite ! assoc. etrans. { do 3 apply maponpaths_2. exact p0. } clear p0. rewrite ! assoc'. do 2 apply maponpaths. rewrite functor_comp. etrans. { apply (pr21 (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC))). } rewrite assoc. rewrite <- functor_id. apply maponpaths_2. assert (p0 : LiftPreservesPretensor Duniv H_eso H_ff TC I x2 = (TransportedTensorComm Duniv H_eso H_ff TC) (I,x2)). { simpl. rewrite ! functor_id. rewrite ! id_left. rewrite ! id_right. etrans. { apply maponpaths_2. apply functor_id. } apply id_left. } rewrite p0. clear p0. set (i := pr2 (nat_z_iso_inv ((TransportedAssocRight Duniv H_eso H_ff TC))) ((x1, I), x2)). use (z_iso_inv_to_left _ _ _ (_,,i)). set (j := pr2 (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC)) (x1, I_pretensor TC I x2)). use (z_iso_inv_to_right _ _ _ _ (_,,j)). exact (TransportedAssocRightOnOb Duniv H_eso H_ff TC x1 I x2). 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.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.catiso UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecompEquivalence UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedUnitors UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedAssociator