{X Y : pType} : pushl (point X) = (pushr (point Y)) :> (X \/ Y) := pglue tt.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.