proposition: Proposition comp_profunctor_colim_profunctor_data_laws (x : C₁) (z : C₃) : profunctor_laws (comp_profunctor_colim_profunctor_data x z).
proof: Proof. repeat split ; intros ; cbn. - rewrite !profunctor_id. apply idpath. - rewrite <- !profunctor_comp. rewrite !id_right. apply idpath. - apply isasetdirprod ; 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