{A B : Group} (f : A $-> B) `{IsEmbedding f} : GroupIsomorphism A (grp_image_embedding f). Proof. snrapply Build_GroupIsomorphism. - snrapply Build_GroupHomomorphism. + intro x. exists (f x). exists x. reflexivity. + cbn; grp_auto. - apply isequiv_surj_emb. 2: apply (cancelL_isembedding (g:=pr1)). intros [b [a p]]; cbn. rapply contr_inhabited_hprop. refine (tr (a; _)). srapply path_sigma'. 1: exact p. refine (transport_sigma' _ _ @ _). by apply path_sigma_hprop. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import WildCat.Core. Require Import HSet.