`{Univalence} {A A' B : AbGroup} (alpha : A $-> A') (E : AbSES B A) (F : AbSES B A') (p : abses_pushout alpha E = F) : exists phi : middle E $-> F, inclusion F o alpha == phi o inclusion E. Proof. induction p. exists ab_pushout_inr; intro x. nrapply ab_pushout_commsq. 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.