Definition kernel_issubmonoid {A B : monoid} (f : monoidfun A B) : issubmonoid (monoid_kernel_hsubtype f). Proof. use make_issubmonoid. - intros x y. refine (monoidfunmul f _ _ @ _). refine (maponpaths _ (pr2 y) @ _). refine (runax _ _ @ _). exact (pr2 x). - apply monoidfununel. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.