{A B : AbGroup} (f : A $-> B) : f $o ab_codiagonal $== ab_codiagonal $o functor_ab_biprod f f := fun a => grp_homo_op f _ _.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.