`{Funext} {A B : AbGroup} (f g : B $-> A) : ab_biprod_corec f g = (functor_ab_biprod f g) $o ab_diagonal. Proof. apply equiv_path_grouphomomorphism; reflexivity. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.