{A : AbGroup} : ab_biprod (ab_biprod A A) A $-> A := ab_codiagonal $o (functor_ab_biprod ab_codiagonal grp_homo_id).
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.