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