`{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. apply equiv_path_grouphomomorphism. intro a; cbn. exact (grp_assoc _ _ _)^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.