Proposition univcat_profunctor_double_bicat_cylinder_laws : double_bicat_cylinder_laws univcat_profunctor_ver_bicat_sq_id_comp_whisker. Proof. repeat split. - intros C₁ C₂ C₃ C₄ D₁ D₂ D₃ D₄ F₁ F₂ F₃ G₁ G₂ G₃ P₁ P₂ P₃ P₄ τ₁ τ₂ τ₃. use eq_profunctor_square. intros y x h ; cbn. rewrite lmap_id, rmap_id. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ C₇ C₈ F₁ F₂ F₃ F₄ P₁ P₂ P₃ Q₁ Q₂ Q₃ τ₁ τ₂ τ₃. use eq_profunctor_square. intros x₁ x₂ h. use mor_from_comp_profunctor_ob_eq. clear h. intros x₃ h h'. cbn in *. use (mor_from_comp_profunctor_ob_eq P₂ P₃ x₁ x₃ (λ h', comp_v_profunctor_square_mor (comp_v_profunctor_square τ₁ τ₂) τ₃ x₁ x₂ (associator_profunctor_nat_trans_mor P₁ P₂ P₃ x₁ x₂ (comp_profunctor_ob_in P₁ (comp_profunctor P₂ P₃) x₃ h h'))) (λ h', associator_profunctor_nat_trans_mor Q₁ Q₂ Q₃ (F₄ x₁) (F₁ x₂) (comp_v_profunctor_square_mor τ₁ (comp_v_profunctor_square τ₂ τ₃) x₁ x₂ (comp_profunctor_ob_in P₁ (comp_profunctor P₂ P₃) x₃ h h')))). clear h'. intros x₄ h' h'' ; cbn. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. apply associator_profunctor_nat_trans_mor_ob_comm. } etrans. { exact (comp_v_profunctor_square_mor_comm (comp_v_profunctor_square τ₁ τ₂) τ₃ _ _ _ _ _). } cbn. etrans. { apply maponpaths_2. exact (comp_v_profunctor_square_mor_comm τ₁ τ₂ _ _ _ _ _). } refine (!_). etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm τ₁ (comp_v_profunctor_square τ₂ τ₃) _ _ _ _ _). } rewrite associator_profunctor_nat_trans_mor_comm ; cbn. etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm τ₂ τ₃ _ _ _ _ _). } etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm Q₁ Q₂ Q₃ (τ₁ x₃ x₂ h) (τ₂ x₄ x₃ h') (τ₃ x₁ x₄ h'')). } cbn. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ. use eq_profunctor_square. intros y x h ; cbn. rewrite lmap_id, rmap_id. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ. use eq_profunctor_square. intros y x h. use mor_from_comp_profunctor_ob_eq. clear h. intros z h h' ; cbn in *. rewrite lunitor_profunctor_nat_trans_mor_comm. refine (!_). etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm (id_v_profunctor_square F) τ y x z h h'). } cbn. rewrite lunitor_profunctor_nat_trans_mor_comm. rewrite (profunctor_square_rmap τ). apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ. use eq_profunctor_square. intros y x h ; cbn. rewrite lmap_id, rmap_id. apply idpath. - intros C₁ C₂ C₃ C₄ F G P Q τ. use eq_profunctor_square. intros y x h. use mor_from_comp_profunctor_ob_eq. clear h. intros z h h' ; cbn in *. rewrite runitor_profunctor_nat_trans_mor_comm. refine (!_). etrans. { apply maponpaths. exact (comp_v_profunctor_square_mor_comm τ (id_v_profunctor_square G) y x z h h'). } cbn. rewrite runitor_profunctor_nat_trans_mor_comm. rewrite (profunctor_square_lmap τ). apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ F₃ P₁ P₂ P₁' P₂' Q₁ Q₂ Q₁' Q₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂'. intros p q. use eq_profunctor_square. intros x₁ x₂ h. use mor_from_comp_profunctor_ob_eq. clear h. intros x₃ h h' ; cbn in *. etrans. { do 2 apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ₁ P₁' h h'). } etrans. { apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm P₂ τ₂ (τ₁ x₃ x₂ h) h'). } etrans. { exact (comp_v_profunctor_square_mor_comm s₁' s₂' x₁ x₂ x₃ (τ₁ x₃ x₂ h) (τ₂ x₁ x₃ h')). } refine (!_). etrans. { do 2 apply maponpaths. exact (comp_v_profunctor_square_mor_comm s₁ s₂ x₁ x₂ x₃ h h'). } etrans. { apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm θ₁ Q₁' (s₁ x₃ x₂ h) (s₂ x₁ x₃ h')). } cbn. etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm Q₂ θ₂ (θ₁ (F₂ x₃) (F₁ x₂) (s₁ x₃ x₂ h)) (s₂ x₁ x₃ h')). } cbn. pose (profunctor_square_eq_pointwise p h) as p'. pose (profunctor_square_eq_pointwise q h') as q'. cbn in p', q'. rewrite q'. rewrite p'. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ C₆ F₁ F₂ F₃ P₁ P₂ P₁' P₂' Q₁ Q₂ Q₁' Q₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂'. intros p q. use eq_profunctor_square. intros x₁ x₂ h ; cbn in *. rewrite lmap_comp. etrans. { apply maponpaths. refine (!_). apply (profunctor_square_lmap s₂). } etrans. { apply (profunctor_square_eq_pointwise q). } cbn. etrans. { do 2 apply maponpaths. exact (profunctor_square_eq_pointwise p h). } cbn. rewrite (profunctor_square_rmap s₂'). rewrite <- rmap_comp. apply maponpaths_2. rewrite nat_trans_ax. 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.