`{Funext} {B A : AbGroup@{u}} : {phi : GroupHomomorphism (point (AbSES B A)) (point (AbSES B A)) & (phi o inclusion _ == inclusion _) * (projection _ == projection _ o phi)} <~> (B $-> A). Proof. srapply equiv_adjointify. - intros [phi _]. exact (ab_biprod_pr1 $o phi $o ab_biprod_inr). - intro f. snrefine (_;_). + refine (ab_biprod_rec ab_biprod_inl _). refine (ab_biprod_corec f grp_homo_id). + split; intro x; cbn. * apply path_prod; cbn. -- exact (ap _ (grp_homo_unit f) @ right_identity _). -- exact (right_identity _). * exact (left_identity _)^. - intro f. rapply equiv_path_grouphomomorphism; intro b; cbn. exact (left_identity _). - intros [phi [p q]]. apply path_sigma_hprop; cbn. rapply equiv_path_grouphomomorphism; intros [a b]; cbn. apply path_prod; cbn. + rewrite (grp_prod_decompose a b). refine (_ @ (grp_homo_op (ab_biprod_pr1 $o phi) _ _)^). apply grp_cancelR; symmetry. exact (ap fst (p a)). + rewrite (grp_prod_decompose a b). refine (_ @ (grp_homo_op (ab_biprod_pr2 $o phi) _ _)^); cbn; symmetry. exact (ap011 _ (ap snd (p a)) (q (group_unit, b))^). Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.