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