proposition: Theorem isequiv_ab_biprod_rec `{Funext} {A B Y : AbGroup} : IsEquiv (@ab_biprod_rec_uncurried A B Y).
proof: Proof. srapply isequiv_adjointify. - intro phi. exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr). - intro phi. exact (ab_biprod_rec_beta phi). - intros [a b]. apply path_prod. + apply ab_biprod_rec_inl_beta. + apply ab_biprod_rec_inr_beta. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse