Definition profunctor_nat_trans_weq_square {C D : category} (P Q : D ↛ C) : profunctor_nat_trans P Q ≃ profunctor_square (functor_identity _) (functor_identity _) P Q. Proof. use weq_iso. - exact profunctor_nat_trans_to_square. - exact profunctor_square_to_profunctor_nat_trans. - abstract (intros τ ; use eq_profunctor_nat_trans ; intros ; cbn ; apply idpath). - abstract (intros τ ; use eq_profunctor_square ; intros ; cbn ; apply idpath). 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.