Proposition lmap_comp_profunctor {z₁ z₂ : C₃} (k : z₂ --> z₁) {x : C₁} {y : C₂} (h : P y x) (h' : Q z₁ y) : lmap comp_profunctor k (comp_profunctor_ob_in y h h') = comp_profunctor_ob_in y h (lmap Q k h'). Proof. cbn. rewrite comp_profunctor_mor_comm. rewrite rmap_id. apply idpath. 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.