`{Univalence} {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) : AbSES C A. Proof. snrapply Build_AbSES. - exact (abses_pullback_inclusion_transpose_endpoint' (inclusion E) F p). - exact (grp_quotient_map $o inclusion F). - srapply (ab_cokernel_embedding_rec _ (projection E $o projection F)). intro b. refine (ap (projection E) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b) @ _). apply iscomplex_abses. - apply isembedding_grouphomomorphism. intros a q0. pose proof (in_coset := related_quotient_paths _ _ _ q0). destruct in_coset as [b q1]; rewrite grp_unit_r in q1. assert (q2 : ab_biprod_inr b = ab_biprod_inl (-a)). 1: { apply (isinj_embedding (grp_pullback_pr1 _ _ $o p^$.1)). - apply abses_pullback_inclusion_lemma. exact _. - nrefine (q1 @ _); symmetry. refine (ap (grp_pullback_pr1 _ _) (fst p^$.2 (-a)) @ _). exact (grp_homo_inv _ _). } pose proof (q3 := ap negate (fst ((equiv_path_prod _ _)^-1 q2))); cbn in q3. exact ((negate_involutive _)^ @ q3^ @ negate_mon_unit). - apply (cancelR_conn_map (Tr (-1)) grp_quotient_map). 1: exact _. simpl. exact _. - snrapply Build_IsExact. + srapply phomotopy_homotopy_hset. intro a; simpl. refine (ap (projection E) _ @ _). 1: apply iscomplex_abses. apply grp_homo_unit. + intros [y q]. apply (@contr_inhabited_hprop _ _). assert (f : merely (hfiber grp_quotient_map y)). 1: apply center, issurj_class_of. revert_opaque f; apply Trunc_rec; intros [f q0]. assert (b : merely (hfiber (inclusion E) (projection F f))). 1: { rapply isexact_preimage. exact (ap _ q0 @ q). } revert_opaque b; apply Trunc_rec; intros [b q1]. assert (a : merely (hfiber (inclusion F) (sg_op f (-(grp_pullback_pr1 _ _ (p^$.1 (ab_biprod_inr b))))))). 1: { rapply isexact_preimage. refine (grp_homo_op _ _ _ @ _). refine (ap (fun x => _ + x) (grp_homo_inv _ _) @ _). refine (ap (fun x => _ - x) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b @ q1) @ _). apply right_inverse. } revert_opaque a; apply Trunc_rec; intros [a q2]. refine (tr (a; _)). let T := type of y in apply (@path_sigma_hprop T). 1: intros ?; apply istrunc_paths; apply group_isgroup. refine (ap grp_quotient_map q2 @ _ @ q0). refine (grp_homo_op _ _ _ @ _). apply grp_moveR_Mg. refine (_ @ (left_inverse _)^). apply qglue. exists b. refine (_ @ (grp_unit_r _)^). exact (negate_involutive _)^. Defined.
Require Import Basics Types HSet HFiber Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.Pullback. Require Import Modalities.Identity Modalities.Modality Truncations.Core.