(Sphere 2) -> TwoSphere. Proof. apply (Susp_rec base base). apply (Susp_rec (idpath base) (idpath base)). apply (Susp_rec surf (idpath (idpath base))). apply Empty_rec. Defined.
Require Import Basics Types. Require Import WildCat.Equiv. Require Import NullHomotopy. Require Import Homotopy.Suspension. Require Import Pointed. Require Import Truncations. Require Import Spaces.Circle Spaces.TwoSphere.