{B A : AbGroup@{u}} (E : AbSES B A) {s : GroupHomomorphism B E} (h : (projection _) $o s == idmap) : GroupIsomorphism E (ab_biprod A B). Proof. etransitivity (ab_biprod (ab_kernel _) B). - exact (projection_split_iso1 E h). - srapply (equiv_functor_ab_biprod (grp_iso_inverse _) grp_iso_id). rapply grp_iso_cxfib. 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.