proposition: 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: Proof. use mor_from_HSET_coend_eq ; cbn. intros y h. apply ps. Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core