Definition collage_profunctor_square : profunctor_square collage_profunctor_category_inr collage_profunctor_category_inl P (id_profunctor _). Proof. use make_profunctor_square. - exact (λ _ _ h, h). - abstract (intro ; intros ; cbn ; rewrite rmap_id ; rewrite lmap_id ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares.