Lemma isunitquot {X : monoid} (R : binopeqrel X) : isunit (@op (setwithbinopquot R)) (setquotpr R (pr1 (pr2 (pr2 X)))). Proof. intros. set (qun := setquotpr R (pr1 (pr2 (pr2 X)))). set (qsetwithop := setwithbinopquot R). split. - intro x. apply (setquotunivprop R (λ x, (@op qsetwithop) qun x = x)%logic). simpl. intro x0. apply (maponpaths (setquotpr R) (lunax X x0)). - intro x. apply (setquotunivprop R (λ x, (@op qsetwithop) x qun = x)%logic). simpl. intro x0. apply (maponpaths (setquotpr R) (runax X x0)). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.