{X Y A B C D : pType} (f : X $-> A) (g : Y $-> B) (h : A $-> C) (k : B $-> D) : functor_smash (h $o f) (k $o g) $== functor_smash h k $o functor_smash f g. Proof. pointed_reduce. snrapply Build_pHomotopy. { snrapply Smash_ind_FlFr. 1-3: reflexivity. - intros x. apply equiv_p1_1q. lhs nrapply Smash_rec_beta_gluel. symmetry. lhs nrapply (ap_compose (functor_smash _ _) _ (gluel x)). lhs nrapply ap. 2: nrapply Smash_rec_beta_gluel. lhs nrapply Smash_rec_beta_gluel. apply concat_1p. - intros y. apply equiv_p1_1q. lhs nrapply Smash_rec_beta_gluer. symmetry. lhs nrapply (ap_compose (functor_smash _ _) _ (gluer y)). lhs nrapply ap. 2: nrapply Smash_rec_beta_gluer. lhs nrapply Smash_rec_beta_gluer. apply concat_1p. } 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.