Proposition hom_v_sq_precategory_laws : is_precategory hom_v_sq_precategory_data. Proof. use make_is_precategory_one_assoc. - intros v₁ v₂ s ; cbn. rewrite lunitor_h_comp_square'. rewrite <- dwhisker_square_comp. rewrite linvunitor_lunitor. rewrite dwhisker_square_id. rewrite <- uwhisker_square_comp. rewrite linvunitor_lunitor. rewrite uwhisker_square_id. apply idpath. - intros v₁ v₂ s ; cbn. rewrite runitor_h_comp_square'. rewrite <- dwhisker_square_comp. rewrite lunitor_runitor_identity. rewrite rinvunitor_runitor. rewrite dwhisker_square_id. rewrite runitor_lunitor_identity. rewrite <- uwhisker_square_comp. rewrite linvunitor_lunitor. rewrite uwhisker_square_id. apply idpath. - intros v₁ v₂ v₃ v₄ s₁ s₂ s₃ ; cbn. do 2 apply maponpaths. rewrite r_uwhisker_h_comp_square. rewrite r_dwhisker_h_comp_square. rewrite l_uwhisker_h_comp_square. rewrite l_dwhisker_h_comp_square. rewrite lassociator_h_comp_square'. rewrite !dwhisker_uwhisker_square. rewrite <- uwhisker_square_comp. rewrite <- !dwhisker_square_comp. use eq_uwhisker_square. { rewrite lwhisker_hcomp. rewrite triangle_l_inv. rewrite <- rwhisker_hcomp. rewrite lunitor_V_id_is_left_unit_V_id. apply idpath. } use eq_dwhisker_square. { rewrite lunitor_lwhisker. rewrite runitor_lunitor_identity. apply idpath. } 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.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws.