`{Funext} {A : AbGroup} : @ab_cotriagonal A $o ab_biprod_twist = ab_cotriagonal. Proof. apply equiv_path_grouphomomorphism. intro x. cbn. refine ((grp_assoc _ _ _)^ @ _). refine (abgroup_commutative _ _ _ @ _). exact (ap (fun a => a + snd x) (abgroup_commutative _ _ _)). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.