Proposition from_comp_profunctor_ob_comm (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') (y : C₂) (h : P y x) (h' : Q z y) : from_comp_profunctor_ob z x fs ps (comp_profunctor_ob_in y h h') = fs y h h'. Proof. exact (mor_from_HSET_coend_comm _ _ _ _ _). 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.