proposition: Proposition ab_biprod_rec {A B Y : AbGroup} (f : A $-> Y) (g : B $-> Y) : (ab_biprod A B) $-> Y.
proof: 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.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse