abses_pullback_inclusion_transpose_endpoint' {A B E : AbGroup} (i : B $-> E) `{IsEmbedding i} (F : AbSES E A) (p : abses_pullback i F $== pt) : AbGroup := ab_cokernel_embedding (abses_pullback_inclusion_transpose_map i F p).
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.