fact: Definition path_homomorphism_from_free_group {S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i} {G : Group} (f g : F_S $-> G) (K : f o i == g o i) : f = g.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list