{A : AbGroup} : direct_sum_swap $o (@ab_diagonal A) = ab_diagonal := idpath.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.