(X : pType) : psusp (loops X) ->* X := Build_pMap (psusp (loops X)) X (Susp_rec (point X) (point X) idmap) 1.
Require Import Basics. Require Import Types. Require Import Pointed.Core. Require Import Pointed.Loops. Require Import Pointed.pTrunc. Require Import Pointed.pEquiv. Require Import Homotopy.Suspension. Require Import Homotopy.Freudenthal. Require Import Truncations. Require Import WildCat.