proposition: Proposition profunctor_hor_comp_laws : hor_comp_laws profunctor_hor_comp_data.
proof: Proof. split. - intros C D E P Q. use eq_profunctor_square. intros z x h ; cbn. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn. etrans. { apply (comp_v_profunctor_square_mor_comm (id_h_profunctor_square P) (id_h_profunctor_square Q)). } cbn. apply idpath. - intros. use eq_profunctor_square. intros z x h. use mor_from_comp_profunctor_ob_eq. clear h. intros y h h' ; cbn. etrans. { apply (comp_v_profunctor_square_mor_comm (comp_h_profunctor_square s₁ s₁') (comp_h_profunctor_square s₂ s₂')). } refine (!_). etrans. { etrans. { apply maponpaths. apply (comp_v_profunctor_square_mor_comm s₁ s₂). } apply (comp_v_profunctor_square_mor_comm s₁' s₂'). } cbn. 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