Definition idtoiso_in_collage_inr {x₁ x₂ : C₂} (p : x₁ = x₂) : pr1 (idtoiso p) = pr1 (@idtoiso collage_profunctor_category (inr x₁) (inr x₂) (maponpaths inr p)).
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.