`{Funext} (G : Group) (A : Type) : (A -> G) <~> (FreeGroup A $-> G) := equiv_isfreegroupon_rec. Global Instance ishprop_isfreegroupon `{Funext} (F : Group) (A : Type) (i : A -> F) : IsHProp (IsFreeGroupOn A F i). Proof. unfold IsFreeGroupOn. apply istrunc_forall. Defined.
Require Import Basics Types Group Subgroup