proposition: Lemma abses_kernel_iso_inv_beta `{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: Proof. rapply (equiv_ind (abses_kernel_iso i p)); intro a. exact (ap i (eissect (abses_kernel_iso i p) _)). Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse