{A B : pType} {P : Type} (f g : Smash A B -> P) (Hsm : forall a b, f (sm a b) = g (sm a b)) (Hl : f auxl = g auxl) (Hr : f auxr = g auxr) (Hgluel : forall a, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)) (Hgluer : forall b, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)) : f == g. Proof. snrapply (Smash_ind Hsm Hl Hr). - intros a. nrapply transport_paths_FlFr'. exact (Hgluel a). - intros b. nrapply transport_paths_FlFr'. exact (Hgluer b). 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.