proposition: Proposition representable_profunctor_right_laws : profunctor_laws representable_profunctor_right_data.
proof: Proof. repeat split ; intros ; cbn. - rewrite functor_id. rewrite id_left, id_right. apply idpath. - rewrite functor_comp. rewrite !assoc'. apply idpath. - apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core