Proposition univcat_profunctor_whisker_square_bicat_law : whisker_square_bicat_law univcat_profunctor_ver_bicat_sq_id_comp_whisker. 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 (uwhisker_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 θ₁ (dwhisker_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 θ₁ (uwhisker_profunctor_square τ θ₂) z x y h h'). } refine (!_). etrans. { exact (comp_v_profunctor_square_mor_comm (dwhisker_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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Profunctors.Transformation. 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.ProfunctorTwosidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.