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