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