`{Funext} {A B C Y : AbGroup} {f : A $-> B} {g : A $-> C} : IsEquiv (ab_pushout_rec_uncurried f g Y). Proof. srapply isequiv_adjointify. - intro phi. refine (phi $o ab_pushout_inl; phi $o ab_pushout_inr; _). intro a. apply (ap phi). exact (ab_pushout_commsq a). - intro phi. exact (ab_pushout_rec_beta phi). - intros [b [c p]]. srapply path_sigma. + apply equiv_path_grouphomomorphism. intro x; simpl. refine (ap (fun k => b x + k) (grp_homo_unit c) @ _). apply right_identity. + refine (transport_sigma' _ _ @ _). apply path_sigma_hprop; simpl. apply equiv_path_grouphomomorphism. intro y; simpl. refine (ap (fun k => k + c y) (grp_homo_unit b) @ _). apply left_identity. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.