diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index ff8e35bf5b..8358bb2272 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -150,15 +150,6 @@ Section Abel.
     exact a.
   Defined.
 
-  (** And its recursion version. *)
-  Definition Abel_rec_hprop (P : Type) `{IsHProp P}
-    (a : G -> P)
-    : Abel -> P.
-  Proof.
-    apply (Abel_rec _ a).
-    intros; apply path_ishprop.
-  Defined.
-
 End Abel.
 
 (** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
@@ -342,6 +333,14 @@ Proof.
   apply grp_homo_op.
 Defined.
 
+Definition abel_ind_homotopy {G H : Group} {f g : Hom (A:=Group) (abel G) H}
+  (p : f $o abel_unit $== g $o abel_unit)
+  : f $== g.
+Proof.
+  rapply Abel_ind_hprop.
+  rapply p.
+Defined.
+
 (** Finally we can prove that our construction abel is an abelianization. *)
 Global Instance isabelianization_abel {G : Group}
   : IsAbelianization (abel G) abel_unit.
diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v
index 1d3558b7b7..338c9a6dad 100644
--- a/theories/Algebra/AbGroups/FreeAbelianGroup.v
+++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v
@@ -43,6 +43,16 @@ Definition FreeAbGroup_rec_beta_in {S : Type} {A : AbGroup} (f : S -> A)
   : FreeAbGroup_rec f o freeabgroup_in == f
   := fun _ => idpath.
 
+Definition FreeAbGroup_ind_homotopy {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.
+
 (** The abelianization of a free group on a set is a free abelian group on that set. *)
 Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext}
   {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A)