(I : Type) (X : I -> pType) (Z : pType) (f : forall i, X i $-> Z) : FamilyWedge I X $-> Z. Proof. snrapply Build_pMap. - snrapply Pushout_rec. + apply (sig_rec f). + exact pconst. + intros i. exact (point_eq (f i)). - exact idpath. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.