proposition: Proposition grp_kernel_corec {A B G : Group} {f : A $-> B} (g : G $-> A) (h : f $o g == grp_homo_const) : G $-> grp_kernel f.
proof: 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.
imports: Basics Types Algebra.Groups.Group Algebra.Groups.Subgroup WildCat.Core