{A B : Group} (f : A $-> B) : Subgroup B. Proof. snrapply (Build_Subgroup' (fun b => hexists (fun a => f a = b))). - exact _. - apply tr. exists mon_unit. apply grp_homo_unit. - intros x y p q; strip_truncations; apply tr. destruct p as [a p], q as [b q]. exists (a * -b). lhs nrapply grp_homo_op; f_ap. lhs nrapply grp_homo_inv; f_ap. 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.