iscohhspace_hspace' (A : pType) `{IsHSpace A} `{forall a, IsEquiv (a *.)} : IsCohHSpace A. Proof. snrapply Build_IsCohHSpace. { nrapply ishspace_homogeneous. apply ishomogeneous_hspace. } apply iscoherent_homogeneous. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise