(X Y : pType) : Smash X Y $-> Smash Y X := Build_pMap _ _ (Smash_rec (flip sm) auxr auxl gluer gluel) 1.
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.