Definition collage_profunctor_precategory_ob_mor : precategory_ob_mor. Proof. use make_precategory_ob_mor. - exact (C₁ ⨿ C₂). - intros x₁ x₂. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ]. + exact (x₁ --> x₂). + exact ∅. + exact (P y₁ x₂). + exact (y₁ --> y₂). 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.