(A : pType) : { hspace_op : SgOp A & { hspace_left_identity : LeftIdentity hspace_op pt & { hspace_right_identity : RightIdentity hspace_op pt & hspace_left_identity pt = hspace_right_identity pt } } } <~> IsCohHSpace A := ltac:(make_equiv).
Require Import Basics HSpace.Core Pointed.Core Pointed.Loops.