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