Proposition profunctor_square_lmap {C₁ C₂ D₁ D₂ : category} {F : C₁ ⟶ C₂} {G : D₁ ⟶ D₂} {P : D₁ ↛ C₁} {Q : D₂ ↛ C₂} (τ : profunctor_square F G P Q) {y₁ y₂ : C₁} {x : D₁} (g : y₂ --> y₁) (h : P y₁ x) : τ y₂ x (lmap P g h) = lmap Q (#F g) (τ y₁ x h). Proof. pose (eqtohomot (pr2 τ (y₁ ,, x) (y₂ ,, x) (g ,, identity _)) h) as p. cbn in p. rewrite functor_id in p. rewrite rmap_id in p. exact p. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.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. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Transformation.