(P : Sphere 1 -> Type) (b : P North) (p : DPath P (merid North @ (merid South)^) b b) : forall x : Sphere 1, P x. Proof. srapply Susp_ind. 1: exact b. 1: exact (merid South # b). srapply Susp_ind; hnf. { apply moveL_transport_p. refine ((transport_pp _ _ _ _)^ @ _). apply p. } 1: reflexivity. apply Empty_ind. 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.