Group -> AbGroup. Proof. intro G. snrapply Build_AbGroup. - srapply (Build_Group (Abel G)). - exact _. Defined.
Require Import Basics Types Truncations.Core. Require Import Cubical.DPath WildCat. Require Import Colimits.Coeq. Require Import Algebra.AbGroups.AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.