Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics Basics.Equivalences.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.

Local Open Scope pointed_scope.
Local Open Scope dpath_scope.
Local Open Scope path_scope.

(* Definition of smash product *)

Definition sum_to_prod (X Y : pType) : X + Y -> X * Y
  := sum_ind _ (fun x => (x, point Y)) (fun y => (point X, y)).

Definition sum_to_bool X Y : X + Y -> Bool
  := sum_ind _ (fun _ => false) (fun _ => true).

Definition Smash@{u v w | u <= w, v <= w} (X : pType@{u}) (Y : pType@{v}) : pType@{w}
  := [Pushout@{w w w w} (sum_to_prod@{w w w} X Y) (sum_to_bool@{u v w} X Y), pushl (point X, point Y)].

Section Smash.

  Context {X Y : pType}.

  Definition sm (x : X) (y : Y) : Smash X Y := pushl (x, y).

  Definition auxl : Smash X Y := pushr false.

  Definition auxr : Smash X Y := pushr true.

  Definition gluel (x : X) : sm x pt = auxl
    := pglue (f:=sum_to_prod X Y) (g:=sum_to_bool X Y) (inl x).

  Definition gluer (y : Y) : sm pt y = auxr
    := pglue (f:=sum_to_prod X Y) (g:=sum_to_bool X Y) (inr y).

  Definition gluel' (x x' : X) : sm x pt = sm x' pt
    := gluel x @ (gluel x')^.

  Definition gluer' (y y' : Y) : sm pt y = sm pt y'
    := gluer y @ (gluer y')^.

  Definition glue (x : X) (y : Y) : sm x pt = sm pt y
    := gluel' x pt @ gluer' pt y.

  Definition glue_pt_left (y : Y) : glue pt y = gluer' pt y.
X, Y: pType
y: Y
glue pt y = gluer' pt y
  Proof.
X, Y: pType
y: Y
glue pt y = gluer' pt y
    refine (_ @ concat_1p _).
X, Y: pType
y: Y
glue pt y = 1 @ gluer' pt y
    apply whiskerR, concat_pV.
  Defined.

  Definition glue_pt_right (x : X) : glue x pt = gluel' x pt.
X, Y: pType
x: X
glue x pt = gluel' x pt
  Proof.
X, Y: pType
x: X
glue x pt = gluel' x pt
    refine (_ @ concat_p1 _).
X, Y: pType
x: X
glue x pt = gluel' x pt @ 1
    apply whiskerL, concat_pV.
  Defined.

  Definition ap_sm_left {x x' : X} (p : x = x')
    : ap (fun t => sm t pt) p = gluel' x x'.
X, Y: pType
x, x': X
p: x = x'
ap (fun t : X => sm t pt) p = gluel' x x'
  Proof.
X, Y: pType
x, x': X
p: x = x'
ap (fun t : X => sm t pt) p = gluel' x x'
    destruct p.
X, Y: pType
x: X
ap (fun t : X => sm t pt) 1 = gluel' x x
    symmetry.
X, Y: pType
x: X
gluel' x x = ap (fun t : X => sm t pt) 1
    apply concat_pV.
  Defined.

  Definition ap_sm_right {y y' : Y} (p : y = y')
    : ap (sm pt) p = gluer' y y'.
X, Y: pType
y, y': Y
p: y = y'
ap (sm pt) p = gluer' y y'
  Proof.
X, Y: pType
y, y': Y
p: y = y'
ap (sm pt) p = gluer' y y'
    destruct p.
X, Y: pType
y: Y
ap (sm pt) 1 = gluer' y y
    symmetry.
X, Y: pType
y: Y
gluer' y y = ap (sm pt) 1
    apply concat_pV.
  Defined.

  Definition Smash_ind {P : Smash X Y -> Type}
    (Psm : forall a b, P (sm a b)) (Pl : P auxl) (Pr : P auxr)
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr)
    : forall x : Smash X Y, P x.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall x : Smash X Y, P x
  Proof.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall x : Smash X Y, P x
    srapply Pushout_ind.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall b : X * Y, P (pushl b)
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall c : Bool, P (pushr c)
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall a : X + Y,
transport P (pglue a) (?pushb (sum_to_prod X Y a)) =
?pushc (sum_to_bool X Y a)
    +
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall b : X * Y, P (pushl b) intros [a b].
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
P (pushl (a, b))
      apply Psm.
    +
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall c : Bool, P (pushr c) exact (Bool_ind _ Pr Pl).
    +
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall a : X + Y,
transport P (pglue a)
  ((fun b0 : X * Y => (fun (a0 : X) (b : Y) => Psm a0 b) (fst b0) (snd b0))
     (sum_to_prod X Y a)) =
Bool_ind (fun b : Bool => P (pushr b)) Pr Pl (sum_to_bool X Y a) srapply sum_ind.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall a : X,
(fun s : X + Y =>
 transport P (pglue s)
   ((fun b0 : X * Y => (fun (a0 : X) (b : Y) => Psm a0 b) (fst b0) (snd b0))
      (sum_to_prod X Y s)) =
 Bool_ind (fun b : Bool => P (pushr b)) Pr Pl (sum_to_bool X Y s)) 
  (inl a)
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall b : Y,
(fun s : X + Y =>
 transport P (pglue s)
   ((fun b0 : X * Y => (fun (a : X) (b1 : Y) => Psm a b1) (fst b0) (snd b0))
      (sum_to_prod X Y s)) =
 Bool_ind (fun b0 : Bool => P (pushr b0)) Pr Pl (sum_to_bool X Y s)) 
  (inr b)
      -
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall a : X,
(fun s : X + Y =>
 transport P (pglue s)
   ((fun b0 : X * Y => (fun (a0 : X) (b : Y) => Psm a0 b) (fst b0) (snd b0))
      (sum_to_prod X Y s)) =
 Bool_ind (fun b : Bool => P (pushr b)) Pr Pl (sum_to_bool X Y s)) 
  (inl a) exact Pgl.
      -
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a : X) (b : Y), P (sm a b)
Pl: P auxl
Pr: P auxr
Pgl: forall a : X, DPath P (gluel a) (Psm a pt) Pl
Pgr: forall b : Y, DPath P (gluer b) (Psm pt b) Pr
forall b : Y,
(fun s : X + Y =>
 transport P (pglue s)
   ((fun b0 : X * Y => (fun (a : X) (b1 : Y) => Psm a b1) (fst b0) (snd b0))
      (sum_to_prod X Y s)) =
 Bool_ind (fun b0 : Bool => P (pushr b0)) Pr Pl (sum_to_bool X Y s)) 
  (inr b) exact Pgr.
  Defined.

  Definition Smash_ind_beta_gluel {P : Smash X Y -> Type}
    {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr}
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a : X)
    : apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a
    := Pushout_ind_beta_pglue P _ _ _ (inl a).

  Definition Smash_ind_beta_gluer {P : Smash X Y -> Type}
    {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr}
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (b : Y)
    : apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b
    := Pushout_ind_beta_pglue P _ _ _ (inr b).

  Definition Smash_ind_beta_gluel' {P : Smash X Y -> Type}
    {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr}
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a b : X)
    : apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a b)
    = (Pgl a) @Dp ((Pgl b)^D).
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @Dp (Pgl b) ^D
  Proof.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @Dp (Pgl b) ^D
    lhs napply dp_apD_pp.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel a) @Dp
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel b)^ = Pgl a @Dp (Pgl b) ^D
    apply ap011.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel b)^ = (Pgl b) ^D
    1: apply Smash_ind_beta_gluel.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel b)^ = (Pgl b) ^D
    lhs napply dp_apD_V.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
(apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel b)) ^D = (Pgl b) ^D
    apply ap.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: X
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel b) = Pgl b
    apply Smash_ind_beta_gluel.
  Defined.

  Definition Smash_ind_beta_gluer' {P : Smash X Y -> Type}
    {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr}
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a b : Y)
    : apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' a b)
    = (Pgr a) @Dp ((Pgr b)^D).
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @Dp (Pgr b) ^D
  Proof.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @Dp (Pgr b) ^D
    lhs napply dp_apD_pp.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer a) @Dp
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b)^ = Pgr a @Dp (Pgr b) ^D
    apply ap011.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer a) = Pgr a
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b)^ = (Pgr b) ^D
    1: apply Smash_ind_beta_gluer.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b)^ = (Pgr b) ^D
    lhs napply dp_apD_V.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
(apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b)) ^D = (Pgr b) ^D
    apply ap.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a, b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b
    apply Smash_ind_beta_gluer.
  Defined.

  Definition Smash_ind_beta_glue {P : Smash X Y -> Type}
    {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr}
    (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl)
    (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a : X) (b : Y)
    : apD (Smash_ind Psm Pl Pr Pgl Pgr) (glue a b)
    = ((Pgl a) @Dp ((Pgl pt)^D)) @Dp ((Pgr pt) @Dp ((Pgr b)^D)).
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (glue a b) =
(Pgl a @Dp (Pgl pt) ^D) @Dp (Pgr pt @Dp (Pgr b) ^D)
  Proof.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (glue a b) =
(Pgl a @Dp (Pgl pt) ^D) @Dp (Pgr pt @Dp (Pgr b) ^D)
    lhs napply dp_apD_pp.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a pt) @Dp
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' pt b) =
(Pgl a @Dp (Pgl pt) ^D) @Dp (Pgr pt @Dp (Pgr b) ^D)
    apply ap011.
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a pt) = Pgl a @Dp (Pgl pt) ^D
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' pt b) = Pgr pt @Dp (Pgr b) ^D
    -
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluel' a pt) = Pgl a @Dp (Pgl pt) ^D apply Smash_ind_beta_gluel'.
    -
X, Y: pType
P: Smash X Y -> Type
Psm: forall (a0 : X) (b0 : Y), P (sm a0 b0)
Pl: P auxl
Pr: P auxr
Pgl: forall a0 : X, DPath P (gluel a0) (Psm a0 pt) Pl
Pgr: forall b0 : Y, DPath P (gluer b0) (Psm pt b0) Pr
a: X
b: Y
apD (Smash_ind Psm Pl Pr Pgl Pgr) (gluer' pt b) = Pgr pt @Dp (Pgr b) ^D apply Smash_ind_beta_gluer'.
  Defined.

  Definition Smash_rec {P : Type} (Psm : X -> Y -> P) (Pl Pr : P)
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr)
    : Smash X Y -> P
    := Smash_ind Psm Pl Pr (fun x => dp_const (Pgl x)) (fun x => dp_const (Pgr x)).

  (* Version of smash_rec that forces (Pgl pt) and (Pgr pt) to be idpath *)
  Definition 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.

  Definition Smash_rec_beta_gluel {P : Type} {Psm : X -> Y -> P} {Pl Pr : P}
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a : X)
    : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b : Y, Psm pt b = Pr
a: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a
  Proof.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b : Y, Psm pt b = Pr
a: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a
    rhs_V napply (eissect dp_const).
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b : Y, Psm pt b = Pr
a: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = dp_const^-1 (dp_const (Pgl a))
    apply moveL_equiv_V.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b : Y, Psm pt b = Pr
a: X
dp_const (ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a)) = dp_const (Pgl a)
    lhs_V napply dp_apD_const.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b : Y, Psm pt b = Pr
a: X
apD (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = dp_const (Pgl a)
    napply Smash_ind_beta_gluel.
  Defined.

  Definition Smash_rec_beta_gluer {P : Type} {Psm : X -> Y -> P} {Pl Pr : P}
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (b : Y)
    : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b
  Proof.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b
    rhs_V napply (eissect dp_const).
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = dp_const^-1 (dp_const (Pgr b))
    apply moveL_equiv_V.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
b: Y
dp_const (ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b)) = dp_const (Pgr b)
    lhs_V napply dp_apD_const.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
b: Y
apD (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = dp_const (Pgr b)
    napply Smash_ind_beta_gluer.
  Defined.

  Definition Smash_rec_beta_gluel' {P : Type} {Psm : X -> Y -> P} {Pl Pr : P}
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : X)
    : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^
  Proof.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^
    lhs napply ap_pV.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) @
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel b))^ = Pgl a @ (Pgl b)^
    f_ap.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel a) = Pgl a
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel b))^ = (Pgl b)^
    1: apply Smash_rec_beta_gluel.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel b))^ = (Pgl b)^
    apply inverse2.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: X
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel b) = Pgl b
    apply Smash_rec_beta_gluel.
  Defined.

  Definition Smash_rec_beta_gluer' {P : Type} {Psm : X -> Y -> P} {Pl Pr : P}
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : Y)
    : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @ (Pgr b)^.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @ (Pgr b)^
  Proof.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @ (Pgr b)^
    lhs napply ap_pV.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer a) @
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b))^ = Pgr a @ (Pgr b)^
    f_ap.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer a) = Pgr a
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b))^ = (Pgr b)^
    1: apply Smash_rec_beta_gluer.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
(ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b))^ = (Pgr b)^
    apply inverse2.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a, b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b
    apply Smash_rec_beta_gluer.
  Defined.

  Definition Smash_rec_beta_glue {P : Type} {Psm : X -> Y -> P} {Pl Pr : P}
    (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a : X)
    (b : Y) : ap (Smash_rec Psm Pl Pr Pgl Pgr) (glue a b)
    = ((Pgl a) @ (Pgl pt)^) @ (Pgr pt @ (Pgr b)^).
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (glue a b) =
(Pgl a @ (Pgl pt)^) @ (Pgr pt @ (Pgr b)^)
  Proof.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (glue a b) =
(Pgl a @ (Pgl pt)^) @ (Pgr pt @ (Pgr b)^)
    lhs napply ap_pp.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a pt) @
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' pt b) =
(Pgl a @ (Pgl pt)^) @ (Pgr pt @ (Pgr b)^)
    f_ap.
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a pt) = Pgl a @ (Pgl pt)^
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' pt b) = Pgr pt @ (Pgr b)^
    -
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a pt) = Pgl a @ (Pgl pt)^ apply Smash_rec_beta_gluel'.
    -
X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a0 : X, Psm a0 pt = Pl
Pgr: forall b0 : Y, Psm pt b0 = Pr
a: X
b: Y
ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' pt b) = Pgr pt @ (Pgr b)^ apply Smash_rec_beta_gluer'.
  Defined.

End Smash.

Arguments sm : simpl never.
Arguments auxl : simpl never.
Arguments gluel : simpl never.
Arguments gluer : simpl never.

(** ** Miscellaneous lemmas about Smash *)

(** A version of [Smash_ind] specifically for proving that two functions from a [Smash] are homotopic. *)
Definition Smash_ind_FlFr {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.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
f == g
Proof.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
f == g
  snapply (Smash_ind Hsm Hl Hr).
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
forall a : A, DPath (fun x : Smash A B => f x = g x) (gluel a) (Hsm a pt) Hl
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
forall b : B, DPath (fun x : Smash A B => f x = g x) (gluer b) (Hsm pt b) Hr
  -
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
forall a : A, DPath (fun x : Smash A B => f x = g x) (gluel a) (Hsm a pt) Hl intros a.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a0 : A) (b : B), f (sm a0 b) = g (sm a0 b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a0 : A, ap f (gluel a0) @ Hl = Hsm a0 pt @ ap g (gluel a0)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
a: A
DPath (fun x : Smash A B => f x = g x) (gluel a) (Hsm a pt) Hl
    transport_paths FlFr.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a0 : A) (b : B), f (sm a0 b) = g (sm a0 b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a0 : A, ap f (gluel a0) @ Hl = Hsm a0 pt @ ap g (gluel a0)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
a: A
ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
    exact (Hgluel a).
  -
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b : B), f (sm a b) = g (sm a b)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b : B, ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
forall b : B, DPath (fun x : Smash A B => f x = g x) (gluer b) (Hsm pt b) Hr intros b.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b0 : B), f (sm a b0) = g (sm a b0)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b0 : B, ap f (gluer b0) @ Hr = Hsm pt b0 @ ap g (gluer b0)
b: B
DPath (fun x : Smash A B => f x = g x) (gluer b) (Hsm pt b) Hr
    transport_paths FlFr.
A, B: pType
P: Type
f, g: Smash A B -> P
Hsm: forall (a : A) (b0 : B), f (sm a b0) = g (sm a b0)
Hl: f auxl = g auxl
Hr: f auxr = g auxr
Hgluel: forall a : A, ap f (gluel a) @ Hl = Hsm a pt @ ap g (gluel a)
Hgluer: forall b0 : B, ap f (gluer b0) @ Hr = Hsm pt b0 @ ap g (gluer b0)
b: B
ap f (gluer b) @ Hr = Hsm pt b @ ap g (gluer b)
    exact (Hgluer b).
Defined.

(** A version of [Smash_ind]j specifically for proving that the composition of two functions is the identity map. *)
Definition Smash_ind_FFlr {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.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
g o f == idmap
Proof.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
g o f == idmap
  snapply (Smash_ind Hsm Hl Hr).
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
forall a : A,
DPath (fun x : Smash A B => (g o f) x = idmap x) (gluel a) (Hsm a pt) Hl
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
forall b : B,
DPath (fun x : Smash A B => (g o f) x = idmap x) (gluer b) (Hsm pt b) Hr
  -
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
forall a : A,
DPath (fun x : Smash A B => (g o f) x = idmap x) (gluel a) (Hsm a pt) Hl intros a; cbn beta.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a0 : A) (b : B), g (f (sm a0 b)) = sm a0 b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a0 : A, ap g (ap f (gluel a0)) @ Hl = Hsm a0 pt @ gluel a0
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
a: A
DPath (fun x : Smash A B => g (f x) = x) (gluel a) (Hsm a pt) Hl
    transport_paths FFlr.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a0 : A) (b : B), g (f (sm a0 b)) = sm a0 b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a0 : A, ap g (ap f (gluel a0)) @ Hl = Hsm a0 pt @ gluel a0
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
a: A
ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
    exact (Hgluel a).
  -
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b : B), g (f (sm a b)) = sm a b
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b : B, ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
forall b : B,
DPath (fun x : Smash A B => (g o f) x = idmap x) (gluer b) (Hsm pt b) Hr intros b; cbn beta.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b0 : B), g (f (sm a b0)) = sm a b0
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b0 : B, ap g (ap f (gluer b0)) @ Hr = Hsm pt b0 @ gluer b0
b: B
DPath (fun x : Smash A B => g (f x) = x) (gluer b) (Hsm pt b) Hr
    transport_paths FFlr.
A, B: pType
P: Type
f: Smash A B -> P
g: P -> Smash A B
Hsm: forall (a : A) (b0 : B), g (f (sm a b0)) = sm a b0
Hl: g (f auxl) = auxl
Hr: g (f auxr) = auxr
Hgluel: forall a : A, ap g (ap f (gluel a)) @ Hl = Hsm a pt @ gluel a
Hgluer: forall b0 : B, ap g (ap f (gluer b0)) @ Hr = Hsm pt b0 @ gluer b0
b: B
ap g (ap f (gluer b)) @ Hr = Hsm pt b @ gluer b
    exact (Hgluer b).
Defined.

(** ** Functoriality of the smash product *)

Definition functor_smash {A B X Y : pType} (f : A $-> X) (g : B $-> Y)
  : Smash A B $-> Smash X Y.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
Smash A B $-> Smash X Y
Proof.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
Smash A B $-> Smash X Y
  srapply Build_pMap.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
Smash A B -> Smash X Y
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
?f pt = pt
  -
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
Smash A B -> Smash X Y snapply (Smash_rec (fun a b => sm (f a) (g b)) auxl auxr).
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
forall a : A, (fun (a0 : A) (b : B) => sm (f a0) (g b)) a pt = auxl
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
forall b : B, (fun (a : A) (b0 : B) => sm (f a) (g b0)) pt b = auxr
    +
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
forall a : A, (fun (a0 : A) (b : B) => sm (f a0) (g b)) a pt = auxl intro a; cbn beta.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
a: A
sm (f a) (g pt) = auxl
      rhs_V napply (gluel (f a)).
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
a: A
sm (f a) (g pt) = sm (f a) pt
      exact (ap011 _ 1 (point_eq g)).
    +
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
forall b : B, (fun (a : A) (b0 : B) => sm (f a) (g b0)) pt b = auxr intro b; cbn beta.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
b: B
sm (f pt) (g b) = auxr
      rhs_V napply (gluer (g b)).
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
b: B
sm (f pt) (g b) = sm pt (g b)
      exact (ap011 _ (point_eq f) 1).
  -
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
Smash_rec (fun (a : A) (b : B) => sm (f a) (g b)) auxl auxr
  (fun a : A =>
   ap011 sm 1 (point_eq g) @ gluel (f a)
   :
   (fun (a0 : A) (b : B) => sm (f a0) (g b)) a pt = auxl)
  (fun b : B =>
   ap011 sm (point_eq f) 1 @ gluer (g b)
   :
   (fun (a : A) (b0 : B) => sm (f a) (g b0)) pt b = auxr)
  pt =
pt exact (ap011 _ (point_eq f) (point_eq g)).
Defined.

Definition functor_smash_idmap (X Y : pType)
  : functor_smash (@pmap_idmap X) (@pmap_idmap Y) $== pmap_idmap.
X, Y: pType
functor_smash pmap_idmap pmap_idmap $== pmap_idmap
Proof.
X, Y: pType
functor_smash pmap_idmap pmap_idmap $== pmap_idmap
  snapply Build_pHomotopy.
X, Y: pType
functor_smash pmap_idmap pmap_idmap == pmap_idmap
X, Y: pType
?p pt =
dpoint_eq (functor_smash pmap_idmap pmap_idmap) @ (dpoint_eq pmap_idmap)^
  {
X, Y: pType
functor_smash pmap_idmap pmap_idmap == pmap_idmap snapply Smash_ind_FlFr.
X, Y: pType
forall (a : X) (b : Y),
functor_smash pmap_idmap pmap_idmap (sm a b) = pmap_idmap (sm a b)
X, Y: pType
functor_smash pmap_idmap pmap_idmap auxl = pmap_idmap auxl
X, Y: pType
functor_smash pmap_idmap pmap_idmap auxr = pmap_idmap auxr
X, Y: pType
forall a : X,
ap (functor_smash pmap_idmap pmap_idmap) (gluel a) @ ?Hl =
?Hsm a pt @ ap pmap_idmap (gluel a)
X, Y: pType
forall b : Y,
ap (functor_smash pmap_idmap pmap_idmap) (gluer b) @ ?Hr =
?Hsm pt b @ ap pmap_idmap (gluer b)
    1-3: reflexivity.
X, Y: pType
forall a : X,
ap (functor_smash pmap_idmap pmap_idmap) (gluel a) @ 1 =
(fun (a0 : X) (b : Y) => 1) a pt @ ap pmap_idmap (gluel a)
X, Y: pType
forall b : Y,
ap (functor_smash pmap_idmap pmap_idmap) (gluer b) @ 1 =
(fun (a : X) (b0 : Y) => 1) pt b @ ap pmap_idmap (gluer b)
    -
X, Y: pType
forall a : X,
ap (functor_smash pmap_idmap pmap_idmap) (gluel a) @ 1 =
(fun (a0 : X) (b : Y) => 1) a pt @ ap pmap_idmap (gluel a) intros x.
X, Y: pType
x: X
ap (functor_smash pmap_idmap pmap_idmap) (gluel x) @ 1 =
(fun (a : X) (b : Y) => 1) x pt @ ap pmap_idmap (gluel x)
      apply equiv_p1_1q.
X, Y: pType
x: X
ap (functor_smash pmap_idmap pmap_idmap) (gluel x) = ap pmap_idmap (gluel x)
      rhs napply ap_idmap.
X, Y: pType
x: X
ap (functor_smash pmap_idmap pmap_idmap) (gluel x) = gluel x
      lhs napply Smash_rec_beta_gluel.
X, Y: pType
x: X
ap011 sm 1 (point_eq pmap_idmap) @ gluel (pmap_idmap x) = gluel x
      apply concat_1p.
    -
X, Y: pType
forall b : Y,
ap (functor_smash pmap_idmap pmap_idmap) (gluer b) @ 1 =
(fun (a : X) (b0 : Y) => 1) pt b @ ap pmap_idmap (gluer b) intros y.
X, Y: pType
y: Y
ap (functor_smash pmap_idmap pmap_idmap) (gluer y) @ 1 =
(fun (a : X) (b : Y) => 1) pt y @ ap pmap_idmap (gluer y)
      apply equiv_p1_1q.
X, Y: pType
y: Y
ap (functor_smash pmap_idmap pmap_idmap) (gluer y) = ap pmap_idmap (gluer y)
      rhs napply ap_idmap.
X, Y: pType
y: Y
ap (functor_smash pmap_idmap pmap_idmap) (gluer y) = gluer y
      lhs napply Smash_rec_beta_gluer.
X, Y: pType
y: Y
ap011 sm (point_eq pmap_idmap) 1 @ gluer (pmap_idmap y) = gluer y
      apply concat_1p. }
X, Y: pType
Smash_ind_FlFr (functor_smash pmap_idmap pmap_idmap) pmap_idmap
  (fun (a : X) (b : Y) => 1) 1 1
  (fun x : X =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     ((Smash_rec_beta_gluel
         (fun a : X =>
          ap011 sm 1 (point_eq pmap_idmap) @ gluel (pmap_idmap a)
          :
          (fun (a0 : X) (b : Y) => sm (pmap_idmap a0) (pmap_idmap b)) a pt =
          auxl)
         (fun b : Y =>
          ap011 sm (point_eq pmap_idmap) 1 @ gluer (pmap_idmap b)
          :
          (fun (a : X) (b0 : Y) => sm (pmap_idmap a) (pmap_idmap b0)) pt b =
          auxr)
         x @
       concat_1p (gluel x)) @
      (ap_idmap (gluel x))^))
  (fun y : Y =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     ((Smash_rec_beta_gluer
         (fun a : X =>
          ap011 sm 1 (point_eq pmap_idmap) @ gluel (pmap_idmap a)
          :
          (fun (a0 : X) (b : Y) => sm (pmap_idmap a0) (pmap_idmap b)) a pt =
          auxl)
         (fun b : Y =>
          ap011 sm (point_eq pmap_idmap) 1 @ gluer (pmap_idmap b)
          :
          (fun (a : X) (b0 : Y) => sm (pmap_idmap a) (pmap_idmap b0)) pt b =
          auxr)
         y @
       concat_1p (gluer y)) @
      (ap_idmap (gluer y))^))
  pt =
dpoint_eq (functor_smash pmap_idmap pmap_idmap) @ (dpoint_eq pmap_idmap)^
  reflexivity.
Defined.

Definition functor_smash_compose {X Y A B C D : pType}
  (f : X $-> A) (g : Y $-> B) (h : A $-> C) (k : B $-> D)
  : functor_smash (h $o f) (k $o g) $== functor_smash h k $o functor_smash f g.
X, Y, A, B, C, D: pType
f: X $-> A
g: Y $-> B
h: A $-> C
k: B $-> D
functor_smash (h $o f) (k $o g) $== functor_smash h k $o functor_smash f g
Proof.
X, Y, A, B, C, D: pType
f: X $-> A
g: Y $-> B
h: A $-> C
k: B $-> D
functor_smash (h $o f) (k $o g) $== functor_smash h k $o functor_smash f g
  pointed_reduce.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |}) ==*
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |}
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |}
  snapply Build_pHomotopy.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |}) ==
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |}
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |}
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
?p pt =
dpoint_eq
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
(dpoint_eq
   (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
      {| pointed_fun := k; dpoint_eq := 1 |}
    o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
         {| pointed_fun := g; dpoint_eq := 1 |}))^
  {
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |}) ==
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |}
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |} snapply Smash_ind_FlFr.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall (a : [X, point4]) (b : [Y, point3]),
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |})
  (sm a b) =
(functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
   {| pointed_fun := k; dpoint_eq := 1 |}
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  (sm a b)
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |})
  auxl =
(functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
   {| pointed_fun := k; dpoint_eq := 1 |}
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  auxl
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
functor_smash
  ({| pointed_fun := h; dpoint_eq := 1 |}
   o* {| pointed_fun := f; dpoint_eq := 1 |})
  ({| pointed_fun := k; dpoint_eq := 1 |}
   o* {| pointed_fun := g; dpoint_eq := 1 |})
  auxr =
(functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
   {| pointed_fun := k; dpoint_eq := 1 |}
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  auxr
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall a : [X, point4],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluel a) @
?Hl =
?Hsm a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a)
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall b : [Y, point3],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluer b) @
?Hr =
?Hsm pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b)
    1-3: reflexivity.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall a : [X, point4],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluel a) @
1 =
(fun (a0 : [X, point4]) (b : [Y, point3]) => 1) a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a)
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall b : [Y, point3],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluer b) @
1 =
(fun (a : [X, point4]) (b0 : [Y, point3]) => 1) pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b)
    -
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall a : [X, point4],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluel a) @
1 =
(fun (a0 : [X, point4]) (b : [Y, point3]) => 1) a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) intros x.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluel x) @
1 =
(fun (a : [X, point4]) (b : [Y, point3]) => 1) x pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x)
      apply equiv_p1_1q.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluel x) =
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x)
      lhs napply Smash_rec_beta_gluel.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap011 sm 1
  (point_eq
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
gluel
  (({| pointed_fun := h; dpoint_eq := 1 |}
    o* {| pointed_fun := f; dpoint_eq := 1 |}) x) =
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x)
      symmetry.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x) =
ap011 sm 1
  (point_eq
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
gluel
  (({| pointed_fun := h; dpoint_eq := 1 |}
    o* {| pointed_fun := f; dpoint_eq := 1 |}) x)
      lhs napply (ap_compose (functor_smash _ _) _ (gluel x)).
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (ap
     (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
     (gluel x)) =
ap011 sm 1
  (point_eq
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
gluel
  (({| pointed_fun := h; dpoint_eq := 1 |}
    o* {| pointed_fun := f; dpoint_eq := 1 |}) x)
      lhs napply ap.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x) =
?Goal
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  ?Goal =
ap011 sm 1
  (point_eq
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
gluel
  (({| pointed_fun := h; dpoint_eq := 1 |}
    o* {| pointed_fun := f; dpoint_eq := 1 |}) x)
      2: napply Smash_rec_beta_gluel.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel x) =
gluel ({| pointed_fun := f; dpoint_eq := 1 |} (fst (x, pt)))
      lhs napply Smash_rec_beta_gluel.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
x: [X, point4]
ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := f; dpoint_eq := 1 |} x) =
gluel ({| pointed_fun := f; dpoint_eq := 1 |} x)
      apply concat_1p.
    -
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
forall b : [Y, point3],
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluer b) @
1 =
(fun (a : [X, point4]) (b0 : [Y, point3]) => 1) pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) intros y.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluer y) @
1 =
(fun (a : [X, point4]) (b : [Y, point3]) => 1) pt y @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y)
      apply equiv_p1_1q.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (gluer y) =
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y)
      lhs napply Smash_rec_beta_gluer.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap011 sm
  (point_eq
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |}))
  1 @
gluer
  (({| pointed_fun := k; dpoint_eq := 1 |}
    o* {| pointed_fun := g; dpoint_eq := 1 |}) y) =
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y)
      symmetry.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y) =
ap011 sm
  (point_eq
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |}))
  1 @
gluer
  (({| pointed_fun := k; dpoint_eq := 1 |}
    o* {| pointed_fun := g; dpoint_eq := 1 |}) y)
      lhs napply (ap_compose (functor_smash _ _) _ (gluer y)).
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (ap
     (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
     (gluer y)) =
ap011 sm
  (point_eq
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |}))
  1 @
gluer
  (({| pointed_fun := k; dpoint_eq := 1 |}
    o* {| pointed_fun := g; dpoint_eq := 1 |}) y)
      lhs napply ap.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y) =
?Goal
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  ?Goal =
ap011 sm
  (point_eq
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |}))
  1 @
gluer
  (({| pointed_fun := k; dpoint_eq := 1 |}
    o* {| pointed_fun := g; dpoint_eq := 1 |}) y)
      2: napply Smash_rec_beta_gluer.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer y) =
gluer ({| pointed_fun := g; dpoint_eq := 1 |} (snd (pt, y)))
      lhs napply Smash_rec_beta_gluer.
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
y: [Y, point3]
ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := g; dpoint_eq := 1 |} y) =
gluer ({| pointed_fun := g; dpoint_eq := 1 |} y)
      apply concat_1p. }
X: Type
point4: IsPointed X
Y: Type
point3: IsPointed Y
A, B, C, D: Type
f: X -> A
g: Y -> B
h: A -> C
k: B -> D
Smash_ind_FlFr
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |}))
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |}
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (fun (a : [X, point4]) (b : [Y, point3]) => 1) 1 1
  (fun x : [X, point4] =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     (Smash_rec_beta_gluel
        (fun a : [X, point4] =>
         ap011 sm 1
           (point_eq
              ({| pointed_fun := k; dpoint_eq := 1 |}
               o* {| pointed_fun := g; dpoint_eq := 1 |})) @
         gluel
           (({| pointed_fun := h; dpoint_eq := 1 |}
             o* {| pointed_fun := f; dpoint_eq := 1 |}) a)
         :
         (fun (a0 : [X, point4]) (b : [Y, point3]) =>
          sm
            (({| pointed_fun := h; dpoint_eq := 1 |}
              o* {| pointed_fun := f; dpoint_eq := 1 |}) a0)
            (({| pointed_fun := k; dpoint_eq := 1 |}
              o* {| pointed_fun := g; dpoint_eq := 1 |}) b))
           a pt =
         auxl)
        (fun b : [Y, point3] =>
         ap011 sm
           (point_eq
              ({| pointed_fun := h; dpoint_eq := 1 |}
               o* {| pointed_fun := f; dpoint_eq := 1 |}))
           1 @
         gluer
           (({| pointed_fun := k; dpoint_eq := 1 |}
             o* {| pointed_fun := g; dpoint_eq := 1 |}) b)
         :
         (fun (a : [X, point4]) (b0 : [Y, point3]) =>
          sm
            (({| pointed_fun := h; dpoint_eq := 1 |}
              o* {| pointed_fun := f; dpoint_eq := 1 |}) a)
            (({| pointed_fun := k; dpoint_eq := 1 |}
              o* {| pointed_fun := g; dpoint_eq := 1 |}) b0))
           pt b =
         auxr)
        x @
      (ap_compose
         (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
            {| pointed_fun := g; dpoint_eq := 1 |})
         (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
            {| pointed_fun := k; dpoint_eq := 1 |})
         (gluel x) @
       (ap
          (ap
             (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
                {| pointed_fun := k; dpoint_eq := 1 |}))
          (Smash_rec_beta_gluel
             (fun a : [X, point4] =>
              ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
              gluel ({| pointed_fun := f; dpoint_eq := 1 |} a)
              :
              (fun (a0 : [X, point4]) (b : [Y, point3]) =>
               sm ({| pointed_fun := f; dpoint_eq := 1 |} a0)
                 ({| pointed_fun := g; dpoint_eq := 1 |} b))
                a pt =
              auxl)
             (fun b : [Y, point3] =>
              ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
              gluer ({| pointed_fun := g; dpoint_eq := 1 |} b)
              :
              (fun (a : [X, point4]) (b0 : [Y, point3]) =>
               sm ({| pointed_fun := f; dpoint_eq := 1 |} a)
                 ({| pointed_fun := g; dpoint_eq := 1 |} b0))
                pt b =
              auxr)
             x @
           concat_1p (gluel ({| pointed_fun := f; dpoint_eq := 1 |} x))) @
        Smash_rec_beta_gluel
          (fun a : [A, f point4] =>
           ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
           gluel ({| pointed_fun := h; dpoint_eq := 1 |} a)
           :
           (fun (a0 : [A, f point4]) (b : [B, g point3]) =>
            sm ({| pointed_fun := h; dpoint_eq := 1 |} a0)
              ({| pointed_fun := k; dpoint_eq := 1 |} b))
             a pt =
           auxl)
          (fun b : [B, g point3] =>
           ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
           gluer ({| pointed_fun := k; dpoint_eq := 1 |} b)
           :
           (fun (a : [A, f point4]) (b0 : [B, g point3]) =>
            sm ({| pointed_fun := h; dpoint_eq := 1 |} a)
              ({| pointed_fun := k; dpoint_eq := 1 |} b0))
             pt b =
           auxr)
          ({| pointed_fun := f; dpoint_eq := 1 |} (fst (x, pt)))))^))
  (fun y : [Y, point3] =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     (Smash_rec_beta_gluer
        (fun a : [X, point4] =>
         ap011 sm 1
           (point_eq
              ({| pointed_fun := k; dpoint_eq := 1 |}
               o* {| pointed_fun := g; dpoint_eq := 1 |})) @
         gluel
           (({| pointed_fun := h; dpoint_eq := 1 |}
             o* {| pointed_fun := f; dpoint_eq := 1 |}) a)
         :
         (fun (a0 : [X, point4]) (b : [Y, point3]) =>
          sm
            (({| pointed_fun := h; dpoint_eq := 1 |}
              o* {| pointed_fun := f; dpoint_eq := 1 |}) a0)
            (({| pointed_fun := k; dpoint_eq := 1 |}
              o* {| pointed_fun := g; dpoint_eq := 1 |}) b))
           a pt =
         auxl)
        (fun b : [Y, point3] =>
         ap011 sm
           (point_eq
              ({| pointed_fun := h; dpoint_eq := 1 |}
               o* {| pointed_fun := f; dpoint_eq := 1 |}))
           1 @
         gluer
           (({| pointed_fun := k; dpoint_eq := 1 |}
             o* {| pointed_fun := g; dpoint_eq := 1 |}) b)
         :
         (fun (a : [X, point4]) (b0 : [Y, point3]) =>
          sm
            (({| pointed_fun := h; dpoint_eq := 1 |}
              o* {| pointed_fun := f; dpoint_eq := 1 |}) a)
            (({| pointed_fun := k; dpoint_eq := 1 |}
              o* {| pointed_fun := g; dpoint_eq := 1 |}) b0))
           pt b =
         auxr)
        y @
      (ap_compose
         (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
            {| pointed_fun := g; dpoint_eq := 1 |})
         (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
            {| pointed_fun := k; dpoint_eq := 1 |})
         (gluer y) @
       (ap
          (ap
             (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
                {| pointed_fun := k; dpoint_eq := 1 |}))
          (Smash_rec_beta_gluer
             (fun a : [X, point4] =>
              ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
              gluel ({| pointed_fun := f; dpoint_eq := 1 |} a)
              :
              (fun (a0 : [X, point4]) (b : [Y, point3]) =>
               sm ({| pointed_fun := f; dpoint_eq := 1 |} a0)
                 ({| pointed_fun := g; dpoint_eq := 1 |} b))
                a pt =
              auxl)
             (fun b : [Y, point3] =>
              ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
              gluer ({| pointed_fun := g; dpoint_eq := 1 |} b)
              :
              (fun (a : [X, point4]) (b0 : [Y, point3]) =>
               sm ({| pointed_fun := f; dpoint_eq := 1 |} a)
                 ({| pointed_fun := g; dpoint_eq := 1 |} b0))
                pt b =
              auxr)
             y @
           concat_1p (gluer ({| pointed_fun := g; dpoint_eq := 1 |} y))) @
        Smash_rec_beta_gluer
          (fun a : [A, f point4] =>
           ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
           gluel ({| pointed_fun := h; dpoint_eq := 1 |} a)
           :
           (fun (a0 : [A, f point4]) (b : [B, g point3]) =>
            sm ({| pointed_fun := h; dpoint_eq := 1 |} a0)
              ({| pointed_fun := k; dpoint_eq := 1 |} b))
             a pt =
           auxl)
          (fun b : [B, g point3] =>
           ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
           gluer ({| pointed_fun := k; dpoint_eq := 1 |} b)
           :
           (fun (a : [A, f point4]) (b0 : [B, g point3]) =>
            sm ({| pointed_fun := h; dpoint_eq := 1 |} a)
              ({| pointed_fun := k; dpoint_eq := 1 |} b0))
             pt b =
           auxr)
          ({| pointed_fun := g; dpoint_eq := 1 |} (snd (pt, y)))))^))
  pt =
dpoint_eq
  (functor_smash
     ({| pointed_fun := h; dpoint_eq := 1 |}
      o* {| pointed_fun := f; dpoint_eq := 1 |})
     ({| pointed_fun := k; dpoint_eq := 1 |}
      o* {| pointed_fun := g; dpoint_eq := 1 |})) @
(dpoint_eq
   (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
      {| pointed_fun := k; dpoint_eq := 1 |}
    o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
         {| pointed_fun := g; dpoint_eq := 1 |}))^
  reflexivity.
Defined.

Definition functor_smash_homotopic {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.
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.
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
  pointed_reduce.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} ==*
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |}
  snapply Build_pHomotopy.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} ==
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |}
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
?p pt =
dpoint_eq
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
(dpoint_eq
   (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
      {| pointed_fun := k; dpoint_eq := 1 |}))^
  {
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} ==
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} snapply Smash_ind_FlFr.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall (a : [X, point2]) (b : [Y, point1]),
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} 
  (sm a b) =
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} (sm a b)
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} auxl =
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} auxl
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} auxr =
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} auxr
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall a : [X, point2],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel a) @
?Hl =
?Hsm a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel a)
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall b : [Y, point1],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer b) @
?Hr =
?Hsm pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer b)
    1: exact (fun x y => ap011 _ (p x) (q y)).
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} auxl =
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} auxl
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
  {| pointed_fun := g; dpoint_eq := q point1 @ 1 |} auxr =
functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
  {| pointed_fun := k; dpoint_eq := 1 |} auxr
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall a : [X, point2],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel a) @
?Hl =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel a)
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall b : [Y, point1],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer b) @
?Hr =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer b)
    1,2: reflexivity.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall a : [X, point2],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel a) @
1 =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel a)
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall b : [Y, point1],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer b) @
1 =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer b)
    -
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall a : [X, point2],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel a) @
1 =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) a pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel a) intros x.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel x) @
1 =
(fun (x0 : [X, point2]) (y : [Y, point1]) => ap011 sm (p x0) (q y)) x pt @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel x)
      lhs napply concat_p1.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluel x) =
ap011 sm (p x) (q pt) @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel x)
      lhs napply Smash_rec_beta_gluel.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} x) =
ap011 sm (p x) (q pt) @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel x)
      rhs napply whiskerL.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} x) =
ap011 sm (p x) (q pt) @ ?Goal
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluel x) =
?Goal
      2: napply Smash_rec_beta_gluel.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} x) =
ap011 sm (p x) (q pt) @
(ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
 gluel ({| pointed_fun := h; dpoint_eq := 1 |} x))
      simpl; induction (p x); simpl.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap (sm (f x)) (q point1 @ 1) @ gluel (f x) =
ap (sm (f x)) (q pt) @ (1 @ gluel (f x))
      rhs_V napply concat_pp_p.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap (sm (f x)) (q point1 @ 1) @ gluel (f x) =
(ap (sm (f x)) (q pt) @ 1) @ gluel (f x)
      apply whiskerR.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x0 : X, f x0 = h x0
q: forall x0 : Y, g x0 = k x0
x: [X, point2]
ap (sm (f x)) (q point1 @ 1) = ap (sm (f x)) (q pt) @ 1
      napply ap_pp.
    -
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
forall b : [Y, point1],
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer b) @
1 =
(fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) pt b @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer b) intros y.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer y) @
1 =
(fun (x : [X, point2]) (y0 : [Y, point1]) => ap011 sm (p x) (q y0)) pt y @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer y)
      lhs napply concat_p1.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (gluer y) =
ap011 sm (p pt) (q y) @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer y)
      lhs napply Smash_rec_beta_gluer.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}) 1 @
gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} y) =
ap011 sm (p pt) (q y) @
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer y)
      rhs napply whiskerL.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}) 1 @
gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} y) =
ap011 sm (p pt) (q y) @ ?Goal
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (gluer y) =
?Goal
      2: napply Smash_rec_beta_gluer.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}) 1 @
gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} y) =
ap011 sm (p pt) (q y) @
(ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
 gluer ({| pointed_fun := k; dpoint_eq := 1 |} y))
      simpl; induction (q y); simpl.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (p point2 @ 1) 1 @ gluer (g y) =
ap011 sm (p pt) 1 @ (1 @ gluer (g y))
      rhs_V napply concat_pp_p.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (p point2 @ 1) 1 @ gluer (g y) =
(ap011 sm (p pt) 1 @ 1) @ gluer (g y)
      apply whiskerR.
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
y: [Y, point1]
ap011 sm (p point2 @ 1) 1 = ap011 sm (p pt) 1 @ 1
      exact (ap011_pp _ _ _ 1 1). }
X: Type
point2: IsPointed X
Y: Type
point1: IsPointed Y
A, B: Type
f, h: X -> A
g, k: Y -> B
p: forall x : X, f x = h x
q: forall x : Y, g x = k x
Smash_ind_FlFr
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
  (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
     {| pointed_fun := k; dpoint_eq := 1 |})
  (fun (x : [X, point2]) (y : [Y, point1]) => ap011 sm (p x) (q y)) 1 1
  (fun x : [X, point2] =>
   concat_p1
     (ap
        (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
           {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
        (gluel x)) @
   (Smash_rec_beta_gluel
      (fun a : [X, point2] =>
       ap011 sm 1
         (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
       gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a)
       :
       (fun (a0 : [X, point2]) (b : [Y, point1]) =>
        sm ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a0)
          ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b))
         a pt =
       auxl)
      (fun b : [Y, point1] =>
       ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |})
         1 @
       gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b)
       :
       (fun (a : [X, point2]) (b0 : [Y, point1]) =>
        sm ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a)
          ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b0))
         pt b =
       auxr)
      x @
    (((let p0 := p x in
       let a := h x in
       paths_rect A (f x)
         (fun (a0 : A) (p1 : f x = a0) =>
          ap (sm (f x)) (q point1 @ 1) @ gluel (f x) =
          ap011 sm p1 (q pt) @ (1 @ gluel a0))
         (whiskerR (ap_pp (sm (f x)) (q point1) 1) (gluel (f x)) @
          concat_pp_p (ap (sm (f x)) (q pt)) 1 (gluel (f x))
          :
          ap (sm (f x)) (q point1 @ 1) @ gluel (f x) =
          ap011 sm 1 (q pt) @ (1 @ gluel (f x)))
         a p0)
      :
      ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
      gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} x) =
      ap011 sm (p x) (q pt) @
      (ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
       gluel ({| pointed_fun := h; dpoint_eq := 1 |} x))) @
     (whiskerL (ap011 sm (p x) (q pt))
        (Smash_rec_beta_gluel
           (fun a : [X, point2] =>
            ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
            gluel ({| pointed_fun := h; dpoint_eq := 1 |} a)
            :
            (fun (a0 : [X, point2]) (b : [Y, point1]) =>
             sm ({| pointed_fun := h; dpoint_eq := 1 |} a0)
               ({| pointed_fun := k; dpoint_eq := 1 |} b))
              a pt =
            auxl)
           (fun b : [Y, point1] =>
            ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
            gluer ({| pointed_fun := k; dpoint_eq := 1 |} b)
            :
            (fun (a : [X, point2]) (b0 : [Y, point1]) =>
             sm ({| pointed_fun := h; dpoint_eq := 1 |} a)
               ({| pointed_fun := k; dpoint_eq := 1 |} b0))
              pt b =
            auxr)
           x))^)))
  (fun y : [Y, point1] =>
   concat_p1
     (ap
        (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
           {| pointed_fun := g; dpoint_eq := q point1 @ 1 |})
        (gluer y)) @
   (Smash_rec_beta_gluer
      (fun a : [X, point2] =>
       ap011 sm 1
         (point_eq {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
       gluel ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a)
       :
       (fun (a0 : [X, point2]) (b : [Y, point1]) =>
        sm ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a0)
          ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b))
         a pt =
       auxl)
      (fun b : [Y, point1] =>
       ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |})
         1 @
       gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b)
       :
       (fun (a : [X, point2]) (b0 : [Y, point1]) =>
        sm ({| pointed_fun := f; dpoint_eq := p point2 @ 1 |} a)
          ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} b0))
         pt b =
       auxr)
      y @
    (((let p0 := q y in
       let b := k y in
       paths_rect B (g y)
         (fun (b0 : B) (p1 : g y = b0) =>
          ap011 sm (p point2 @ 1) 1 @ gluer (g y) =
          ap011 sm (p pt) p1 @ (1 @ gluer b0))
         (whiskerR (ap011_pp sm (p point2) 1 1 1) (gluer (g y)) @
          concat_pp_p (ap011 sm (p pt) 1) 1 (gluer (g y))
          :
          ap011 sm (p point2 @ 1) 1 @ gluer (g y) =
          ap011 sm (p pt) 1 @ (1 @ gluer (g y)))
         b p0)
      :
      ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}) 1 @
      gluer ({| pointed_fun := g; dpoint_eq := q point1 @ 1 |} y) =
      ap011 sm (p pt) (q y) @
      (ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
       gluer ({| pointed_fun := k; dpoint_eq := 1 |} y))) @
     (whiskerL (ap011 sm (p pt) (q y))
        (Smash_rec_beta_gluer
           (fun a : [X, point2] =>
            ap011 sm 1 (point_eq {| pointed_fun := k; dpoint_eq := 1 |}) @
            gluel ({| pointed_fun := h; dpoint_eq := 1 |} a)
            :
            (fun (a0 : [X, point2]) (b : [Y, point1]) =>
             sm ({| pointed_fun := h; dpoint_eq := 1 |} a0)
               ({| pointed_fun := k; dpoint_eq := 1 |} b))
              a pt =
            auxl)
           (fun b : [Y, point1] =>
            ap011 sm (point_eq {| pointed_fun := h; dpoint_eq := 1 |}) 1 @
            gluer ({| pointed_fun := k; dpoint_eq := 1 |} b)
            :
            (fun (a : [X, point2]) (b0 : [Y, point1]) =>
             sm ({| pointed_fun := h; dpoint_eq := 1 |} a)
               ({| pointed_fun := k; dpoint_eq := 1 |} b0))
              pt b =
            auxr)
           y))^)))
  pt =
dpoint_eq
  (functor_smash {| pointed_fun := f; dpoint_eq := p point2 @ 1 |}
     {| pointed_fun := g; dpoint_eq := q point1 @ 1 |}) @
(dpoint_eq
   (functor_smash {| pointed_fun := h; dpoint_eq := 1 |}
      {| pointed_fun := k; dpoint_eq := 1 |}))^
  exact (ap022 _ (concat_p1 (p pt))^ (concat_p1 (q pt))^ @ (concat_p1 _)^).
Defined.

#[export] Instance is0bifunctor_smash : Is0Bifunctor Smash.
Is0Bifunctor Smash
Proof.
Is0Bifunctor Smash
  snapply Build_Is0Bifunctor'.
Is01Cat pType
Is01Cat pType
Is0Functor (uncurry Smash)
  1,2: exact _.
Is0Functor (uncurry Smash)
  napply Build_Is0Functor.
forall a b : pType * pType, (a $-> b) -> uncurry Smash a $-> uncurry Smash b
  intros [X Y] [A B] [f g].
X, Y, A, B: pType
f: fst (X, Y) $-> fst (A, B)
g: snd (X, Y) $-> snd (A, B)
uncurry Smash (X, Y) $-> uncurry Smash (A, B)
  exact (functor_smash f g).
Defined.

#[export] Instance is1bifunctor_smash : Is1Bifunctor Smash.
Is1Bifunctor Smash
Proof.
Is1Bifunctor Smash
  snapply Build_Is1Bifunctor'.
Is1Functor (uncurry Smash)
  snapply Build_Is1Functor.
forall (a b : pType * pType) (f g : a $-> b),
f $== g -> fmap (uncurry Smash) f $== fmap (uncurry Smash) g
forall a : pType * pType,
fmap (uncurry Smash) (Id a) $== Id (uncurry Smash a)
forall (a b c : pType * pType) (f : a $-> b) (g : b $-> c),
fmap (uncurry Smash) (g $o f) $==
fmap (uncurry Smash) g $o fmap (uncurry Smash) f
  -
forall (a b : pType * pType) (f g : a $-> b),
f $== g -> fmap (uncurry Smash) f $== fmap (uncurry Smash) g intros [X Y] [A B] [f g] [h i] [p q].
X, Y, A, B: pType
f: fst (X, Y) $-> fst (A, B)
g: snd (X, Y) $-> snd (A, B)
h: fst (X, Y) $-> fst (A, B)
i: snd (X, Y) $-> snd (A, B)
p: fst (f, g) $-> fst (h, i)
q: snd (f, g) $-> snd (h, i)
fmap (uncurry Smash) (f, g) $== fmap (uncurry Smash) (h, i)
    exact (functor_smash_homotopic p q).
  -
forall a : pType * pType,
fmap (uncurry Smash) (Id a) $== Id (uncurry Smash a) intros [X Y].
X, Y: pType
fmap (uncurry Smash) (Id (X, Y)) $== Id (uncurry Smash (X, Y))
    exact (functor_smash_idmap X Y).
  -
forall (a b c : pType * pType) (f : a $-> b) (g : b $-> c),
fmap (uncurry Smash) (g $o f) $==
fmap (uncurry Smash) g $o fmap (uncurry Smash) f intros [X Y] [A B] [C D] [f g] [h i].
X, Y, A, B, C, D: pType
f: fst (X, Y) $-> fst (A, B)
g: snd (X, Y) $-> snd (A, B)
h: fst (A, B) $-> fst (C, D)
i: snd (A, B) $-> snd (C, D)
fmap (uncurry Smash) ((h, i) $o (f, g)) $==
fmap (uncurry Smash) (h, i) $o fmap (uncurry Smash) (f, g)
    exact (functor_smash_compose f g h i).
Defined.

(** ** Symmetry of the smash product *)

Definition pswap (X Y : pType) : Smash X Y $-> Smash Y X
  := Build_pMap (Smash_rec (flip sm) auxr auxl gluer gluel) 1.

Definition pswap_pswap {X Y : pType}
  : pswap X Y $o pswap Y X $== pmap_idmap.
X, Y: pType
pswap X Y $o pswap Y X $== pmap_idmap
Proof.
X, Y: pType
pswap X Y $o pswap Y X $== pmap_idmap
  snapply Build_pHomotopy.
X, Y: pType
pswap X Y $o pswap Y X == pmap_idmap
X, Y: pType
?p pt = dpoint_eq (pswap X Y $o pswap Y X) @ (dpoint_eq pmap_idmap)^
  -
X, Y: pType
pswap X Y $o pswap Y X == pmap_idmap snapply Smash_ind_FFlr.
X, Y: pType
forall (a : Y) (b : X), pswap X Y (pswap Y X (sm a b)) = sm a b
X, Y: pType
pswap X Y (pswap Y X auxl) = auxl
X, Y: pType
pswap X Y (pswap Y X auxr) = auxr
X, Y: pType
forall a : Y,
ap (pswap X Y) (ap (pswap Y X) (gluel a)) @ ?Hl = ?Hsm a pt @ gluel a
X, Y: pType
forall b : X,
ap (pswap X Y) (ap (pswap Y X) (gluer b)) @ ?Hr = ?Hsm pt b @ gluer b
    1-3: reflexivity.
X, Y: pType
forall a : Y,
ap (pswap X Y) (ap (pswap Y X) (gluel a)) @ 1 =
(fun (a0 : Y) (b : X) => 1) a pt @ gluel a
X, Y: pType
forall b : X,
ap (pswap X Y) (ap (pswap Y X) (gluer b)) @ 1 =
(fun (a : Y) (b0 : X) => 1) pt b @ gluer b
    +
X, Y: pType
forall a : Y,
ap (pswap X Y) (ap (pswap Y X) (gluel a)) @ 1 =
(fun (a0 : Y) (b : X) => 1) a pt @ gluel a intros y.
X, Y: pType
y: Y
ap (pswap X Y) (ap (pswap Y X) (gluel y)) @ 1 =
(fun (a : Y) (b : X) => 1) y pt @ gluel y
      apply equiv_p1_1q.
X, Y: pType
y: Y
ap (pswap X Y) (ap (pswap Y X) (gluel y)) = gluel y
      lhs napply ap.
X, Y: pType
y: Y
ap (pswap Y X) (gluel y) = ?Goal
X, Y: pType
y: Y
ap (pswap X Y) ?Goal = gluel y
      1: apply Smash_rec_beta_gluel.
X, Y: pType
y: Y
ap (pswap X Y) (gluer y) = gluel y
      napply Smash_rec_beta_gluer.
    +
X, Y: pType
forall b : X,
ap (pswap X Y) (ap (pswap Y X) (gluer b)) @ 1 =
(fun (a : Y) (b0 : X) => 1) pt b @ gluer b intros x.
X, Y: pType
x: X
ap (pswap X Y) (ap (pswap Y X) (gluer x)) @ 1 =
(fun (a : Y) (b : X) => 1) pt x @ gluer x
      apply equiv_p1_1q.
X, Y: pType
x: X
ap (pswap X Y) (ap (pswap Y X) (gluer x)) = gluer x
      lhs napply ap.
X, Y: pType
x: X
ap (pswap Y X) (gluer x) = ?Goal
X, Y: pType
x: X
ap (pswap X Y) ?Goal = gluer x
      1: apply Smash_rec_beta_gluer.
X, Y: pType
x: X
ap (pswap X Y) (gluel x) = gluer x
      napply Smash_rec_beta_gluel.
  -
X, Y: pType
Smash_ind_FFlr (pswap Y X) (pswap X Y) (fun (a : Y) (b : X) => 1) 1 1
  (fun y : Y =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     (ap (ap (pswap X Y)) (Smash_rec_beta_gluel gluer gluel y) @
      Smash_rec_beta_gluer gluer gluel y))
  (fun x : X =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     (ap (ap (pswap X Y)) (Smash_rec_beta_gluer gluer gluel x) @
      Smash_rec_beta_gluel gluer gluel x))
  pt =
dpoint_eq (pswap X Y $o pswap Y X) @ (dpoint_eq pmap_idmap)^ reflexivity.
Defined.

Definition pequiv_pswap {X Y : pType} : Smash X Y $<~> Smash Y X.
X, Y: pType
Smash X Y $<~> Smash Y X
Proof.
X, Y: pType
Smash X Y $<~> Smash Y X
  snapply cate_adjointify.
X, Y: pType
Smash X Y $-> Smash Y X
X, Y: pType
Smash Y X $-> Smash X Y
X, Y: pType
?f $o ?g $== Id (Smash Y X)
X, Y: pType
?g $o ?f $== Id (Smash X Y)
  1,2: exact (pswap _ _).
X, Y: pType
pswap X Y $o pswap Y X $== Id (Smash Y X)
X, Y: pType
pswap Y X $o pswap X Y $== Id (Smash X Y)
  1,2: exact pswap_pswap.
Defined.

Definition pswap_natural {A B X Y : pType} (f : A $-> X) (g : B $-> Y)
  : pswap X Y $o functor_smash f g $== functor_smash g f $o pswap A B.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
pswap X Y $o functor_smash f g $== functor_smash g f $o pswap A B
Proof.
A, B, X, Y: pType
f: A $-> X
g: B $-> Y
pswap X Y $o functor_smash f g $== functor_smash g f $o pswap A B
  pointed_reduce.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
pswap [X, f point2] [Y, g point1]
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |} ==*
functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
  {| pointed_fun := f; dpoint_eq := 1 |}
o* pswap [A, point2] [B, point1]
  snapply Build_pHomotopy.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
pswap [X, f point2] [Y, g point1]
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |} ==
functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
  {| pointed_fun := f; dpoint_eq := 1 |}
o* pswap [A, point2] [B, point1]
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
?p pt =
dpoint_eq
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |}) @
(dpoint_eq
   (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
      {| pointed_fun := f; dpoint_eq := 1 |}
    o* pswap [A, point2] [B, point1]))^
  -
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
pswap [X, f point2] [Y, g point1]
o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |} ==
functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
  {| pointed_fun := f; dpoint_eq := 1 |}
o* pswap [A, point2] [B, point1] snapply Smash_ind_FlFr.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall (a : [A, point2]) (b : [B, point1]),
(pswap [X, f point2] [Y, g point1]
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  (sm a b) =
(functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
   {| pointed_fun := f; dpoint_eq := 1 |}
 o* pswap [A, point2] [B, point1]) (sm a b)
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
(pswap [X, f point2] [Y, g point1]
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  auxl =
(functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
   {| pointed_fun := f; dpoint_eq := 1 |}
 o* pswap [A, point2] [B, point1]) auxl
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
(pswap [X, f point2] [Y, g point1]
 o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
      {| pointed_fun := g; dpoint_eq := 1 |})
  auxr =
(functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
   {| pointed_fun := f; dpoint_eq := 1 |}
 o* pswap [A, point2] [B, point1]) auxr
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall a : [A, point2],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) @
?Hl =
?Hsm a pt @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluel a)
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall b : [B, point1],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) @
?Hr =
?Hsm pt b @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluer b)
    1-3: reflexivity.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall a : [A, point2],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) @
1 =
(fun (a0 : [A, point2]) (b : [B, point1]) => 1) a pt @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluel a)
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall b : [B, point1],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) @
1 =
(fun (a : [A, point2]) (b0 : [B, point1]) => 1) pt b @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluer b)
    +
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall a : [A, point2],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) @
1 =
(fun (a0 : [A, point2]) (b : [B, point1]) => 1) a pt @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluel a) intros a.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) @
1 =
(fun (a0 : [A, point2]) (b : [B, point1]) => 1) a pt @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluel a)
      apply equiv_p1_1q.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluel a)
      rhs napply (ap_compose (pswap _ _) _ (gluel a)).
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  (ap (pswap [A, point2] [B, point1]) (gluel a))
      rhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  ?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (pswap [A, point2] [B, point1]) (gluel a) = ?Goal
      2: apply Smash_rec_beta_gluel.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  (gluer a)
      rhs napply Smash_rec_beta_gluer.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := f; dpoint_eq := 1 |} a)
      lhs napply (ap_compose (functor_smash _ _) (pswap _ _) (gluel a)).
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (pswap [X, f point2] [Y, g point1])
  (ap
     (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
     (gluel a)) =
ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := f; dpoint_eq := 1 |} a)
      lhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluel a) =
?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (pswap [X, f point2] [Y, g point1]) ?Goal =
ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := f; dpoint_eq := 1 |} a)
      1: apply Smash_rec_beta_gluel.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (pswap [X, f point2] [Y, g point1])
  (ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
   gluel ({| pointed_fun := f; dpoint_eq := 1 |} a)) =
ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := f; dpoint_eq := 1 |} a)
      simpl.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (Smash_rec (flip sm) auxr auxl gluer gluel) (1 @ gluel (f a)) =
1 @ gluer (f a)
      lhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
1 @ gluel (f a) = ?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (Smash_rec (flip sm) auxr auxl gluer gluel) ?Goal = 1 @ gluer (f a)
      1: apply concat_1p.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (Smash_rec (flip sm) auxr auxl gluer gluel) (gluel (f a)) =
1 @ gluer (f a)
      rhs napply concat_1p.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
a: [A, point2]
ap (Smash_rec (flip sm) auxr auxl gluer gluel) (gluel (f a)) = gluer (f a)
      napply Smash_rec_beta_gluel.
    +
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
forall b : [B, point1],
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) @
1 =
(fun (a : [A, point2]) (b0 : [B, point1]) => 1) pt b @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluer b) intros b.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) @
1 =
(fun (a : [A, point2]) (b0 : [B, point1]) => 1) pt b @
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluer b)
      apply equiv_p1_1q.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (gluer b)
      rhs napply (ap_compose (pswap _ _) (functor_smash _ _) (gluer b)).
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  (ap (pswap [A, point2] [B, point1]) (gluer b))
      rhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  ?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [A, point2] [B, point1]) (gluer b) = ?Goal
      2: apply Smash_rec_beta_gluer.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
ap
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |})
  (gluel b)
      rhs napply Smash_rec_beta_gluel.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      lhs napply (ap_compose (functor_smash _ _) (pswap _ _) (gluer b)).
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1])
  (ap
     (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
     (gluer b)) =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      lhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap
  (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
     {| pointed_fun := g; dpoint_eq := 1 |})
  (gluer b) =
?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1]) ?Goal =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      1: apply Smash_rec_beta_gluer.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1])
  (ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
   gluer ({| pointed_fun := g; dpoint_eq := 1 |} b)) =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      lhs napply ap.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
gluer ({| pointed_fun := g; dpoint_eq := 1 |} b) = 
?Goal
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1]) ?Goal =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      1: apply concat_1p.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1])
  (gluer ({| pointed_fun := g; dpoint_eq := 1 |} b)) =
ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      rhs napply concat_1p.
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
b: [B, point1]
ap (pswap [X, f point2] [Y, g point1])
  (gluer ({| pointed_fun := g; dpoint_eq := 1 |} b)) =
gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)
      napply Smash_rec_beta_gluer.
  -
A: Type
point2: IsPointed A
B: Type
point1: IsPointed B
X, Y: Type
f: A -> X
g: B -> Y
Smash_ind_FlFr
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |})
  (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
     {| pointed_fun := f; dpoint_eq := 1 |}
   o* pswap [A, point2] [B, point1])
  (fun (a : [A, point2]) (b : [B, point1]) => 1) 1 1
  (fun a : [A, point2] =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     ((((ap_compose
           (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
              {| pointed_fun := g; dpoint_eq := 1 |})
           (pswap [X, f point2] [Y, g point1]) (gluel a) @
         (ap (ap (pswap [X, f point2] [Y, g point1]))
            (Smash_rec_beta_gluel
               (fun a0 : [A, point2] =>
                ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
                gluel ({| pointed_fun := f; dpoint_eq := 1 |} a0))
               (fun b : [B, point1] =>
                ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
                gluer ({| pointed_fun := g; dpoint_eq := 1 |} b))
               a) @
          (ap (ap (Smash_rec (flip sm) auxr auxl gluer gluel))
             (concat_1p (gluel (f a))) @
           (Smash_rec_beta_gluel gluer gluel (f a) @
            (concat_1p (gluer (f a)))^)
           :
           ap (pswap [X, f point2] [Y, g point1])
             (ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
              gluel ({| pointed_fun := f; dpoint_eq := 1 |} a)) =
           ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
           gluer ({| pointed_fun := f; dpoint_eq := 1 |} a)))) @
        (Smash_rec_beta_gluer
           (fun a0 : [B, point1] =>
            ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
            gluel ({| pointed_fun := g; dpoint_eq := 1 |} a0)
            :
            (fun (a1 : [B, point1]) (b : [A, point2]) =>
             sm ({| pointed_fun := g; dpoint_eq := 1 |} a1)
               ({| pointed_fun := f; dpoint_eq := 1 |} b))
              a0 pt =
            auxl)
           (fun b : [A, point2] =>
            ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
            gluer ({| pointed_fun := f; dpoint_eq := 1 |} b)
            :
            (fun (a0 : [B, point1]) (b0 : [A, point2]) =>
             sm ({| pointed_fun := g; dpoint_eq := 1 |} a0)
               ({| pointed_fun := f; dpoint_eq := 1 |} b0))
              pt b =
            auxr)
           a)^) @
       (ap
          (ap
             (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
                {| pointed_fun := f; dpoint_eq := 1 |}))
          (Smash_rec_beta_gluel gluer gluel a))^) @
      (ap_compose (pswap [A, point2] [B, point1])
         (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
            {| pointed_fun := f; dpoint_eq := 1 |})
         (gluel a))^))
  (fun b : [B, point1] =>
   let X0 := equiv_fun equiv_p1_1q in
   X0
     ((((ap_compose
           (functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
              {| pointed_fun := g; dpoint_eq := 1 |})
           (pswap [X, f point2] [Y, g point1]) (gluer b) @
         (ap (ap (pswap [X, f point2] [Y, g point1]))
            (Smash_rec_beta_gluer
               (fun a : [A, point2] =>
                ap011 sm 1 (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) @
                gluel ({| pointed_fun := f; dpoint_eq := 1 |} a))
               (fun b0 : [B, point1] =>
                ap011 sm (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) 1 @
                gluer ({| pointed_fun := g; dpoint_eq := 1 |} b0))
               b) @
          (ap (ap (pswap [X, f point2] [Y, g point1]))
             (concat_1p (gluer ({| pointed_fun := g; dpoint_eq := 1 |} b))) @
           (Smash_rec_beta_gluer gluer gluel
              ({| pointed_fun := g; dpoint_eq := 1 |} (snd (pt, b))) @
            (concat_1p (gluel ({| pointed_fun := g; dpoint_eq := 1 |} b)))^)))) @
        (Smash_rec_beta_gluel
           (fun a : [B, point1] =>
            ap011 sm 1 (point_eq {| pointed_fun := f; dpoint_eq := 1 |}) @
            gluel ({| pointed_fun := g; dpoint_eq := 1 |} a)
            :
            (fun (a0 : [B, point1]) (b0 : [A, point2]) =>
             sm ({| pointed_fun := g; dpoint_eq := 1 |} a0)
               ({| pointed_fun := f; dpoint_eq := 1 |} b0))
              a pt =
            auxl)
           (fun b0 : [A, point2] =>
            ap011 sm (point_eq {| pointed_fun := g; dpoint_eq := 1 |}) 1 @
            gluer ({| pointed_fun := f; dpoint_eq := 1 |} b0)
            :
            (fun (a : [B, point1]) (b1 : [A, point2]) =>
             sm ({| pointed_fun := g; dpoint_eq := 1 |} a)
               ({| pointed_fun := f; dpoint_eq := 1 |} b1))
              pt b0 =
            auxr)
           b)^) @
       (ap
          (ap
             (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
                {| pointed_fun := f; dpoint_eq := 1 |}))
          (Smash_rec_beta_gluer gluer gluel b))^) @
      (ap_compose (pswap [A, point2] [B, point1])
         (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
            {| pointed_fun := f; dpoint_eq := 1 |})
         (gluer b))^))
  pt =
dpoint_eq
  (pswap [X, f point2] [Y, g point1]
   o* functor_smash {| pointed_fun := f; dpoint_eq := 1 |}
        {| pointed_fun := g; dpoint_eq := 1 |}) @
(dpoint_eq
   (functor_smash {| pointed_fun := g; dpoint_eq := 1 |}
      {| pointed_fun := f; dpoint_eq := 1 |}
    o* pswap [A, point2] [B, point1]))^ reflexivity.
Defined.