proposition: Lemma pmap_abses_const_to_pointed `{Univalence} {B' A' B A : AbGroup@{u}} : pconst ==* to_pointed (@pmap_abses_const B' A' B A).
proof: Proof. srapply Build_pHomotopy. 1: reflexivity. apply moveL_pV. refine (concat_1p _ @ _). apply equiv_path_abses_1. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse