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