(X : pType) : psusp X $-> psusp X \/ psusp X. Proof. refine (Build_pMap _ _ (Susp_rec pt pt _) idpath). intros x. refine (ap wedge_inl _ @ wglue @ ap wedge_inr _ @ wglue^). 1,2: exact (loop_susp_unit X x). Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.