{X Y : pType} : Smash X Y $<~> Smash Y X. Proof. snrapply cate_adjointify. 1,2: exact (pswap _ _). 1,2: exact pswap_pswap. 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.