proposition: Proposition iff_abses_trivial_split `{Univalence} {B A : AbGroup@{u}} (E : AbSES B A) : {s : B $-> E & (projection _) $o s == idmap} <-> (E = point (AbSES B A)).
proof: Proof. refine (iff_compose _ (iff_equiv equiv_path_abses_iso)); split. - intros [s h]. exists (projection_split_iso E h). split. + nrapply projection_split_beta. + reflexivity. - intros [phi [g h]]. exists (grp_homo_compose (grp_iso_inverse phi) ab_biprod_inr). intro x; cbn. exact (h _ @ ap snd (eisretr _ _)). Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse