Proposition transpose_pentagon_law : pentagon_law transpose_associator. Proof. unfold pentagon_law ; cbn. unfold double_associator. cbn -[idtoiso_twosided_disp]. intros v w x y z v₁ v₂ v₃ v₄. etrans. { apply maponpaths. etrans. { apply maponpaths. apply idtoiso_twosided_disp_transpose. } apply maponpaths_2. apply idtoiso_twosided_disp_transpose. } refine (!_). etrans. { etrans. { apply maponpaths. apply maponpaths_2. apply idtoiso_twosided_disp_transpose. } apply maponpaths_2. etrans. { apply maponpaths. apply idtoiso_twosided_disp_transpose. } apply maponpaths_2. apply maponpaths. apply idtoiso_twosided_disp_transpose. } rewrite transportb_disp_mor2_transpose. refine (!_). etrans. { do 2 apply maponpaths. refine (!_). apply path_to_globular_iso_square_inv. } rewrite !globular_iso_to_path_to_iso. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. etrans. { apply maponpaths. apply maponpaths_2. refine (!_). apply (runitor_square' (C := C)). } rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. etrans. { do 2 apply maponpaths. apply runitor_rinvunitor_h. } unfold transportb_square. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_id_right_v. unfold transportb_square. rewrite transportf_f_square. rewrite !transportf_hcomp_l. rewrite !transportf_f_square. use transportf_square_eq. rewrite <- !id_h_square_comp. rewrite transportf_square_id. etrans. { apply maponpaths_2. apply maponpaths. apply transportf_square_id_h_square_eq'. } refine (!_). etrans. { apply maponpaths_2. apply maponpaths. apply transportf_square_id_h_square_eq'. } etrans. { apply maponpaths. apply transportf_square_id_h_square_eq'. } use eq_hcomp_square. - abstract (rewrite !assocl_v ; apply idpath). - refine (!_). etrans. { refine (!_). apply (transportf_hcomp_r (idpath _)). } apply maponpaths. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - apply transportf_square_id_h_square_eq. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws. Import TransportSquare.