`{Funext} {A A' B B' : AbGroup} (p : A $-> B) (p' : A' $-> B') `{S : IsSurjection p} `{S' : IsSurjection p'} : IsSurjection (functor_ab_biprod p p'). Proof. intros [b b']. pose proof (a := S b); pose proof (a' := S' b'). apply center in a, a'. strip_truncations. rapply contr_inhabited_hprop. apply tr. exists (ab_biprod_inl a.1 + ab_biprod_inr a'.1); cbn. apply path_prod; refine (grp_homo_op _ _ _ @ _); rewrite (grp_homo_unit _); cbn. - exact (right_identity _ @ a.2). - exact (left_identity _ @ a'.2). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.