Proposition double_inverse_pentagon {C : double_cat} {v w x y z : C} (h₁ : v -->h w) (h₂ : w -->h x) (h₃ : x -->h y) (h₄ : y -->h z) : rassociator_h (h₁ ·h h₂) h₃ h₄ ⋆v rassociator_h h₁ h₂ (h₃ ·h h₄) = transportf_square (id_v_right _) (id_v_right _) ((rassociator_h h₁ h₂ h₃ ⋆h id_v_square h₄) ⋆v rassociator_h h₁ (h₂ ·h h₃) h₄ ⋆v (id_v_square h₁ ⋆h rassociator_h h₂ h₃ h₄)). Proof. refine (!(square_id_right_v' _) @ _ @ square_id_right_v' _). apply maponpaths. rewrite <- !lassociator_rassociator_h'. rewrite !transportf_square_postwhisker. apply maponpaths. refine (square_assoc_v _ _ _ @ _ @ !(square_assoc_v _ _ _)). apply maponpaths. apply maponpaths_2. etrans. { refine (!(square_assoc_v' _ _ _) @ _). rewrite rassociator_lassociator_h. unfold transportb_square. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_id_right_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!(square_id_right_v' _) @ _ @ square_id_right_v' _). apply maponpaths. rewrite <- !lassociator_rassociator_h'. rewrite !transportf_square_postwhisker. apply maponpaths. refine (square_assoc_v _ _ _ @ _ @ !(square_assoc_v _ _ _)). apply maponpaths. apply maponpaths_2. rewrite transportf_square_prewhisker. rewrite rassociator_lassociator_h. unfold transportb_square. rewrite transportf_f_square. refine (!_). etrans. { refine (!(square_assoc_v' _ _ _) @ _). rewrite double_pentagon'. rewrite transportf_square_postwhisker. rewrite transportf_square_prewhisker. rewrite !transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. etrans. { do 3 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. etrans. { do 3 apply maponpaths. apply maponpaths_2. apply hcomp_split_globular_l_id ; apply idpath. } rewrite transportf_square_prewhisker. rewrite !transportf_square_postwhisker. rewrite rassociator_lassociator_h. unfold transportb_square. rewrite !transportf_f_square. etrans. { do 3 apply maponpaths. apply maponpaths_2. rewrite transportf_hcomp_r. rewrite transportf_square_id. rewrite comp_h_square_id. apply idpath. } rewrite transportf_square_prewhisker. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. rewrite rassociator_lassociator_h. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite (hcomp_split_globular_r_id (idpath _) (idpath _)). rewrite !transportf_f_square. rewrite rassociator_lassociator_h. unfold transportb_square. rewrite !transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_id. rewrite comp_h_square_id. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.Variations. Import TransportSquare.