proposition: Proposition profunctor_triangle_law : triangle_law profunctor_lunitor profunctor_runitor profunctor_associator.
proof: Proof. intros C₁ C₂ C₃ P Q. use eq_profunctor_square. intros z x h. refine (!_). etrans. { apply transportf_disp_mor2_profunctors. } cbn in *. use (mor_from_comp_profunctor_ob_eq P (comp_profunctor (id_profunctor C₂) Q) _ _ (λ h, comp_v_profunctor_square_mor (id_h_profunctor_square P) (lunitor_profunctor_square Q) z x h) (λ h, comp_v_profunctor_square_mor (runitor_profunctor_square P) (id_h_profunctor_square Q) z x (associator_profunctor_nat_trans_mor P (id_profunctor C₂) Q z x h))). clear h. intros y h kl ; cbn. use (mor_from_comp_profunctor_ob_eq (id_profunctor C₂) Q z y (λ kl, comp_v_profunctor_square_mor (id_h_profunctor_square P) (lunitor_profunctor_square Q) z x (comp_profunctor_ob_in P (comp_profunctor (id_profunctor C₂) Q) y h kl)) (λ kl, comp_v_profunctor_square_mor (runitor_profunctor_square P) (id_h_profunctor_square 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 kl)))). clear kl. intros y' k l ; cbn. etrans. { apply (comp_v_profunctor_square_mor_comm (id_h_profunctor_square P) (lunitor_profunctor_square Q) z x). } cbn. rewrite lunitor_profunctor_nat_trans_mor_comm. rewrite associator_profunctor_nat_trans_mor_comm. refine (!_). etrans. { apply maponpaths. apply associator_profunctor_nat_trans_mor_ob_comm. } etrans. { apply (comp_v_profunctor_square_mor_comm (runitor_profunctor_square P) (id_h_profunctor_square Q) z x). } cbn. rewrite runitor_profunctor_nat_trans_mor_comm. rewrite comp_profunctor_ob_in_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