{A A' B B' : AbGroup} (f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g} : IsEquiv (functor_ab_biprod f g). Proof. srapply isequiv_adjointify. 1: { rapply functor_ab_biprod; apply grp_iso_inverse. + exact (Build_GroupIsomorphism _ _ f _). + exact (Build_GroupIsomorphism _ _ g _). } all: intros [a b]; simpl. all: apply path_prod'. 1,2: apply eisretr. all: apply eissect. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.