Proposition profunctor_pentagon_law : pentagon_law profunctor_associator. Proof. intros C₁ C₂ C₃ C₄ C₅ P₁ P₂ P₃ P₄. use eq_profunctor_square. intros z v h. etrans. { apply transportf_disp_mor2_profunctors. } use mor_from_comp_profunctor_ob_eq. clear h. intros w h₁ h. cbn in *. use (mor_from_comp_profunctor_ob_eq P₂ (comp_profunctor P₃ P₄) z w (λ h, 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₁ h))) (λ h, comp_v_profunctor_square_mor (associator_profunctor_square P₁ P₂ P₃) (id_h_profunctor_square P₄) z v (associator_profunctor_nat_trans_mor P₁ (comp_profunctor P₂ P₃) P₄ z v (comp_v_profunctor_square_mor (id_h_profunctor_square P₁) (associator_profunctor_square P₂ P₃ P₄) z v (comp_profunctor_ob_in P₁ (comp_profunctor P₂ (comp_profunctor P₃ P₄)) w h₁ h))))). clear h. intros x h₂ h ; cbn. use (mor_from_comp_profunctor_ob_eq P₃ P₄ z x (λ h, 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 h₂ h)))) (λ h, comp_v_profunctor_square_mor (associator_profunctor_square P₁ P₂ P₃) (id_h_profunctor_square P₄) z v (associator_profunctor_nat_trans_mor P₁ (comp_profunctor P₂ P₃) P₄ z v (comp_v_profunctor_square_mor (id_h_profunctor_square P₁) (associator_profunctor_square 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 h₂ h)))))). clear h. intros y h₃ h₄ ; cbn. etrans. { rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. apply (associator_profunctor_nat_trans_mor_ob_comm P₁ P₂ (comp_profunctor P₃ P₄)). } rewrite associator_profunctor_nat_trans_mor_comm. exact (associator_profunctor_nat_trans_mor_ob_comm (comp_profunctor P₁ P₂) P₃ P₄ (comp_profunctor_ob_in P₁ P₂ w h₁ h₂) h₃ h₄). } refine (!_). etrans. { etrans. { do 2 apply maponpaths. apply (comp_v_profunctor_square_mor_comm (id_h_profunctor_square P₁) (associator_profunctor_square P₂ P₃ P₄)). } cbn. rewrite !associator_profunctor_nat_trans_mor_comm. etrans. { do 2 apply maponpaths. apply associator_profunctor_nat_trans_mor_ob_comm. } etrans. { apply maponpaths. apply associator_profunctor_nat_trans_mor_ob_comm. } etrans. { apply (comp_v_profunctor_square_mor_comm (associator_profunctor_square P₁ P₂ P₃) (id_h_profunctor_square P₄)). } cbn. rewrite associator_profunctor_nat_trans_mor_comm. apply maponpaths_2. apply associator_profunctor_nat_trans_mor_ob_comm. } 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.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints.