Proposition has_homsets_mor_quot_category : has_homsets mor_quot_precategory. Proof. intros x y. apply isasetsetquot. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.