`{Univalence} {B A : AbGroup@{u}} (E : AbSES B A) : {s : B $-> E & (projection _) $o s == idmap} <-> (E = point (AbSES B A)). 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.
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.