proposition: Lemma isunitquot {X : monoid} (R : binopeqrel X) : isunit (@op (setwithbinopquot R)) (setquotpr R (pr1 (pr2 (pr2 X)))).
proof: 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)). simpl. intro x0. apply (maponpaths (setquotpr R) (lunax X x0)). - intro x. apply (setquotunivprop R (λ x, (@op qsetwithop) x qun = x)). simpl. intro x0. apply (maponpaths (setquotpr R) (runax X x0)). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders