`{Funext} {A : pType} (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)} : (A ->* A) <~> (A ->* [A,a]). Proof. nrapply pequiv_pequiv_postcompose. rapply pequiv_hspace_left_op. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise