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