fact: Definition Smash_rec' {P : Type} {Psm : X -> Y -> P} (Pgl : forall a, Psm a pt = Psm pt pt) (Pgr : forall b, Psm pt b = Psm pt pt) (ql : Pgl pt = 1) (qr : Pgr pt = 1) : Smash X Y -> P := Smash_rec Psm (Psm pt pt) (Psm pt pt) Pgl Pgr.
imports: Basics Pointed.Core Types Colimits.Pushout Cubical