`{Funext} {A : pType} `{IsHSpace A} `{forall a:A, IsEquiv (a *.)} : [(A ->* A) * A, (pmap_idmap, pt)] <~>* selfmaps A. Proof. snrapply Build_pEquiv'. 1: exact equiv_map_pmap_hspace. cbn. apply path_forall, hspace_left_identity. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise