`{Univalence} {A B : AbGroup} : (B $-> A) <~> loops (AbSES B A) := equiv_path_abses oE abses_endomorphism_trivial^-1.
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.