proposition: Proposition profunctor_pentagon_law : pentagon_law profunctor_associator.
proof: 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.
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.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints