proposition: Proposition lmap_rmap_functor {C₁ C₂ : category} (P : profunctor C₁ C₂) {x₁ x₂ : C₁} {y₁ y₂ : C₂} (f : x₁ --> x₂) (g : y₂ --> y₁) (z : P y₁ x₁) : lmap P g (rmap P f z) = P #[ g , f ] z.
proof: Proof. unfold lmap, rmap ; cbn. rewrite <- profunctor_comp. rewrite !id_right. apply idpath. Qed.
imports: UniMath.Foundations.Preamble UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.All