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