`{Funext} {A : pType} `{IsHomogeneous A} : IsCohHSpace A. Proof. apply (equiv_iscohhspace_ptd_action A)^-1. exists homogeneous_pt_id. apply homogeneous_pt_id_beta. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise