Definition mor_quot_precategory_ob_mor : precategory_ob_mor. Proof. use make_precategory_ob_mor. - exact C. - exact (λ x y, setquot (λ (f g : x --> y), f ~_{ eq } g)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.