`{Funext} {A : pType} `{IsCoherent A} `{forall a:A, IsEquiv (hspace_op a)} : IsCohHSpace A <~> (A ->* (A ->** A)). Proof. refine (_ oE equiv_iscohhspace_psect A). refine (_ oE (equiv_pequiv_pslice_psect _ _ _ hspace_ev_trivialization^*)^-1%equiv). refine (_ oE equiv_psect_psnd (A:=[A ->* A, pmap_idmap])). refine (pequiv_pequiv_postcompose _); symmetry. rapply pequiv_hspace_left_op. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise