proposition: Proposition comp_profunctor_ob_in_comm {z : C₃} {y₁ y₂ : C₂} (g : y₁ --> y₂) {x : C₁} (h : P y₂ x) (h' : Q z y₁) : comp_profunctor_ob_in y₂ h (rmap Q g h') = comp_profunctor_ob_in y₁ (lmap P g h) h'.
proof: Proof. pose (HSET_coend_comm (comp_profunctor_colim_profunctor x z) g (h ,, h')) as p. cbn in p. rewrite !profunctor_id in p. exact p. Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core