Smash.v

Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics Basics.Equivalences.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 (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
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 a : X, Psm a 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 a : X, Psm a 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 a : X, Psm a 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 a : X, Psm a 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 a : X, Psm a 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 b : Y, Psm pt b = 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 b : Y, Psm pt b = 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 b : Y, Psm pt b = 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 b : Y, Psm pt b = 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 b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, 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)^)
  Proof.X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b : Y, 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)^)
    lhs napply ap_pp.X, Y: pType
P: Type
Psm: X -> Y -> P
Pl, Pr: P
Pgl: forall a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 a : X, Psm a pt = Pl
Pgr: forall b : Y, Psm pt b = 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 (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)
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 (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)
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) (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)
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) (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)
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 (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
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 (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
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) (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
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) (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
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 ({| ... |} a0) ({| ... |} 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 ({| ... |} a) ({| ... |} 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 ({| ... |} a0) ({| ... |} 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 ({| ... |} a) ({| ... |} 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 x : X, f x = h x
q: forall x : Y, g x = k x
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 (x : [X, point2]) (y : [Y, point1]) =>
 ap011 sm (p x) (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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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 x : X, f x = h x
q: forall x : Y, g x = k x
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]) (y : [Y, point1]) =>
 ap011 sm (p x) (q y)) 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 (a : [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]) (b : [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 {| ...; ... |}) @
                gluel ({| ...; ... |} a0))
               (fun b : [B, point1] =>
                ap011 sm (point_eq {| ...; ... |}) 1 @
                gluer ({| ...; ... |} 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 {| ...; ... |}) @
              gluel ({| ...; ... |} 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 {| ...; ... |}) @
                gluel ({| ...; ... |} a))
               (fun b0 : [B, point1] =>
                ap011 sm (point_eq {| ...; ... |}) 1 @
                gluer ({| ...; ... |} b0)) b) @
          (ap (ap (pswap [X, f point2] [Y, g point1]))
             (concat_1p (gluer ({| ...; ... |} b))) @
           (Smash_rec_beta_gluer gluer gluel
              ({| pointed_fun := g; dpoint_eq := 1 |}
                 (snd (pt, b))) @
            (concat_1p (gluel ({| ... |} 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.