Proposition profunctor_triangle_law : triangle_law profunctor_lunitor profunctor_runitor profunctor_associator. 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.
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.