{X Y : pType} : pswap X Y $o pswap Y X $== pmap_idmap. Proof. snrapply Build_pHomotopy. - snrapply Smash_ind_FFlr. 1-3: reflexivity. + intros y. apply equiv_p1_1q. lhs nrapply ap. 1: apply Smash_rec_beta_gluel. nrapply Smash_rec_beta_gluer. + intros x. apply equiv_p1_1q. lhs nrapply ap. 1: apply Smash_rec_beta_gluer. nrapply Smash_rec_beta_gluel. - reflexivity. 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.