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. 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.
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.