fact: Definition equiv_isfreegroupon_rec `{Funext} {G F : Group} {A : Type} {i : A -> F} `{IsFreeGroupOn A F i} : (A -> G) <~> (F $-> G) := Build_Equiv _ _ isfreegroupon_rec _.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list