Proposition univcat_profunctor_ver_sq_bicat_prebicat_laws : ver_sq_bicat_prebicat_laws univcat_profunctor_ver_sq_bicat_id_comp_cells. Proof. repeat split. - intros C₁ C₂ P Q τ. use eq_profunctor_nat_trans. intros y x h ; cbn. apply idpath. - intros C₁ C₂ P Q τ. use eq_profunctor_nat_trans. intros y x h ; cbn. apply idpath. - intros C₁ C₂ P₁ P₂ P₃ P₄ τ₁ τ₂ τ₃. use eq_profunctor_nat_trans. intros y x h ; cbn. apply idpath. - intros C₁ C₂ C₃ P Q. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn. exact (lwhisker_profunctor_nat_trans_mor_comm P (profunctor_nat_trans_id Q) h h'). - intros C₁ C₂ C₃ P Q. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn. exact (rwhisker_profunctor_nat_trans_mor_comm (profunctor_nat_trans_id P) Q h h'). - intros C₁ C₂ C₃ P Q₁ Q₂ Q₃ τ₁ τ₂. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn in *. etrans. { apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm P τ₁ h h'). } etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm P τ₂ h (τ₁ z y h')). } refine (!_). etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm P (profunctor_nat_trans_comp τ₁ τ₂) h h'). } cbn. apply idpath. - intros C₁ C₂ C₃ P₁ P₂ P₃ Q τ₁ τ₂. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn in *. etrans. { apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ₁ Q h h'). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm τ₂ Q (τ₁ y x h) h'). } refine (!_). etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm (profunctor_nat_trans_comp τ₁ τ₂) Q h h'). } cbn. apply idpath. - intros C₁ C₂ P Q τ. use eq_profunctor_nat_trans. intros y x h. use mor_from_comp_profunctor_ob_eq. clear h. intros w h h' ; cbn in *. etrans. { apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm (id_profunctor C₁) τ h h'). } rewrite !lunitor_profunctor_nat_trans_mor_comm. rewrite <- profunctor_nat_trans_rmap. apply idpath. - intros C₁ C₂ P Q τ. use eq_profunctor_nat_trans. intros y x h. use mor_from_comp_profunctor_ob_eq. clear h. intros w h h' ; cbn in *. etrans. { apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ (id_profunctor C₂) h h'). } rewrite !runitor_profunctor_nat_trans_mor_comm. rewrite <- profunctor_nat_trans_lmap. apply idpath. - intros C₁ C₂ C₃ C₄ P Q R₁ R₂ τ. use eq_profunctor_nat_trans. intros z w h. use mor_from_comp_profunctor_ob_eq. clear h. intros x h h' ; cbn in *. use (mor_from_comp_profunctor_ob_eq Q R₁ z x (λ h', associator_profunctor_nat_trans_mor P Q R₂ z w (lwhisker_profunctor_nat_trans_mor P (lwhisker_profunctor_nat_trans Q τ) z w (comp_profunctor_ob_in P (comp_profunctor Q R₁) x h h'))) (λ h', lwhisker_profunctor_nat_trans_mor (comp_profunctor P Q) τ z w (associator_profunctor_nat_trans_mor P Q R₁ z w (comp_profunctor_ob_in P (comp_profunctor Q R₁) x h h')))). clear h'. intros y h' h'' ; cbn. etrans. { apply maponpaths. apply lwhisker_profunctor_nat_trans_mor_comm. } cbn. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. apply lwhisker_profunctor_nat_trans_mor_comm. } etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm P Q R₂ h h' (τ z y h'')). } refine (!_). rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P Q R₁ h h' h''). } etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm (comp_profunctor P Q) τ (comp_profunctor_ob_in P Q x h h') h''). } apply idpath. - intros C₁ C₂ C₃ C₄ P Q₁ Q₂ R τ. use eq_profunctor_nat_trans. intros z w h. use mor_from_comp_profunctor_ob_eq. clear h. intros x h h' ; cbn in *. use (mor_from_comp_profunctor_ob_eq Q₁ R z x (λ h', associator_profunctor_nat_trans_mor P Q₂ R z w (lwhisker_profunctor_nat_trans_mor P (rwhisker_profunctor_nat_trans τ R) z w (comp_profunctor_ob_in P (comp_profunctor Q₁ R) x h h'))) (λ h', rwhisker_profunctor_nat_trans_mor (lwhisker_profunctor_nat_trans P τ) R z w (associator_profunctor_nat_trans_mor P Q₁ R z w (comp_profunctor_ob_in P (comp_profunctor Q₁ R) x h h')))). clear h'. intros y h' h'' ; cbn. etrans. { apply maponpaths. apply lwhisker_profunctor_nat_trans_mor_comm. } cbn. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. apply rwhisker_profunctor_nat_trans_mor_comm. } etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm P Q₂ R h (τ y x h') h''). } refine (!_). rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P Q₁ R h h' h''). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm (lwhisker_profunctor_nat_trans P τ) R (comp_profunctor_ob_in P Q₁ x h h') h''). } etrans. { apply maponpaths_2. exact (lwhisker_profunctor_nat_trans_mor_comm P τ h h'). } apply idpath. - intros C₁ C₂ C₃ C₄ P₁ P₂ Q R τ. use eq_profunctor_nat_trans. intros z w h. use mor_from_comp_profunctor_ob_eq. clear h ; cbn. intros x h h'. use (mor_from_comp_profunctor_ob_eq Q R z x (λ h', rwhisker_profunctor_nat_trans_mor (rwhisker_profunctor_nat_trans τ Q) R z w (associator_profunctor_nat_trans_mor P₁ Q R z w (comp_profunctor_ob_in P₁ (comp_profunctor Q R) x h h'))) (λ h', associator_profunctor_nat_trans_mor P₂ Q R z w (rwhisker_profunctor_nat_trans_mor τ (comp_profunctor Q R) z w (comp_profunctor_ob_in P₁ (comp_profunctor Q R) x h h')))). clear h'. intros y h' h'' ; cbn in *. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P₁ Q R h h' h''). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm (rwhisker_profunctor_nat_trans τ Q) R (comp_profunctor_ob_in P₁ Q x h h') h''). } cbn. etrans. { apply maponpaths_2. exact (rwhisker_profunctor_nat_trans_mor_comm τ Q h h'). } refine (!_). etrans. { apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ (comp_profunctor Q R) h (comp_profunctor_ob_in Q R y h' h'')). } rewrite associator_profunctor_nat_trans_mor_comm. etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm P₂ Q R (τ x w h) h' h''). } apply idpath. - intros C₁ C₂ C₃ P₁ P₂ Q₁ Q₂ τ₁ τ₂. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn in *. etrans. { apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ₁ Q₁ h h'). } etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm P₂ τ₂ (τ₁ y x h) h'). } refine (!_). etrans. { apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm P₁ τ₂ h h'). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm τ₁ Q₂ h (τ₂ z y h')). } apply idpath. - intros C₁ C₂ P. exact (inv_profunctor_nat_trans_right (is_profunctor_nat_iso_lunitor_profunctor_nat_trans P)). - intros C₁ C₂ P. exact (inv_profunctor_nat_trans_left (is_profunctor_nat_iso_lunitor_profunctor_nat_trans P)). - intros C₁ C₂ P. exact (inv_profunctor_nat_trans_right (is_profunctor_nat_iso_runitor_profunctor_nat_trans P)). - intros C₁ C₂ P. exact (inv_profunctor_nat_trans_left (is_profunctor_nat_iso_runitor_profunctor_nat_trans P)). - intros C₁ C₂ C₃ C₄ P Q R. exact (inv_profunctor_nat_trans_right (is_profunctor_nat_iso_associator_profunctor_nat_trans P Q R)). - intros C₁ C₂ C₃ C₄ P Q R. exact (inv_profunctor_nat_trans_left (is_profunctor_nat_iso_associator_profunctor_nat_trans P Q R)). - intros C₁ C₂ C₃ P Q. use eq_profunctor_nat_trans. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn in *. use (mor_from_comp_profunctor_ob_eq (id_profunctor C₂) Q z y (λ h', rwhisker_profunctor_nat_trans_mor (runitor_profunctor_nat_trans P) Q z x (associator_profunctor_nat_trans_mor P (id_profunctor C₂) Q z x (comp_profunctor_ob_in P (comp_profunctor (id_profunctor C₂) Q) y h h'))) (λ h', lwhisker_profunctor_nat_trans_mor P (lunitor_profunctor_nat_trans Q) z x (comp_profunctor_ob_in P (comp_profunctor (id_profunctor C₂) Q) y h h'))). clear h'. intros y' h' h'' ; cbn in *. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P (id_profunctor C₂) Q h h' h''). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm (runitor_profunctor_nat_trans P) Q (comp_profunctor_ob_in P (id_profunctor C₂) y h h') h''). } cbn. rewrite runitor_profunctor_nat_trans_mor_comm. refine (!_). etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm P (lunitor_profunctor_nat_trans Q) h (comp_profunctor_ob_in (id_profunctor C₂) Q y' h' h'')). } cbn. rewrite lunitor_profunctor_nat_trans_mor_comm. rewrite comp_profunctor_ob_in_comm. apply idpath. - intros C₁ C₂ C₃ C₄ C₅ P₁ P₂ P₃ P₄. use eq_profunctor_nat_trans. intros z v h. use mor_from_comp_profunctor_ob_eq. clear h. intros w h k ; cbn in *. use (mor_from_comp_profunctor_ob_eq P₂ (comp_profunctor P₃ P₄) z w (λ k, rwhisker_profunctor_nat_trans_mor (associator_profunctor_nat_trans P₁ P₂ P₃) P₄ z v (associator_profunctor_nat_trans_mor P₁ (comp_profunctor P₂ P₃) P₄ z v (lwhisker_profunctor_nat_trans_mor P₁ (associator_profunctor_nat_trans P₂ P₃ P₄) z v (comp_profunctor_ob_in P₁ (comp_profunctor P₂ (comp_profunctor P₃ P₄)) w h k)))) (λ k, associator_profunctor_nat_trans_mor (comp_profunctor P₁ P₂) P₃ P₄ z v (associator_profunctor_nat_trans_mor P₁ P₂ (comp_profunctor P₃ P₄) z v (comp_profunctor_ob_in P₁ (comp_profunctor P₂ (comp_profunctor P₃ P₄)) w h k)))). clear k. intros x k l ; cbn. use (mor_from_comp_profunctor_ob_eq P₃ P₄ z x (λ l, rwhisker_profunctor_nat_trans_mor (associator_profunctor_nat_trans P₁ P₂ P₃) P₄ z v (associator_profunctor_nat_trans_mor P₁ (comp_profunctor P₂ P₃) P₄ z v (lwhisker_profunctor_nat_trans_mor P₁ (associator_profunctor_nat_trans P₂ P₃ P₄) z v (comp_profunctor_ob_in P₁ (comp_profunctor P₂ (comp_profunctor P₃ P₄)) w h (comp_profunctor_ob_in P₂ (comp_profunctor P₃ P₄) x k l))))) (λ l, associator_profunctor_nat_trans_mor (comp_profunctor P₁ P₂) P₃ P₄ z v (associator_profunctor_nat_trans_mor P₁ P₂ (comp_profunctor P₃ P₄) z v (comp_profunctor_ob_in P₁ (comp_profunctor P₂ (comp_profunctor P₃ P₄)) w h (comp_profunctor_ob_in P₂ (comp_profunctor P₃ P₄) x k l))))). clear l. intros y l m ; cbn. etrans. { do 2 apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm P₁ (associator_profunctor_nat_trans P₂ P₃ P₄) h (comp_profunctor_ob_in P₂ (comp_profunctor P₃ P₄) x k (comp_profunctor_ob_in P₃ P₄ y l m))). } cbn. rewrite !associator_profunctor_nat_trans_mor_comm. etrans. { do 2 apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P₂ P₃ P₄ k l m). } etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P₁ (comp_profunctor P₂ P₃) P₄ h (comp_profunctor_ob_in P₂ P₃ x k l) m). } etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm (associator_profunctor_nat_trans P₁ P₂ P₃) P₄ _ m). } cbn. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths_2. exact (associator_profunctor_nat_trans_mor_ob_comm P₁ P₂ P₃ h k l). } refine (!_). etrans. { apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P₁ P₂ (comp_profunctor P₃ P₄) h k _). } rewrite associator_profunctor_nat_trans_mor_comm. etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm (comp_profunctor P₁ P₂) P₃ P₄ _ l m). } 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.