Proposition collage_profunctor_category_has_homsets : has_homsets collage_profunctor_precategory_ob_mor. Proof. intros x₁ x₂. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; cbn in *. - apply homset_property. - apply isasetempty. - apply setproperty. - apply homset_property. Qed.
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.