Definition abgr_kernel_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype A := monoid_kernel_hsubtype f.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.