{A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B') : ab_biprod A B $-> ab_biprod A' B' := (ab_biprod_corec (f $o ab_biprod_pr1) (g $o ab_biprod_pr2)).
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.