{A B C : AbGroup} : ab_biprod A (ab_biprod B C) $<~> ab_biprod (ab_biprod A B) C. Proof. snrapply Build_GroupIsomorphism'. - apply equiv_prod_assoc. - unfold IsSemiGroupPreserving; reflexivity. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.