{B A : AbGroup@{u}} {E F : AbSES B A} (phi : GroupHomomorphism E F) (p0 : phi $o inclusion E == inclusion F) (p1 : projection E == projection F $o phi) : IsEquiv phi. Proof. apply isequiv_surj_emb. - intro f. rapply contr_inhabited_hprop. assert (e0 : Tr (-1) (hfiber (projection E) (projection F f))). 1: apply center, issurjection_projection. strip_truncations. assert (a : Tr (-1) (hfiber (inclusion F) (f + (- phi e0.1)))). 1: { refine (isexact_preimage (Tr (-1)) (inclusion F) (projection F) _ _). refine (grp_homo_op _ _ _ @ _). refine (ap _ (grp_homo_inv _ _) @ _). apply (grp_moveL_1M)^-1. exact (e0.2^ @ p1 e0.1). } strip_truncations. refine (tr (inclusion E a.1 + e0.1; _)). refine (grp_homo_op _ _ _ @ _). refine (ap (fun x => x + phi e0.1) (p0 a.1 @ a.2) @ _). refine ((grp_assoc _ _ _)^ @ _). refine (ap _ (left_inverse (phi e0.1)) @ _). apply grp_unit_r. - apply isembedding_grouphomomorphism. intros e p. assert (a : Tr (-1) (hfiber (inclusion E) e)). 1: { refine (isexact_preimage _ (inclusion E) (projection E) _ _). exact (p1 e @ ap (projection F) p @ grp_homo_unit _). } strip_truncations. refine (a.2^ @ ap (inclusion E ) _ @ grp_homo_unit (inclusion E)). rapply (isinj_embedding (inclusion F) _ _). refine ((p0 a.1)^ @ (ap phi a.2) @ p @ (grp_homo_unit _)^). 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.