fact: Definition equiv_isfreegroupon_isequiv_precomp `{Funext} (F : Group) (A : Type) (i : A -> F) : IsFreeGroupOn A F i <~> forall G, IsEquiv (fun f : F $-> G => f o i).
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list