proposition: Lemma abses_pullback_inclusion_transpose_beta {A B E : AbGroup} (i : B $-> E) `{IsEmbedding i} (F : AbSES E A) (p : abses_pullback i F $== pt) : projection F $o (abses_pullback_inclusion_transpose_map i F p) == i.
proof: Proof. intro b. change b with (ab_biprod_pr2 (A:=A) (mon_unit, b)). refine (pullback_commsq _ _ _ @ ap i _). exact (snd p^$.2 _)^. Defined.
imports: Basics Types HSet HFiber Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.Pullback Modalities.Identity Modalities.Modality Truncations.Core