Proposition horizontal_prebicat_laws : prebicat_laws horizontal_prebicat_data. Proof. repeat split ; cbn. - intros x y f g s. rewrite square_id_left_v. rewrite transportfb_square. apply idpath. - intros x y f g s. rewrite square_id_right_v. unfold transportb_square. rewrite transportf_f_square. apply transportf_square_id. - intros x y f g h k s₁ s₂ s₃. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x y z f g. rewrite comp_h_square_id. apply idpath. - intros x y z f g. rewrite comp_h_square_id. apply idpath. - intros x y z f g h i s₁ s₂. rewrite <- comp_h_square_comp. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_hcomp_r. rewrite transportf_hcomp_l. rewrite transportf_f_square. use transportf_square_eq. rewrite transportf_hcomp_l. rewrite transportf_square_id. apply idpath. - intros x y z f g h i s₁ s₂. rewrite <- comp_h_square_comp. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_hcomp_l. rewrite transportf_hcomp_r. rewrite transportf_f_square. use transportf_square_eq. rewrite transportf_hcomp_l. rewrite transportf_square_id. apply maponpaths. use transportf_square_eq. apply idpath. - intros x y f g s. rewrite <- id_h_square_id. rewrite (lunitor_square s). unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x y f g s. rewrite <- id_h_square_id. rewrite (runitor_square s). unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros w x y z f g h i s. rewrite lassociator_square. unfold transportb_square. rewrite transportf_f_square. rewrite <- comp_h_square_id. use transportf_square_eq. apply idpath. - intros w x y z f g h i s. rewrite lassociator_square. unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros w x y z f g h i s. rewrite <- comp_h_square_id. rewrite lassociator_square. unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x y z f g h i s₁ s₂. rewrite <- !comp_h_square_comp. rewrite !square_id_left_v. rewrite !square_id_right_v. unfold transportb_square. use transportf_square_eq. use eq_hcomp_square. + apply idpath. + rewrite transportf_square_id. use transportf_square_eq. apply idpath. + rewrite transportf_square_id. use transportf_square_eq. apply idpath. - intros x y f. rewrite lunitor_linvunitor_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros x y f. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros x y f. rewrite runitor_rinvunitor_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros x y f. rewrite rinvunitor_runitor_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros w x y z f g h. rewrite lassociator_rassociator_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros w x y z f g h. rewrite rassociator_lassociator_h. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros x y z f g. rewrite double_triangle. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_square_id. apply idpath. - intros v w x y z f g h i. rewrite double_pentagon'. rewrite transportf_square_prewhisker. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Strictness. 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.Core.PseudoDoubleSetCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws. Import TransportSquare.