Smash_rec' {P : Type} {Psm : X -> Y -> P} (Pgl : forall a, Psm a pt = Psm pt pt) (Pgr : forall b, Psm pt b = Psm pt pt) (ql : Pgl pt = 1) (qr : Pgr pt = 1) : Smash X Y -> P := Smash_rec Psm (Psm pt pt) (Psm pt pt) Pgl Pgr.
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.