Definition mor_quot_precategory_data : precategory_data. Proof. use make_precategory_data. - exact mor_quot_precategory_ob_mor. - exact (λ x, setquotpr _ (identity x)). - intros x y z. use setquotfun2'. + exact (λ f g, f · g). + unfold iscomprelrelfun2' ; cbn. split. * abstract (intros f f' g p ; use (mor_cong_rel_congruence p) ; apply eqrelrefl). * abstract (intros f g g' q ; use (mor_cong_rel_congruence _ q) ; apply eqrelrefl). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.