proposition: 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: Proof. cbn. rewrite comp_profunctor_mor_comm. rewrite rmap_id. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core