AbGroups/AbHom.v: prove is1bifunctor_ab_hom

HoTT · Mar 8, 2024 · 62b8d2b · 62b8d2b
1 parent 1046b48
commit 62b8d2b
Showing 1 changed file with 34 additions and 0 deletions.
diff --git 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. *)