Proposition transpose_twosided_disp_cat_axioms : twosided_disp_cat_axioms transpose_twosided_disp_cat_data. 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.
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.