Proposition is_precategory_mor_quot : is_precategory mor_quot_precategory_data. Proof. use make_is_precategory_one_assoc. - intros x y. use setquotunivprop'. + intro. apply isasetsetquot. + intro f. cbn. rewrite id_left. reflexivity. - intros x y. use setquotunivprop'. + intro. apply isasetsetquot. + intro f. cbn. rewrite id_right. reflexivity. - intros w x y z. use setquotunivprop'. { intro. use impred ; intro. use impred ; intro. apply isasetsetquot. } intro f. use setquotunivprop'. { intro. use impred ; intro. apply isasetsetquot. } intro g. use setquotunivprop'. { intro. apply isasetsetquot. } intro h. cbn. rewrite assoc. reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.