fwedge_in' (I : Type) (X : I -> pType) : forall i, X i $-> FamilyWedge I X := fun i => Build_pMap _ _ (fun x => pushl (i; x)) (pglue i).
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.