fact: Definition abgr : UU := total2 (λ X : setwithbinop, isabgrop (@op X)).
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids