proposition: Proposition lunitor_profunctor_nat_trans_law {C₁ C₂ : category} (P : profunctor C₁ C₂) : profunctor_nat_trans_law (lunitor_profunctor_nat_trans_mor P).
proof: Proof. intros y₁ y₂ x₁ x₂ g f h. use (mor_from_comp_profunctor_ob_eq (id_profunctor C₁) P y₁ x₁ (λ h, lunitor_profunctor_nat_trans_mor P y₂ x₂ (comp_profunctor_mor (id_profunctor C₁) P g (identity x₂) (comp_profunctor_mor (id_profunctor C₁) P (identity y₁) f h))) (λ h, lmap P g (rmap P f (lunitor_profunctor_nat_trans_mor P y₁ x₁ h)))). clear h. intros y h h' ; cbn. rewrite !comp_profunctor_mor_comm. rewrite !lunitor_profunctor_nat_trans_mor_comm ; cbn. rewrite !id_left, !id_right. rewrite lmap_id. rewrite <- lmap_rmap. rewrite rmap_comp. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Profunctors.Examples