{A B E : AbGroup} (i : B $-> E) `{IsEmbedding i} (F : AbSES E A) (p : abses_pullback i F $== pt) : B $-> F := grp_pullback_pr1 _ _ $o p^$.1 $o ab_biprod_inr. Local Instance abses_pullback_inclusion_lemma {A B E : AbGroup} (i : B $-> E) `{IsEmbedding i} (F : AbSES E A) (p : abses_pullback i F $== pt) : IsEmbedding (grp_pullback_pr1 _ _ $o p^$.1). Proof. nrapply (istruncmap_compose (-1) p^$.1 (grp_pullback_pr1 (projection F) i)). all: rapply istruncmap_mapinO_tr. 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.