{G : Group} : G $-> (abel G) := @Build_GroupHomomorphism G (abel G) abel_in _.
Require Import Basics Types Truncations.Core. Require Import Cubical.DPath WildCat. Require Import Colimits.Coeq. Require Import Algebra.AbGroups.AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.