Definition from_comp_profunctor_ob (z : C₃) (x : C₁) {X : hSet} (fs : ∏ (y : C₂), P y x → Q z y → X) (ps : ∏ (y₁ y₂ : C₂) (g : y₁ --> y₂) (h : P y₂ x) (h' : Q z y₁), fs y₂ h (rmap Q g h') = fs y₁ (lmap P g h) h') : comp_profunctor_ob z x → X. Proof. use mor_from_HSET_coend. - exact (λ y h, fs y (pr1 h) (pr2 h)). - abstract (cbn ; intros y₁ y₂ g h ; rewrite !profunctor_id ; rewrite <- lmap_functor, <- rmap_functor ; apply ps). Defined.
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.