{A B : AbGroup} (P : ab_biprod A B -> Type) (Hinl : forall a, P (ab_biprod_inl a)) (Hinr : forall b, P (ab_biprod_inr b)) (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. intros [a b]. snrapply ((grp_prod_decompose a b)^ # _). apply Hop. - exact (Hinl a). - exact (Hinr b). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.