Proposition runitor_profunctor_nat_trans_law {C₁ C₂ : category} (P : profunctor C₁ C₂) : profunctor_nat_trans_law (runitor_profunctor_nat_trans_mor P). Proof. intros y₁ y₂ x₁ x₂ g f h. cbn. use (mor_from_comp_profunctor_ob_eq P (id_profunctor C₂) y₁ x₁ (λ h, runitor_profunctor_nat_trans_mor P y₂ x₂ (comp_profunctor_mor P (id_profunctor C₂) g (identity x₂) (comp_profunctor_mor P (id_profunctor C₂) (identity y₁) f h))) (λ h, lmap P g (rmap P f (runitor_profunctor_nat_trans_mor P y₁ x₁ h)))). clear h. intros y h h' ; cbn. rewrite !comp_profunctor_mor_comm. rewrite !runitor_profunctor_nat_trans_mor_comm ; cbn. rewrite !id_left, !id_right. rewrite rmap_id. rewrite <- lmap_rmap. rewrite lmap_comp. 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.