{X Y : pType} {Z : pType} (f : X $-> Z) (g : Y $-> Z) : X \/ Y $-> Z. Proof. snrapply Build_pMap. - snrapply (' f g). exact (point_eq f @ (point_eq g)^). - exact (point_eq f). Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.