{X : Type} {A : AbGroup} {f f' : FreeAbGroup X $-> A} (p : forall x, f (freeabgroup_in x) = f' (freeabgroup_in x)) : f $== f'. Proof. snrapply abel_ind_homotopy. snrapply FreeGroup_ind_homotopy. snrapply p. Defined.
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.