`{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B) `{IsEmbedding i, IsExact (Tr (-1)) _ _ _ i p} : i o (abses_kernel_iso i p)^-1 == subgroup_incl _. Proof. rapply (equiv_ind (abses_kernel_iso i p)); intro a. exact (ap i (eissect (abses_kernel_iso i p) _)). 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.