(P : Type) (b : P) (p : b = b) : Sphere 1 -> P. Proof. srapply Susp_rec. 1,2: exact b. simpl. srapply Susp_rec. 1: exact p. 1: reflexivity. apply Empty_rec. 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.