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