proposition: 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: Proof. use make_ismonoidfun. - refine (setquotuniv2prop' _ _ _). + intros. apply isasetmonoid. + intros. simpl. rewrite setquotfun2comm. rewrite !setquotunivcomm. apply monoidfunmul. - exact (setquotunivcomm _ _ _ _ _ @ monoidfununel _). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders