wedge_rec' {X Y : pType} {Z : Type} (f : X -> Z) (g : Y -> Z) (w : f pt = g pt) : Wedge X Y -> Z. Proof. snrapply Pushout_rec. - exact f. - exact g. - intro. exact w. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.