{A B G : Group} {f : A $-> B} (g : G $-> A) (h : f $o g == grp_homo_const) : G $-> grp_kernel f. Proof. snrapply Build_GroupHomomorphism. - exact (fun x:G => (g x; h x)). - intros x x'. apply path_sigma_hprop; cbn. apply grp_homo_op. Defined.
Require Import Basics Types. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import WildCat.Core.