(Sphere 1) -> Circle. Proof. apply (Susp_rec Circle.base Circle.base). exact (fun x => if (S0_to_Bool x) then loop else 1). 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.