{A B X Y : pType} (f : A $-> X) (g : B $-> Y) : pswap X Y $o functor_smash f g $== functor_smash g f $o pswap A B. Proof. pointed_reduce. snrapply Build_pHomotopy. - snrapply Smash_ind_FlFr. 1-3: reflexivity. + intros a. apply equiv_p1_1q. rhs nrapply (ap_compose (pswap _ _) _ (gluel a)). rhs nrapply ap. 2: apply Smash_rec_beta_gluel. rhs nrapply Smash_rec_beta_gluer. lhs nrapply (ap_compose (functor_smash _ _) (pswap _ _) (gluel a)). lhs nrapply ap. 1: apply Smash_rec_beta_gluel. simpl. lhs nrapply ap. 1: apply concat_1p. rhs nrapply concat_1p. nrapply Smash_rec_beta_gluel. + intros b. apply equiv_p1_1q. rhs nrapply (ap_compose (pswap _ _) (functor_smash _ _) (gluer b)). rhs nrapply ap. 2: apply Smash_rec_beta_gluer. rhs nrapply Smash_rec_beta_gluel. lhs nrapply (ap_compose (functor_smash _ _) (pswap _ _) (gluer b)). lhs nrapply ap. 1: apply Smash_rec_beta_gluer. lhs nrapply ap. 1: apply concat_1p. rhs nrapply concat_1p. nrapply Smash_rec_beta_gluer. - 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.