Definition submonoidtosubsetswithbinop (X : monoid) : submonoid X → @subsetswithbinop X := λ A, make_subsetswithbinop (pr1 A) (pr1 (pr2 A)).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.