`{Funext} (F : Group) (A : Type) (i : A -> F) : IsFreeGroupOn A F i <~> forall G, IsEquiv (fun f : F $-> G => f o i). Proof. srapply equiv_iff_hprop. 1: intros ? ?; exact (equiv_isequiv (equiv_isfreegroupon_rec)^-1). intros k G g. specialize (k G). snrapply contr_equiv'. 1: exact (hfiber (fun f x => grp_homo_map f (i x)) g). { rapply equiv_functor_sigma_id. intro y; symmetry. apply equiv_path_forall. } exact _. Defined.
Require Import Basics Types Group Subgroup