{A : AbGroup} : A $-> ab_biprod A A := ab_biprod_corec grp_homo_id grp_homo_id.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.