Definition monoid_kernel_hsubtype {A B : monoid} (f : monoidfun A B) : hsubtype A. Proof. intros a. use make_hProp. - exact (f a = 1). - apply setproperty. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.