Proposition profunctor_hor_comp_laws : hor_comp_laws profunctor_hor_comp_data. 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.
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.