fact: Definition equiv_hspace_left_op {X : pType} `{IsHSpace X} (x : X) `{IsEquiv _ _ (x *.)} : X <~> X := Build_Equiv _ _ (x *.) _.
imports: Classes.interfaces.canonical_names (SgOp, sg_op, MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity) Basics Types Pointed WildCat.Core Truncations.Core Truncations.Connectedness