proposition: Lemma TransportedPentagonEq : pentagon_eq TD αD.
proof: Proof. intros y1 y2 y3 y4. 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. use factor_through_squash. { exact (∑ a : C, z_iso (H a) y3). } { apply homset_property. } 2: exact (H_eso y3). intros [x3 xx3]. induction (isotoid _ Duniv xx3). clear xx3. use factor_through_squash. { exact (∑ a : C, z_iso (H a) y4). } { apply homset_property. } 2: exact (H_eso y4). intros [x4 xx4]. induction (isotoid _ Duniv xx4). clear xx4. set (pentH := maponpaths #H (pent x1 x2 x3 x4)). rewrite ! functor_comp in pentH. set (tαD := TransportedAssociatorOnOb Duniv H_eso H_ff TC α). etrans. { apply maponpaths. apply TransportedAssociator_tensor_r_on_ob. } etrans. { apply maponpaths_2. apply TransportedAssociator_tensor_l_on_ob. } assert (p0 : assoc_right_tensor_l Duniv H_eso H_ff TC x1 x2 x3 x4 · assoc_left_tensor_r Duniv H_eso H_ff TC x1 x2 x3 x4 = identity _). { unfold assoc_right_tensor_l, assoc_left_tensor_r. rewrite assoc. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply (! functor_comp TD _ _). } etrans. { apply maponpaths_2. do 2 apply maponpaths. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). } etrans. { apply maponpaths_2. do 2 apply maponpaths. rewrite id_right. rewrite id_left. apply idpath. } etrans. { do 2 apply maponpaths_2. exact (TransportedAssocRightInvOnOb Duniv H_eso H_ff TC (TC (x1,x2)) x3 x4). } etrans. { apply maponpaths. exact (TransportedAssocLeftOnOb Duniv H_eso H_ff TC x1 x2 (TC (x3,x4))). } etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. apply (! functor_comp TD _ _). apply maponpaths. etrans. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). rewrite functor_id. rewrite id_left. apply maponpaths. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. apply (! functor_comp TD _ _). apply maponpaths. etrans. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). rewrite id_right. apply maponpaths_2. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } rewrite binprod_id. rewrite functor_id. rewrite id_right. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } etrans. { rewrite assoc'. apply maponpaths. do 2 rewrite assoc. do 2 apply maponpaths_2. exact p0. } clear p0. rewrite id_left. etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. exact pentH. } etrans. 2: { do 2 apply maponpaths_2. apply maponpaths. apply maponpaths_2. exact (! tαD ((x1,x2),x3)). } etrans. 2: { do 3 apply maponpaths. exact (! tαD ((x2,x3),x4)). } etrans. 2: { apply maponpaths_2. apply maponpaths. exact (! TransportedAssociator_tensor_m_on_ob _ _ _ _ _ x1 x2 x3 x4). } etrans. 2: { apply maponpaths_2. rewrite <- (id_right (id H x4)). rewrite binprod_comp. rewrite (functor_comp TD). rewrite <- (id_right (id H x4)). rewrite binprod_comp. rewrite (functor_comp TD). rewrite id_right. rewrite assoc. apply maponpaths_2. rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. assert (p : # TD (nat_z_iso_inv (TransportedAssocRight Duniv H_eso H_ff TC) ((x1, x2), x3) #, id H x4) · assoc_left_tensor_m Duniv H_eso H_ff TC x1 x2 x3 x4 = TransportedTensorComm Duniv H_eso H_ff TC (TC (x1,(TC (x2,x3))),x4)). { rewrite TransportedAssocRightInvOnOb. unfold assoc_left_tensor_m. rewrite assoc. etrans. apply maponpaths_2, (! functor_comp TD _ _). unfold TransportedAssocLeft. simpl. do 2 rewrite id_right. rewrite ! assoc. etrans. 2: apply id_left. apply maponpaths_2. rewrite id_right. fold TD. set (ptH := (TransportedTensorComm Duniv H_eso H_ff TC)). etrans. apply (! functor_comp TD _ _). rewrite <- (functor_id TD). apply maponpaths. rewrite (id_left (C := D ⊠ D)). rewrite (id_right (C := D ⊠ D)). etrans. { rewrite assoc'. apply maponpaths. apply binprod_comp. } etrans. { apply maponpaths_2. rewrite <- (id_left (id H x4)). apply binprod_comp. } rewrite assoc. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. rewrite <- binprod_comp. rewrite id_left. simpl. apply maponpaths_2. rewrite <- (functor_comp TD). apply maponpaths. rewrite <- binprod_comp. rewrite id_right. rewrite functor_id. apply maponpaths. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } rewrite binprod_id. rewrite (functor_id TD). rewrite binprod_id. rewrite id_right. simpl. etrans. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). rewrite id_right. etrans. { apply maponpaths_2. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } apply binprod_id. } exact (! p). } etrans. 2: { rewrite assoc'. apply maponpaths. rewrite <- (id_left (id H x1)). etrans. 2: { apply maponpaths. rewrite binprod_comp. apply (! functor_comp TD _ _). } rewrite assoc. apply maponpaths_2. rewrite <- (id_left (id H x1)). rewrite binprod_comp. rewrite functor_comp. rewrite assoc. apply maponpaths_2. assert (p : assoc_right_tensor_m Duniv H_eso H_ff TC x1 x2 x3 x4 · # TD (id H x1 #, TransportedAssocLeft Duniv H_eso H_ff TC ((x2, x3), x4)) = nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC) (x1 , TC (TC (x2,x3), x4))). { rewrite TransportedAssocLeftOnOb. unfold assoc_right_tensor_m. rewrite TransportedAssocRightInvOnOb. rewrite ! assoc'. etrans. 2: apply id_right. apply maponpaths. simpl. etrans. { apply maponpaths. rewrite <- (functor_comp TD). apply maponpaths. rewrite <- binprod_comp. apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite <- (functor_comp TD). apply maponpaths. etrans. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). apply maponpaths_2. apply (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). } rewrite ! id_left. rewrite binprod_id. rewrite (functor_id TD). rewrite <- (id_left (id H x1)). rewrite binprod_comp. rewrite (functor_comp TD). rewrite binprod_id. rewrite (functor_id TD). rewrite id_left. rewrite <- (functor_comp TD). rewrite <- (functor_id TD). apply maponpaths. rewrite <- binprod_comp. rewrite id_right. rewrite functor_id. etrans. apply maponpaths, (pr2 (TransportedTensorComm Duniv H_eso H_ff TC)). apply binprod_id. } exact (! p). } unfold assoc_left_tensor_l. rewrite TransportedAssocLeftOnOb. rewrite ! assoc'. etrans. 2: { apply maponpaths_2. rewrite <- (id_right (id H x4)). rewrite binprod_comp. apply (! functor_comp TD _ _). } rewrite assoc'. apply maponpaths. etrans. { apply maponpaths_2. exact (TransportedAssocLeftOnOb Duniv H_eso H_ff TC (TC (x1,x2)) x3 x4). } rewrite assoc'. apply maponpaths. rewrite assoc. etrans. { apply maponpaths_2. exact (! pr21 (TransportedTensorComm Duniv H_eso H_ff TC) _ _ (α ((x1,x2),x3) #, id x4)). } rewrite ! assoc'. rewrite <- functor_id. do 3 apply maponpaths. unfold assoc_right_tensor_r. etrans. 2: { rewrite assoc. apply maponpaths_2. rewrite <- (functor_id H). exact (pr21 (nat_z_iso_inv (TransportedTensorComm Duniv H_eso H_ff TC)) _ _ (id x1 #, α ((x2,x3),x4))). } rewrite ! assoc'. apply maponpaths. etrans. { apply maponpaths_2. apply (TransportedAssocRightInvOnOb Duniv H_eso H_ff TC). } rewrite ! assoc'. apply maponpaths. etrans. apply (! functor_comp TD _ _). apply maponpaths. rewrite functor_id. etrans. apply (! binprod_comp _ _ _ _ _ _ _ _ _ _). rewrite id_left. apply maponpaths. refine (_ @ ! TransportedAssocRightInvOnOb Duniv H_eso H_ff TC _ _ _). do 2 apply maponpaths. apply maponpaths_2. apply (! functor_id _ _). 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