fact: Definition iscohhspace_hspace'_beta_mu `{Funext} (A : pType) {m : IsHSpace A} `{forall a, IsEquiv (a *.)} : @hspace_op A (@ishspace_cohhspace A (iscohhspace_hspace' A)) = @hspace_op A m.
imports: Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise Pointed Homotopy.EvaluationFibration