{X Y A B : pType} {f h : X $-> A} {g k : Y $-> B} (p : f $== h) (q : g $== k) : functor_smash f g $== functor_smash h k. Proof. pointed_reduce. snrapply Build_pHomotopy. { snrapply Smash_ind_FlFr. 1: exact (fun x y => ap011 _ (p x) (q y)). 1,2: reflexivity. - intros x. lhs nrapply concat_p1. lhs nrapply Smash_rec_beta_gluel. rhs nrapply whiskerL. 2: nrapply Smash_rec_beta_gluel. simpl; induction (p x); simpl. rhs_V nrapply concat_pp_p. apply whiskerR. nrapply ap_pp. - intros y. lhs nrapply concat_p1. lhs nrapply Smash_rec_beta_gluer. rhs nrapply whiskerL. 2: nrapply Smash_rec_beta_gluer. simpl; induction (q y); simpl. rhs_V nrapply concat_pp_p. apply whiskerR. nrapply (ap011_pp _ _ _ 1 1). } exact (ap022 _ (concat_p1 (p pt))^ (concat_p1 (q pt))^ @ (concat_p1 _)^). 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.