{B A : AbGroup} (E : AbSES B A) {s : GroupHomomorphism B E} (h : (projection _) $o s == idmap) : GroupIsomorphism E (ab_biprod (@ab_kernel E B (projection _)) B). Proof. srapply Build_GroupIsomorphism. - refine (ab_biprod_corec _ (projection _)). exact (projection_split_to_kernel E h). - srapply isequiv_adjointify. + refine (ab_biprod_rec _ s). rapply subgroup_incl. + intros [a b]; simpl. apply path_prod'. * srapply path_sigma_hprop; cbn. refine ((associativity _ _ _)^ @ _). apply grp_cancelL1. refine (ap _ _ @ right_inverse _). apply (ap negate). apply (ap s). refine (grp_homo_op (projection _) a.1 (s b) @ _). exact (ap (fun y => y + _) a.2 @ left_identity _ @ h b). * refine (grp_homo_op (projection _) a.1 (s b) @ _). exact (ap (fun y => y + _) a.2 @ left_identity _ @ h b). + intro e; simpl. by apply grp_moveR_gM. 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.