proposition: Lemma ab_commute_id_codiagonal `{Funext} {A : AbGroup} : (@ab_codiagonal A) $o (functor_ab_biprod ab_codiagonal grp_homo_id) $o ab_biprod_assoc = ab_codiagonal $o (functor_ab_biprod grp_homo_id ab_codiagonal).
proof: Proof. apply equiv_path_grouphomomorphism. intro a; cbn. exact (grp_assoc _ _ _)^. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse