Definition comp_profunctor_mor {z₁ z₂ : C₃} (k : z₂ --> z₁) {x₁ x₂ : C₁} (f : x₁ --> x₂) : comp_profunctor_ob z₁ x₁ → comp_profunctor_ob z₂ x₂. Proof. use from_comp_profunctor_ob. - exact (λ y h h', comp_profunctor_ob_in _ (rmap P f h) (lmap Q k h')). - abstract (intros y₁ y₂ g h h' ; cbn ; rewrite lmap_rmap ; rewrite comp_profunctor_ob_in_comm ; rewrite <- lmap_rmap ; apply idpath). Defined.
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.