From b519a42f0bd3cb8897c8e525f1f32535d5f17357 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 10 Oct 2024 02:35:26 +0100
Subject: [PATCH 1/2] ind_homotopy lemma for FreeAbGroup

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: ba3e0cff-3e2d-482c-92a9-e08ef0929448 -->
---
 theories/Algebra/AbGroups/Abelianization.v   | 10 +++++++++-
 theories/Algebra/AbGroups/FreeAbelianGroup.v | 10 ++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index ff8e35bf5b..ab138b9a66 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -149,7 +149,7 @@ Section Abel.
     srapply Coeq_ind_hprop.
     exact a.
   Defined.
-
+  
   (** And its recursion version. *)
   Definition Abel_rec_hprop (P : Type) `{IsHProp P}
     (a : G -> P)
@@ -342,6 +342,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)

From a88bf226e908691849b817416a15a504b5d0a1eb Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sun, 13 Oct 2024 19:58:13 +0100
Subject: [PATCH 2/2] remove Abel_rec_hprop

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbGroups/Abelianization.v | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index ab138b9a66..8358bb2272 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -149,15 +149,6 @@ Section Abel.
     srapply Coeq_ind_hprop.
     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.