proposition: 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: Proof. exact (mor_from_HSET_coend_comm _ _ _ _ _). Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core