proposition: Proposition univalent_profunctor_whisker_square_bicat_law : whisker_square_bicat_law univalent_profunctor_ver_bicat_sq_id_comp_whisker.
proof: Proof. repeat split. - intros C₁ C₂ C₃ C₄ F G P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G P₁ P₂ P₃ Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q₁ Q₂ Q₃ τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite rmap_id. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃ G P Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite rmap_comp. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite lmap_id. apply idpath. - intros C₁ C₂ C₃ C₄ F G₁ G₂ G₃ P Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite lmap_comp. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ G₁ G₂ P Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite rmap_lmap. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ G P₁ P₂ Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ G P Q₁ Q₂ τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite profunctor_nat_trans_rmap. apply idpath. - intros C₁ C₂ C₃ C₄ F G₁ G₂ P₁ P₂ Q τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G₁ G₂ P Q₁ Q₂ τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite profunctor_nat_trans_lmap. apply idpath. - intros C₁ C₂ C₃ C₄ F G P₁ P₂ Q₁ Q₂ τ₁ τ₂ θ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ P Q τ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. rewrite id_left, id_right. rewrite nat_trans_ax. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ G H P₁ P₂ Q₁ Q₂ τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h. use mor_from_comp_profunctor_ob_eq ; clear h. intros y h h' ; cbn. etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm θ₁ θ₂ z x y h h'). } rewrite comp_profunctor_mor_comm. rewrite lmap_id. refine (!_). etrans. { exact (comp_v_profunctor_square_mor_comm (dwhisker_profunctor_square τ θ₁) θ₂ z x y h h'). } cbn. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F G H₁ H₂ P₁ P₂ Q₁ Q₂ τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn. etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm θ₁ θ₂ z x y h h'). } rewrite comp_profunctor_mor_comm. rewrite rmap_id. refine (!_). etrans. { exact (comp_v_profunctor_square_mor_comm θ₁ (uwhisker_profunctor_square τ θ₂) z x y h h'). } cbn. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F G₁ G₂ H P₁ P₂ Q₁ Q₂ τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. use mor_from_comp_profunctor_ob_eq ; cbn. clear h. intros y h h'. etrans. { exact (comp_v_profunctor_square_mor_comm θ₁ (dwhisker_profunctor_square τ θ₂) z x y h h'). } refine (!_). etrans. { exact (comp_v_profunctor_square_mor_comm (uwhisker_profunctor_square τ θ₁) θ₂ z x y h h'). } cbn. rewrite comp_profunctor_ob_in_comm. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ G₁ G₂ P₁ P₂ Q R τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ G₁ G₂ P Q₁ Q₂ R τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ G₁ G₂ P Q R₁ R₂ τ θ₁ θ₂ ; cbn in *. use eq_profunctor_square ; intros z x h ; cbn. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Profunctors.Examples UniMath.CategoryTheory.Profunctors.Squares UniMath.CategoryTheory.Profunctors.Transformation UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.UnivalenceOp UniMath.Bicategories.Core.Examples.OpCellBicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.DoubleBicat.Core