(I : Type) (X : I -> pType) : pType. Proof. snrapply Build_pType. - srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _). + exact (fun i => (i; pt)). + exact (fun _ => pt). - apply pushr. exact pt. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.