proposition: Proposition profunctor_square_rmap {C₁ C₂ D₁ D₂ : category} {F : C₁ ⟶ C₂} {G : D₁ ⟶ D₂} {P : D₁ ↛ C₁} {Q : D₂ ↛ C₂} (τ : profunctor_square F G P Q) {y : C₁} {x₁ x₂ : D₁} (f : x₁ --> x₂) (h : P y x₁) : τ y x₂ (rmap P f h) = rmap Q (#G f) (τ y x₁ h).
proof: Proof. pose (eqtohomot (pr2 τ (y ,, x₁) (y ,, x₂) (identity _ ,, f)) h) as p. cbn in p. rewrite functor_id in p. rewrite lmap_id in p. exact p. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Profunctors.Examples UniMath.CategoryTheory.Profunctors.Transformation