proposition: Theorem equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B} : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const).
proof: Proof. srapply equiv_adjointify. - intro k. srefine (_ $o k; _). 1: apply subgroup_incl. intro x; cbn. exact (k x).2. - intros [g p]. exact (grp_kernel_corec _ p). - intros [g p]. apply path_sigma_hprop; unfold pr1. apply equiv_path_grouphomomorphism; intro; reflexivity. - intro k. apply equiv_path_grouphomomorphism; intro x. apply path_sigma_hprop; reflexivity. Defined.
imports: Basics Types Algebra.Groups.Group Algebra.Groups.Subgroup WildCat.Core