abses_pullback_splits_induced_map' {A B C : AbGroup} (E : AbSES C B) (Y : AbSES C A) : ab_biprod A B $-> abses_pullback (projection E) Y. Proof. srapply (ab_biprod_rec (inclusion _)). srapply grp_pullback_corec. - exact grp_homo_const. - exact (inclusion E). - intro x. refine (grp_homo_unit _ @ _). symmetry; apply iscomplex_abses. 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.