proposition: Proposition ab_biprod_rec_beta `{Funext} {A B Y : AbGroup} (u : ab_biprod A B $-> Y) : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) = u.
proof: Proof. apply equiv_path_grouphomomorphism. exact (ab_biprod_rec_beta' u). Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse