`{Funext} {A : pType} `{IsHSpace A} `{forall a:A, IsEquiv (a *.)} : (A ->* A) * A <~> (A -> A). Proof. transitivity {a : A & {f : A -> A & f pt = a}}. 2: exact (equiv_sigma_contr _ oE (equiv_sigma_symm _)^-1%equiv). refine (_ oE (equiv_sigma_prod0 _ _)^-1%equiv oE equiv_prod_symm _ _). apply equiv_functor_sigma_id; intro a. exact ((issig_pmap A [A,a])^-1%equiv oE equiv_pmap_hspace a). Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise