proposition: Proposition transpose_twosided_disp_cat_axioms : twosided_disp_cat_axioms transpose_twosided_disp_cat_data.
proof: Proof. repeat split. - unfold id_two_disp_left_law ; cbn. intros x₁ x₂ y₁ y₂ v₁ v₂ h₁ h₂ s. etrans. { refine (!_). apply square_id_right_v'. } rewrite <- lunitor_linvunitor_h'. rewrite transportb_disp_mor2_transpose. rewrite !globular_iso_to_path_to_iso. cbn. rewrite <- (path_to_globular_iso_square_inv (C := C)). rewrite globular_iso_to_path_to_iso. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. apply (square_assoc_v (C := C)). } unfold transportb_square. rewrite transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - unfold id_two_disp_right_law ; cbn. intros x₁ x₂ y₁ y₂ v₁ v₂ h₁ h₂ s. etrans. { refine (!_). apply square_id_right_v'. } rewrite <- runitor_rinvunitor_h'. rewrite transportb_disp_mor2_transpose. rewrite !globular_iso_to_path_to_iso. cbn. rewrite <- (path_to_globular_iso_square_inv (C := C)). rewrite globular_iso_to_path_to_iso. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. apply (square_assoc_v (C := C)). } unfold transportb_square. rewrite transportf_f_square. rewrite runitor_square. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - unfold assoc_two_disp_law ; cbn. intros x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ v₁ v₂ v₃ v₄ h₁ h₂ h₃ k₁ k₂ k₃ s₁ s₂ s₃. etrans. { refine (!_). apply square_id_right_v'. } rewrite <- lassociator_rassociator_h'. rewrite transportb_disp_mor2_transpose. rewrite !globular_iso_to_path_to_iso. cbn. rewrite <- (path_to_globular_iso_square_inv (C := C)). rewrite globular_iso_to_path_to_iso. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. apply (square_assoc_v (C := C)). } unfold transportb_square. rewrite transportf_f_square. rewrite lassociator_square. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x₁ x₂ y₁ y₂ v₁ v₂ h₁ h₂. apply isaset_square. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.DerivedLaws