{X : pType} : { mu : X -> X -> X & prod (forall x, mu pt x = x) (forall x, mu x pt = x) } <~> IsHSpace X := ltac:(make_equiv). Global Instance isequiv_hspace_left_op_pt {X : pType} `{IsHSpace X} : IsEquiv (pt *.). Proof. apply (isequiv_homotopic idmap); intro x. exact (left_identity x)^. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.