Proposition lwhisker_profunctor_nat_trans_law {C₁ C₂ C₃ : category} (P : C₁ ↛ C₂) {Q₁ Q₂ : C₂ ↛ C₃} (τ : profunctor_nat_trans Q₁ Q₂) : profunctor_nat_trans_law (lwhisker_profunctor_nat_trans_mor P τ). Proof. intros z₁ z₂ x₁ x₂ k f h ; cbn in *. use (mor_from_comp_profunctor_ob_eq P Q₁ z₁ x₁ (λ h, lwhisker_profunctor_nat_trans_mor P τ z₂ x₂ (comp_profunctor_mor P Q₁ k (identity x₂) (comp_profunctor_mor P Q₁ (identity z₁) f h))) (λ h, comp_profunctor_mor P Q₂ k (identity x₂) (comp_profunctor_mor P Q₂ (identity z₁) f (lwhisker_profunctor_nat_trans_mor P τ z₁ x₁ h)))). clear h. intros y h h' ; cbn. rewrite !comp_profunctor_mor_comm. rewrite rmap_id, lmap_id. etrans. { exact (lwhisker_profunctor_nat_trans_mor_comm P τ (rmap P f h) (lmap Q₁ k h')). } refine (!_). etrans. { do 2 apply maponpaths. exact (lwhisker_profunctor_nat_trans_mor_comm P τ h h'). } rewrite !comp_profunctor_mor_comm. rewrite rmap_id, lmap_id. rewrite profunctor_nat_trans_lmap. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. 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.