{P : Smash X Y -> Type} (Psm : forall a b, P (sm a b)) (Pl : P auxl) (Pr : P auxr) (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl) (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) : forall x : Smash X Y, P x. Proof. srapply Pushout_ind. + intros [a b]. apply Psm. + apply (Bool_ind _ Pr Pl). + srapply sum_ind. - apply Pgl. - apply Pgr. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics Basics.Equivalences. Require Import Types.Sum Types.Bool Types.Paths Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Equiv. Require Import Colimits.Pushout. Require Import Cubical.DPath. Require Import Pointed.Core.