fact: Definition make_abmonoid : ∏ (t : setwithbinop), (λ X : setwithbinop, isabmonoidop op) t → ∑ X : setwithbinop, isabmonoidop op := tpair (λ X : setwithbinop, isabmonoidop (@op X)).
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders