proposition: Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B) : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f.
proof: Proof. refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv). apply equiv_iff_hprop_uncurried. refine (iff_compose _ (isembedding_grouphomomorphism f)); split. - intros E ? ?. by apply E. - intros e a; split. + apply e. + intro p. exact (ap _ p @ grp_homo_unit f). Defined.
imports: Basics Types Algebra.Groups.Group Algebra.Groups.Subgroup WildCat.Core