Lemma TransportedPentagonEq : pentagon_eq TD αD. 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.
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.