proposition: Corollary ab_biprod_rec_uncurried {A B Y : AbGroup} : (A $-> Y) * (B $-> Y) -> (ab_biprod A B) $-> Y.
proof: Proof. intros [f g]. exact (ab_biprod_rec f g). Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse