Definition abgr_Kernel_subabgr_issubgr {A B : abgr} (f : monoidfun A B) : issubgr (abgr_kernel_hsubtype f). Proof. use make_issubgr. - apply kernel_issubmonoid. - intros x a. apply (grrcan B (f x)). refine (! (binopfunisbinopfun f (grinv A x) x) @ _). refine (maponpaths (λ a : A, f a) (grlinvax A x) @ _). refine (monoidfununel f @ !_). refine (lunax B (f x) @ _). exact a. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.