fact: Definition abgr_kernel_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype A := monoid_kernel_hsubtype f.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids