Sphere 2 <~> TwoSphere := Build_Equiv _ _ _ isequiv_S2_to_TwoSphere. Global Instance istrunc_s0 : IsHSet (Sphere 0). Proof. srapply (istrunc_isequiv_istrunc _ S0_to_Bool^-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.