forall x : Sphere 1, x = x. Proof. srapply Sph1_ind. + exact (merid North @ (merid South)^). + apply dp_paths_lr. by rewrite concat_Vp, concat_1p. 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.