`{Univalence} {X : Type} {B A : AbGroup@{u}} (f g : X -> AbSES B A) : (f $=> g) <~> f == g. Proof. srapply equiv_functor_forall_id; intro x; cbn. srapply equiv_path_abses_iso. 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.