Definition collage_profunctor_precategory_data : precategory_data. Proof. use make_precategory_data. - exact collage_profunctor_precategory_ob_mor. - intro x. induction x as [ x | y ]. + exact (identity x). + exact (identity y). - intros x₁ x₂ x₃ f g. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; induction x₃ as [ x₃ | y₃ ] ; try (apply (fromempty f)) ; try (apply (fromempty g)) ; cbn in *. + exact (f · g). + exact (rmap P g f). + exact (lmap P f g). + exact (f · g). 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.