{X : pType} `{IsHSpace X} (x : X) `{IsEquiv _ _ (x *.)} : X <~>* [X,x] := Build_pEquiv' (B:=[X,x]) (equiv_hspace_left_op x) (right_identity x). Global Instance isequiv_hspace_left_op `{Univalence} {A : pType} `{IsHSpace A} `{IsConnected 0 A} : forall (a : A), IsEquiv (a *.). Proof. nrapply conn_point_elim; exact _. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.