Lemma ismonoidfun_setquotuniv {X Y : monoid} {R : binopeqrel X} (f : monoidfun X Y) (H : iscomprelfun R f) : @ismonoidfun (monoidquot R) Y (setquotuniv R Y f H). Proof. use make_ismonoidfun. - refine (setquotuniv2prop' _ _ _). + intros. apply isasetmonoid. + intros. simpl. rewrite setquotfun2comm. rewrite !setquotunivcomm. apply monoidfunmul. - exact (setquotunivcomm _ _ _ _ _ @ monoidfununel _). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.