{A : AbGroup} : ab_biprod_twist $o @ab_triagonal A = ab_triagonal := idpath.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.