{A B : Group} (f : A $-> B) `{IsEmbedding f} : Subgroup B. Proof. snrapply (Build_Subgroup _ (hfiber f)). repeat split. - exact _. - exact (mon_unit; grp_homo_unit f). - intros x y [a []] [b []]. exists (a * b). apply grp_homo_op. - intros b [a []]. exists (-a). apply grp_homo_inv. 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.