abses_pullback_inclusion0_map' `{Univalence} {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) : AbSESMorphism F (abses_pullback_trivial_preimage E F p). Proof. srapply Build_AbSESMorphism. - exact grp_homo_id. - exact grp_quotient_map. - exact (projection E). - reflexivity. - reflexivity. 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.