`{Funext} {A E B : AbGroup} (f : A $-> E) (g : GroupHomomorphism E B) `{IsSurjection g, IsExact (Tr (-1)) _ _ _ f g} : (abses_cokernel_iso f g)^-1 o g == grp_quotient_map. Proof. intro x; by apply moveR_equiv_V. 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.