IsCohHSpace (psphere 1) := Build_IsCohHSpace _ _ _. Global Instance associative_sgop_s1 : Associative sgop_s1. Proof. intros x y z. revert x. srapply Sph1_ind. 1: reflexivity. apply sq_dp^-1. revert y. srapply Sph1_ind. { apply (sq_flip_v (px0:=1) (px1:=1)). exact (ap_nat' (fun a => ap (fun b => sgop_s1 b z) (rightidentity_s1 a)) (merid North @ (merid South)^)). } apply path_ishprop. Defined.
Require Import Classes.interfaces.canonical_names. Require Import Cubical.DPath Cubical.PathSquare. Require Import Homotopy.Suspension. Require Import Homotopy.HSpace.Core. Require Import Homotopy.HSpace.Coherent. Require Import Spaces.Spheres.