`{Funext} (A : pType) : IsCohHSpace A <~> pSect (ev A). Proof. refine (issig_psect (ev A) oE _^-1%equiv oE (issig_iscohhspace A)^-1%equiv). unfold SgOp, LeftIdentity, RightIdentity. apply equiv_functor_sigma_id; intro mu. apply (equiv_functor_sigma' (equiv_apD10 _ _ _)); intro H1; cbn. apply equiv_functor_sigma_id; intro H2; cbn. refine (equiv_path_inverse _ _ oE _). apply equiv_concat_r. apply concat_p1. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise