fact: Definition monoid_kernel_hsubtype {A B : monoid} (f : monoidfun A B) : hsubtype A.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders