proposition: Proposition profunctor_lunitor_laws : double_lunitor_laws profunctor_lunitor_data.
proof: Proof. intros C₁ C₂ D₁ D₂ P Q F₁ F₂ τ. use eq_profunctor_square. intros y x h. etrans. { apply transportf_disp_mor2_profunctors. } cbn in *. use (mor_from_comp_profunctor_ob_eq (id_profunctor _) P y x (λ h, τ y x (lunitor_profunctor_nat_trans_mor P y x h)) (λ h, lunitor_profunctor_nat_trans_mor Q (F₂ y) (F₁ x) (comp_v_profunctor_square_mor (id_v_profunctor_square _) τ y x h))). clear h. intros z h h' ; cbn. refine (!_). etrans. { apply maponpaths. apply (comp_v_profunctor_square_mor_comm (id_v_profunctor_square _) τ). } rewrite !lunitor_profunctor_nat_trans_mor_comm ; cbn. rewrite (profunctor_square_rmap τ). 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