{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. intro b. change b with (ab_biprod_pr2 (A:=A) (mon_unit, b)). refine (pullback_commsq _ _ _ @ ap i _). exact (snd p^$.2 _)^. 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.