Proposition precomp_profunctor_laws : profunctor_laws precomp_profunctor_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core.