From 62b8d2b4ebbee7a758065b87c6052a4354b84ed9 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Fri, 8 Mar 2024 12:02:47 -0700
Subject: [PATCH] AbGroups/AbHom.v: prove is1bifunctor_ab_hom

---
 theories/Algebra/AbGroups/AbHom.v | 34 +++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
index 98e3da60140..fcc5b53dfbd 100644
--- a/theories/Algebra/AbGroups/AbHom.v
+++ b/theories/Algebra/AbGroups/AbHom.v
@@ -63,12 +63,46 @@ Proof.
   by apply equiv_path_grouphomomorphism.
 Defined.
 
+Global Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
+  : Is1Functor (ab_hom A).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros B B' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (p (phi a)).
+  - intros B phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros B C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
+Global Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
+  : Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros A A' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (ap phi (p a)).
+  - intros A phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros A C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
 Global Instance is0bifunctor_ab_hom `{Funext}
   : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
   rapply Build_Is0Bifunctor.
 Defined.
 
+Global Instance is1bifunctor_ab_hom `{Funext}
+  : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Proof.
+  rapply Build_Is1Bifunctor.
+  intros A A' f B B' g phi; cbn.
+  by apply equiv_path_grouphomomorphism.
+Defined.
+
 (** ** Properties of [ab_hom] *)
 
 (** Precomposition with a surjection is an embedding. *)