Lemma TransportedTriangleEq : triangle_eq TD (H I) luD ruD αD. 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.
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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. 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.DisplayedCats.Constructions.Product. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedUnitors. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedAssociator.