fact: Definition wedge_rec_beta_wglue {X Y Z : pType} (f : X $-> Z) (g : Y $-> Z) : ap (wedge_rec f g) wglue = point_eq f @ (point_eq g)^ := Pushout_rec_beta_pglue _ f g _ tt.
imports: Basics Types Pointed.Core Pointed.pSusp Colimits.Pushout WildCat Homotopy.Suspension