proposition: Proposition hspace_ev_trivialization `{Funext} {A : pType} `{IsCoherent A} `{forall a:A, IsEquiv (a *.)} : ev A o* pequiv_map_pmap_hspace ==* psnd (A:=[A ->* A, pmap_idmap]).
proof: Proof. snrapply Build_pHomotopy. { intros [f x]; cbn. exact (ap _ (dpoint_eq f) @ hspace_right_identity _). } cbn. refine (concat_1p _ @ _^). refine (concat_p1 _ @ concat_p1 _ @ _). refine (ap10_path_forall _ _ _ _ @ _). apply iscoherent. Defined.
imports: Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise Pointed Homotopy.EvaluationFibration