(X Y : pType) : X \/ Y $-> X * Y := pprod_corec _ wedge_pr1 wedge_pr2.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.