abses_pushout_compose' `{Univalence} {A0 A1 A2 B : AbGroup} (f : A0 $-> A1) (g : A1 $-> A2) : abses_pushout (g $o f) $=> abses_pushout (B:=B) g o abses_pushout f. Proof. intro E. srapply abses_path_data_to_iso; srefine (_; (_,_)). - snrapply ab_pushout_rec. + apply inclusion. + exact (component2 (abses_pushout_morphism _ g) $o component2 (abses_pushout_morphism _ f)). + intro a0. refine (left_square (abses_pushout_morphism _ g) _ @ _). exact (ap (component2 (abses_pushout_morphism (abses_pushout f E) g)) (left_square (abses_pushout_morphism _ f) a0)). - apply ab_pushout_rec_beta_left. - srapply Quotient_ind_hprop. intro x; simpl. apply grp_cancelL; symmetry. exact (left_identity _ @ ap (projection E) (left_identity _)). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.