Replace ab_biprod_corec_eta with grp_prod_corec_natural

theories/Algebra/AbGroups/Biproduct.v

@@ -138,10 +138,6 @@ 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_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.
-
 (** *** Functoriality of [ab_biprod] *)
 
 Definition functor_ab_biprod {A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B')

theories/Algebra/AbSES/Core.v

@@ -625,11 +625,17 @@ 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_eta _ _ _ _) @ _).
-  refine (ab_biprod_functor_beta _ _ _ _ _ @ _).
+  (* The next two lines might help the reader, but both are definitional equalities:
+  lhs nrapply (ap _ (grp_prod_corec_natural _ _ _ _)).
+  lhs nrapply ab_biprod_functor_beta.
+  *)
   nrapply path_prod'.
   2: rapply cx_isexact.
-  refine (ap _ (projection_split_to_kernel_beta E h a) @ _).
+  (* The LHS of the remaining goal is definitionally equal to
+       (grp_iso_inverse (grp_iso_cxfib (isexact_inclusion_projection E)) $o
+         (projection_split_to_kernel E h $o inclusion E)) a
+     allowing us to do: *)
+  lhs nrapply (ap _ (projection_split_to_kernel_beta E h a)).
   apply eissect.
 Defined.
 

theories/Algebra/Groups/Group.v

@@ -831,20 +831,24 @@ Proof.
 Defined.
 
 (** Maps into the direct product can be built by mapping separately into each factor. *)
-Proposition grp_prod_corec {G H K : Group}
-            (f : GroupHomomorphism K G)
-            (g : GroupHomomorphism K H)
-  : GroupHomomorphism K (grp_prod G H).
+Proposition grp_prod_corec {G H K : Group} (f : K $-> G) (g : K $-> H)
+  : K $-> (grp_prod G H).
 Proof.
   snrapply Build_GroupHomomorphism.
-  - exact (fun x:K => (f x, g x)).
+  - exact (fun x : K => (f x, g x)).
   - intros x y.
-    refine (path_prod' _ _ ); try apply grp_homo_op.
+    apply path_prod'; apply grp_homo_op.
 Defined.
 
+(** [grp_prod_corec] satisfies a definitional naturality property. *)
+Definition grp_prod_corec_natural {X Y A B : Group}
+  (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
+  : grp_prod_corec g0 g1 $o f $== grp_prod_corec (g0 $o f) (g1 $o f)
+  := fun _ => idpath.
+
 (** The left factor injects into the direct product. *)
 Definition grp_prod_inl {H K : Group}
-  : GroupHomomorphism H (grp_prod H K)
+  : H $-> (grp_prod H K)
   := grp_prod_corec grp_homo_id grp_homo_const.
 
 (** The left injection is an embedding. *)
@@ -858,7 +862,7 @@ Defined.
 
 (** The right factor injects into the direct product. *)
 Definition grp_prod_inr {H K : Group}
-  : GroupHomomorphism K (grp_prod H K)
+  : K $-> (grp_prod H K)
   := grp_prod_corec grp_homo_const grp_homo_id.
 
 (** The right injection is an embedding. *)