{X Y} : Y $-> X \/ Y. Proof. snrapply Build_pMap. - exact (fun x => pushr x). - symmetry. by rapply pglue. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.