proposition: Proposition precomp_profunctor_laws : profunctor_laws precomp_profunctor_data.
proof: Proof. repeat split ; intros ; cbn -[lmap rmap]. - rewrite !functor_id. rewrite lmap_id, rmap_id. apply idpath. - rewrite !functor_comp. rewrite lmap_comp. rewrite rmap_comp. apply maponpaths. rewrite lmap_rmap. apply idpath. - apply setproperty. Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core