fact: Definition ab_triagonal {A : AbGroup} : A $-> ab_biprod (ab_biprod A A) A := (functor_ab_biprod ab_diagonal grp_homo_id) $o ab_diagonal.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse