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