(S : Type) (F_S : AbGroup) (i : S -> F_S) (A : AbGroup) (g : S -> A) : Type := {f : F_S $-> A & f o i == g}.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences. Require Import Types.Sigma Types.Forall Types.Paths. Require Import WildCat.Core WildCat.EquivGpd WildCat.Universe. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization. Require Import Algebra.Groups.FreeGroup. Require Import Spaces.List.Core.