Definition profunctor_nat_iso_weq_iso_square {C D : category} (P Q : D ↛ C) : profunctor_nat_iso P Q ≃ profunctor_iso_square (functor_identity _) (functor_identity _) P Q. Proof. use (weqtotal2 (profunctor_nat_trans_weq_square P Q)). intro τ. use weqimplimpl. - intros Hτ y x. exact (Hτ y x). - intros Hτ y x. exact (Hτ y x). - apply isaprop_is_profunctor_nat_iso. - apply isaprop_is_profunctor_nat_iso. Defined.
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.