`{Funext} (A : pType) {m : IsHSpace A} `{forall a, IsEquiv (a *.)} : @hspace_op A (@ishspace_cohhspace A (iscohhspace_hspace' A)) = @hspace_op A m. Proof. cbn. funext a b. refine (ap (a *.) _). apply moveR_equiv_V. symmetry; apply left_identity. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise