(X Y : pType) : functor_smash (@pmap_idmap X) (@pmap_idmap Y) $== pmap_idmap. Proof. snrapply Build_pHomotopy. { snrapply Smash_ind_FlFr. 1-3: reflexivity. - intros x. apply equiv_p1_1q. rhs nrapply ap_idmap. lhs nrapply Smash_rec_beta_gluel. apply concat_1p. - intros y. apply equiv_p1_1q. rhs nrapply ap_idmap. 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.