{G H : Group} {f g : Hom (A:=Group) (abel G) H} (p : f $o abel_unit $== g $o abel_unit) : f $== g. Proof. rapply Abel_ind_hprop. rapply p. 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.