ab_biprod@{u} (A B : AbGroup@{u}) : AbGroup@{u}. Proof. rapply (Build_AbGroup (grp_prod A B)). intros [a b] [a' b']. apply path_prod; simpl; apply commutativity. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.