proposition: Lemma equiv_pmap_hspace `{Funext} {A : pType} (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)} : (A ->* A) <~> (A ->* [A,a]).
proof: Proof. nrapply pequiv_pequiv_postcompose. rapply pequiv_hspace_left_op. Defined.
imports: Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise Pointed Homotopy.EvaluationFibration