`{Univalence} {B A : AbGroup} (E : AbSES B A) : merely {s : GroupHomomorphism B E & (projection _) $o s == idmap} <~> (tr E = point (Ext B A)). Proof. refine (equiv_path_Tr _ _ oE _). srapply equiv_iff_hprop; apply Trunc_functor; apply iff_abses_trivial_split. Defined.
Require Import Basics Types Truncations.Core. Require Import Pointed WildCat. Require Import Truncations.SeparatedTrunc. Require Import AbelianGroup AbHom AbProjective. Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.