TwoSphere -> (Sphere 2). Proof. apply (TwoSphere_rec (Sphere 2) North). refine (transport (fun x => x = x) (concat_pV (merid North)) _). refine (((ap (fun u => merid u @ (merid North)^) (merid North @ (merid South)^)))). 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.