(X Y : pType) : pType := [Pushout (fun _ : Unit => point X) (fun _ => point Y), pushl (point X)].
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.