Definition make_ismonoidfun {X Y : monoid} {f : X → Y} (H1 : isbinopfun f) (H2 : f 1 = 1) : ismonoidfun f := H1 ,, H2.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.