cleanup in AbGroups

theories/Algebra/AbGroups/AbPushout.v

@@ -71,7 +71,7 @@ Proof.
   srapply path_sigma_hprop.
   refine (grp_quotient_rec_beta _ Y _ _ @ _).
   apply equiv_path_grouphomomorphism; intro bc.
-  exact (ab_biprod_rec_beta' (phi $o grp_quotient_map) bc).
+  exact (ab_biprod_rec_eta (phi $o grp_quotient_map) bc).
 Defined.
 
 (** Restricting [ab_pushout_rec] along [ab_pushout_inl] recovers the left inducing map. *)

theories/Algebra/AbGroups/Biproduct.v

@@ -47,7 +47,7 @@ Proof.
   intros [f g]. exact (ab_biprod_rec f g).
 Defined.
 
-Proposition ab_biprod_rec_beta' {A B Y : AbGroup}
+Proposition ab_biprod_rec_eta {A B Y : AbGroup}
             (u : ab_biprod A B $-> Y)
   : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
 Proof.
@@ -58,29 +58,19 @@ Proof.
   - exact (left_identity b).
 Defined.
 
-Proposition ab_biprod_rec_beta `{Funext} {A B Y : AbGroup}
-            (u : ab_biprod A B $-> Y)
-  : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) = u.
-Proof.
-  apply equiv_path_grouphomomorphism.
-  exact (ab_biprod_rec_beta' u).
-Defined.
-
-Proposition ab_biprod_rec_inl_beta `{Funext} {A B Y : AbGroup}
+Proposition ab_biprod_rec_inl_beta {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
-  : (ab_biprod_rec a b) $o ab_biprod_inl = a.
+  : (ab_biprod_rec a b) $o ab_biprod_inl == a.
 Proof.
-  apply equiv_path_grouphomomorphism.
   intro x; simpl.
   rewrite (grp_homo_unit b).
   exact (right_identity (a x)).
 Defined.
 
-Proposition ab_biprod_rec_inr_beta `{Funext} {A B Y : AbGroup}
+Proposition ab_biprod_rec_inr_beta {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
-  : (ab_biprod_rec a b) $o ab_biprod_inr = b.
+  : (ab_biprod_rec a b) $o ab_biprod_inr == b.
 Proof.
-  apply equiv_path_grouphomomorphism.
   intro y; simpl.
   rewrite (grp_homo_unit a).
   exact (left_identity (b y)).
@@ -93,19 +83,22 @@ Proof.
   - intro phi.
     exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr).
   - intro phi.
-    exact (ab_biprod_rec_beta phi).
+    apply equiv_path_grouphomomorphism.
+    exact (ab_biprod_rec_eta phi).
   - intros [a b].
     apply path_prod.
-    + apply ab_biprod_rec_inl_beta.
-    + apply ab_biprod_rec_inr_beta.
+    + apply equiv_path_grouphomomorphism.
+      apply ab_biprod_rec_inl_beta.
+    + apply equiv_path_grouphomomorphism.
+      apply ab_biprod_rec_inr_beta.
 Defined.
 
 (** Corecursion principle, inherited from Groups/Group.v. *)
 Definition ab_biprod_corec {A B X : AbGroup} (f : X $-> A) (g : X $-> B)
   : X $-> ab_biprod A B
   := grp_prod_corec f g.
 
-Definition ab_corec_beta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
+Definition ab_corec_eta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
   : ab_biprod_corec g0 g1 $o f $== ab_biprod_corec (g0 $o f) (g1 $o f)
   := fun _ => idpath.
 
@@ -190,17 +183,26 @@ Proof.
   - exact (left_identity _)^.
 Defined.
 
+Lemma ab_biprod_corec_eta' {A B X : AbGroup} (f g : ab_biprod A B $-> X)
+  : (f $o ab_biprod_inl $== g $o ab_biprod_inl)
+  -> (f $o ab_biprod_inr $== g $o ab_biprod_inr)
+  -> f $== g.
+Proof.
+  intros h k.
+  intros [a b].
+  refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
+  refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
+  exact (ap011 (+) (h a) (k b)).
+Defined.
+
 (* Maps out of biproducts are determined on the two inclusions. *)
 Lemma equiv_path_biprod_corec `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
   : ((phi $o ab_biprod_inl == psi $o ab_biprod_inl) * (phi $o ab_biprod_inr == psi $o ab_biprod_inr))
       <~> phi == psi.
 Proof.
   apply equiv_iff_hprop.
   - intros [h k].
-    intros [a b].
-    refine (ap phi (ab_biprod_decompose _ _) @ _ @ ap psi (ab_biprod_decompose _ _)^).
-    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-    exact (ap011 (+) (h a) (k b)).
+    apply ab_biprod_corec_eta'; assumption.
   - intro h.
     exact (fun a => h _, fun b => h _).
 Defined.

theories/Algebra/AbSES/Core.v

@@ -625,7 +625,7 @@ Proposition projection_split_beta {B A : AbGroup} (E : AbSES B A)
   : projection_split_iso E h o (inclusion _) == ab_biprod_inl.
 Proof.
   intro a.
-  refine (ap _ (ab_corec_beta _ _ _ _) @ _).
+  refine (ap _ (ab_corec_eta _ _ _ _) @ _).
   refine (ab_biprod_functor_beta _ _ _ _ _ @ _).
   nrapply path_prod'.
   2: rapply cx_isexact.