(A : pType) {m : IsHSpace A} `{forall a, IsEquiv (a *.)} : IsCohHSpace A. Proof. snrapply Build_IsCohHSpace. 1: snrapply Build_IsHSpace. - exact (@hspace_op A m). - exact (@hspace_left_identity A m). - intro a. lhs nrapply (ap (a *.) (hspace_right_identity pt))^. lhs nrapply (ap (a *.) (hspace_left_identity pt)). exact (hspace_right_identity a). - unfold IsCoherent; cbn. apply moveL_Vp. lhs nrapply concat_A1p. refine (_ @@ 1). apply (cancelR _ _ (hspace_left_identity pt)). symmetry; apply concat_A1p. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise