(G : Group) (X : G -> Type) := IsSurjection (subgroup_incl (subgroup_generated X)). Section FreeGroupGenerated. Context {S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}. Local to_subgroup_generated : F_S $-> subgroup_generated (hfiber i). Proof. apply isfreegroupon_rec. intro s. snrapply subgroup_generated_gen_incl. - exact (i s). - exact (s; idpath). Defined.
Require Import Basics Types Group Subgroup