`{Univalence} {A B : Group} (f : A $-> B) : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f. 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.
Require Import Basics Types. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import WildCat.Core.