{B A : AbGroup} (E : AbSES B A) {s : B $-> E} (h : projection _ $o s == idmap) : (middle E) $-> (@ab_kernel E B (projection _)). Proof. snrapply (grp_kernel_corec (G:=E) (A:=E)). - refine (ab_homo_add grp_homo_id (grp_homo_compose ab_homo_negation (s $o (projection _)))). - intro x; simpl. refine (grp_homo_op (projection _) x _ @ _). refine (ap (fun y => (projection _) x + y) _ @ right_inverse ((projection _) x)). refine (grp_homo_inv _ _ @ ap negate _ ). apply h. Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.