Proposition rwhisker_profunctor_nat_trans_law {C₁ C₂ C₃ : category} {P₁ P₂ : C₁ ↛ C₂} (τ : profunctor_nat_trans P₁ P₂) (Q : C₂ ↛ C₃) : profunctor_nat_trans_law (rwhisker_profunctor_nat_trans_mor τ Q). Proof. intros z₁ z₂ x₁ x₂ k f h ; cbn in *. use (mor_from_comp_profunctor_ob_eq P₁ Q z₁ x₁ (λ h, rwhisker_profunctor_nat_trans_mor τ Q 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 (rwhisker_profunctor_nat_trans_mor τ Q z₁ x₁ h)))). clear h. intros y h h' ; cbn. rewrite !comp_profunctor_mor_comm. rewrite rmap_id, lmap_id. etrans. { exact (rwhisker_profunctor_nat_trans_mor_comm τ Q (rmap P₁ f h) (lmap Q k h')). } refine (!_). etrans. { do 2 apply maponpaths. exact (rwhisker_profunctor_nat_trans_mor_comm τ Q h h'). } rewrite !comp_profunctor_mor_comm. rewrite rmap_id, lmap_id. rewrite profunctor_nat_trans_rmap. 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.