{A B : Group} (f : A $-> B) : (forall a, f a = group_unit -> a = group_unit) <-> IsEmbedding f. Proof. split. - intros h b. apply hprop_allpath. intros [a0 p0] [a1 p1]. srapply path_sigma_hprop; simpl. apply grp_moveL_1M. apply h. rewrite grp_homo_op, grp_homo_inv. rewrite p0, p1. apply right_inverse. - intros E a p. rapply (isinj_embedding f). exact (p @ (grp_homo_unit f)^). Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.