Proposition mor_from_comp_profunctor_ob_eq (z : C₃) (x : C₁) {X : hSet} (f g : comp_profunctor_ob z x → X) (w : comp_profunctor_ob z x) (ps : ∏ (y : C₂) (h : P y x) (h' : Q z y), f (comp_profunctor_ob_in y h h') = g (comp_profunctor_ob_in y h h')) : f w = g w. Proof. use mor_from_HSET_coend_eq ; cbn. intros y h. apply ps. 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.