{A B X Y : pType} (f : A $-> X) (g : B $-> Y) : Smash A B $-> Smash X Y. Proof. srapply Build_pMap. - snrapply (Smash_rec (fun a b => sm (f a) (g b)) auxl auxr). + intro a; cbn beta. rhs_V nrapply (gluel (f a)). exact (ap011 _ 1 (point_eq g)). + intro b; cbn beta. rhs_V nrapply (gluer (g b)). exact (ap011 _ (point_eq f) 1). - exact (ap011 _ (point_eq f) (point_eq g)). 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.