fact: Definition Smash_rec {P : Type} (Psm : X -> Y -> P) (Pl Pr : P) (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) : Smash X Y -> P := Smash_ind Psm Pl Pr (fun x => dp_const (Pgl x)) (fun x => dp_const (Pgr x)).
imports: Basics Pointed.Core Types Colimits.Pushout Cubical