Definition is_profunctor_nat_iso_runitor_profunctor_nat_trans {C₁ C₂ : category} (P : profunctor C₁ C₂) : is_profunctor_nat_iso (runitor_profunctor_nat_trans P). Proof. intros y x. use isweq_iso. - refine (λ h, comp_profunctor_ob_in _ _ _ h _). exact (identity y). - abstract (intro h ; use (mor_from_comp_profunctor_ob_eq P (id_profunctor C₂) _ _ (λ h, comp_profunctor_ob_in P (id_profunctor C₂) _ (runitor_profunctor_nat_trans P y x h) (identity y)) (idfun _)) ; clear h ; intros z h h' ; cbn ; rewrite runitor_profunctor_nat_trans_mor_comm ; rewrite <- comp_profunctor_ob_in_comm ; cbn ; rewrite !id_left ; apply idpath). - abstract (intro h ; cbn ; rewrite runitor_profunctor_nat_trans_mor_comm ; rewrite lmap_id; apply idpath). Defined.
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.