{A B : AbGroup} (f g : GroupHomomorphism A B) := ab_cokernel (ab_homo_add (negate_hom f) g).
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.