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