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