proposition: Theorem equiv_cohhspace_ppmap `{Funext} {A : pType} `{IsCoherent A} `{forall a:A, IsEquiv (hspace_op a)} : IsCohHSpace A <~> (A ->* (A ->** A)).
proof: 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.
imports: Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise Pointed Homotopy.EvaluationFibration