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