fact: Definition equiv_path_ishspace `{Funext} {X : pType} (mu nu : IsHSpace X) : path_ishspace_type mu nu <~> (mu = nu).
imports: Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise Pointed Homotopy.EvaluationFibration