{A B Y : AbGroup} (f : A $-> Y) (g : B $-> Y) : (ab_biprod A B) $-> Y. Proof. snrapply Build_GroupHomomorphism. - intros [a b]; exact (f a + g b). - intros [a b] [a' b']; simpl. rewrite (grp_homo_op f). rewrite (grp_homo_op g). rewrite (associativity _ (g b) _). rewrite <- (associativity _ (f a') _). rewrite (commutativity (f a') _). rewrite (associativity _ (g b) _). exact (associativity _ (f a') _)^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.