RightInverse abel_sgop abel_negate abel_mon_unit. Proof. Abel_ind_hprop x; simpl. apply ap; apply right_inverse. 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.