Proposition hom_h_sq_precategory_laws : is_precategory hom_h_sq_precategory_data. Proof. use make_is_precategory_one_assoc. - intros h₁ h₂ s ; cbn. etrans. { do 2 apply maponpaths. apply lunitor_v_comp_square'. } rewrite <- rwhisker_square_comp. rewrite (linvunitor_lunitor (C := ver_bicat_of_verity_double_bicat)). rewrite rwhisker_square_id. rewrite <- lwhisker_square_comp. rewrite (linvunitor_lunitor (C := ver_bicat_of_verity_double_bicat)). rewrite lwhisker_square_id. apply idpath. - intros v₁ v₂ s ; cbn. etrans. { do 2 apply maponpaths. apply runitor_v_comp_square'. } rewrite <- rwhisker_square_comp. rewrite (lunitor_runitor_identity (C := ver_bicat_of_verity_double_bicat)). rewrite (rinvunitor_runitor (C := ver_bicat_of_verity_double_bicat)). rewrite rwhisker_square_id. rewrite <- lwhisker_square_comp. rewrite (runitor_lunitor_identity (C := ver_bicat_of_verity_double_bicat)). rewrite (linvunitor_lunitor (C := ver_bicat_of_verity_double_bicat)). rewrite lwhisker_square_id. apply idpath. - intros v₁ v₂ v₃ v₄ s₁ s₂ s₃ ; cbn. do 2 apply maponpaths. rewrite r_lwhisker_v_comp_square. rewrite r_rwhisker_v_comp_square. rewrite l_lwhisker_v_comp_square. rewrite l_rwhisker_v_comp_square. etrans. { do 2 apply maponpaths. apply lassociator_v_comp_square''. } rewrite !rwhisker_lwhisker_square. rewrite <- !rwhisker_square_comp. rewrite <- !lwhisker_square_comp. use eq_lwhisker_square. { rewrite lwhisker_hcomp. rewrite (triangle_l_inv (C := ver_bicat_of_verity_double_bicat)). rewrite <- rwhisker_hcomp. rewrite (lunitor_V_id_is_left_unit_V_id (C := ver_bicat_of_verity_double_bicat)). apply idpath. } use eq_rwhisker_square. { rewrite (lunitor_lwhisker (C := ver_bicat_of_verity_double_bicat)). apply maponpaths. apply (runitor_lunitor_identity (C := ver_bicat_of_verity_double_bicat)). } 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.