Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.Core Pointed.pSusp.
Require Import Colimits.Pushout.
Require Import WildCat.
Require Import Homotopy.Suspension.

Local Set Universe Minimization ToSet.

(** * Wedge sums *)

Local Open Scope pointed_scope.

Definition Wedge (X Y : pType) : pType
  := [Pushout (fun _ : Unit => point X) (fun _ => point Y), pushl (point X)].

Notation "X \/ Y" := (Wedge X Y) : pointed_scope.

Definition wedge_inl {X Y} : X $-> X \/ Y.
X, Y: pType
X $-> X \/ Y
Proof.
X, Y: pType
X $-> X \/ Y
  snrapply Build_pMap.
X, Y: pType
X -> X \/ Y
X, Y: pType
?Goal pt = pt
  -
X, Y: pType
X -> X \/ Y exact (fun x => pushl x).
  -
X, Y: pType
(fun x : X => pushl x) pt = pt reflexivity.
Defined.

Definition wedge_inr {X Y} : Y $-> X \/ Y.
X, Y: pType
Y $-> X \/ Y
Proof.
X, Y: pType
Y $-> X \/ Y
  snrapply Build_pMap.
X, Y: pType
Y -> X \/ Y
X, Y: pType
?Goal pt = pt
  -
X, Y: pType
Y -> X \/ Y exact (fun x => pushr x).
  -
X, Y: pType
(fun x : Y => pushr x) pt = pt symmetry.
X, Y: pType
pt = (fun x : Y => pushr x) pt
    by rapply pglue.
Defined.

Definition wglue {X Y : pType}
  : pushl (point X) = (pushr (point Y)) :> (X \/ Y) := pglue tt.

(** Wedge recursion into an unpointed type. *)
Definition wedge_rec' {X Y : pType} {Z : Type}
  (f : X -> Z) (g : Y -> Z) (w : f pt = g pt)
  : Wedge X Y -> Z.
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
X \/ Y -> Z
Proof.
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
X \/ Y -> Z
  snrapply Pushout_rec.
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
X -> Z
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
Y -> Z
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
forall a : Unit,
?pushb (unit_name pt a) = ?pushc (unit_name pt a)
  -
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
X -> Z exact f.
  -
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
Y -> Z exact g.
  -
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
forall a : Unit,
f (unit_name pt a) = g (unit_name pt a) intro.
X, Y: pType
Z: Type
f: X -> Z
g: Y -> Z
w: f pt = g pt
a: Unit
f (unit_name pt a) = g (unit_name pt a)
    exact w.
Defined.

Definition wedge_rec {X Y : pType} {Z : pType} (f : X $-> Z) (g : Y $-> Z)
  : X \/ Y $-> Z.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
X \/ Y $-> Z
Proof.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
X \/ Y $-> Z
  snrapply Build_pMap.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
X \/ Y -> Z
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
?Goal pt = pt
  -
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
X \/ Y -> Z snrapply (wedge_rec' f g).
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
f pt = g pt
    exact (point_eq f @ (point_eq g)^).
  -
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
wedge_rec' f g (point_eq f @ (point_eq g)^) pt = pt exact (point_eq f).
Defined.

Definition wedge_rec_beta_wglue {X Y Z : pType} (f : X $-> Z) (g : Y $-> Z)
  : ap (wedge_rec f g) wglue = point_eq f @ (point_eq g)^
  := Pushout_rec_beta_pglue _ f g _ tt.

Definition wedge_pr1 {X Y : pType} : X \/ Y $-> X
  := wedge_rec pmap_idmap pconst.

Definition wedge_pr2 {X Y : pType} : X \/ Y $-> Y
  := wedge_rec pconst pmap_idmap.

Definition wedge_incl (X Y : pType) : X \/ Y $-> X * Y
  := pprod_corec _ wedge_pr1 wedge_pr2.

Definition wedge_incl_beta_wglue {X Y : pType}
  : ap (@wedge_incl X Y) wglue = 1.
X, Y: pType
ap (wedge_incl X Y) wglue = 1
Proof.
X, Y: pType
ap (wedge_incl X Y) wglue = 1
  lhs_V nrapply eta_path_prod.
X, Y: pType
path_prod (wedge_incl X Y (pushl pt))
  (wedge_incl X Y (pushr pt))
  (ap fst (ap (wedge_incl X Y) wglue))
  (ap snd (ap (wedge_incl X Y) wglue)) = 1
  lhs nrapply ap011.
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = ?Goal0
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = ?Goal
X, Y: pType
path_prod (wedge_incl X Y (pushl pt))
  (wedge_incl X Y (pushr pt)) ?Goal ?Goal0 = 1
  -
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = ?Goal0 lhs_V nrapply ap_compose.
X, Y: pType
ap
  (fun x : Pushout (unit_name pt) (unit_name pt) =>
   snd (wedge_incl X Y x)) wglue = ?Goal0
    nrapply wedge_rec_beta_wglue.
  -
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = ?Goal lhs_V nrapply ap_compose.
X, Y: pType
ap
  (fun x : Pushout (unit_name pt) (unit_name pt) =>
   fst (wedge_incl X Y x)) wglue = ?Goal
    nrapply wedge_rec_beta_wglue.
  -
X, Y: pType
path_prod (wedge_incl X Y (pushl pt))
  (wedge_incl X Y (pushr pt))
  (point_eq pmap_idmap @ (point_eq pconst)^)
  (point_eq pconst @ (point_eq pmap_idmap)^) = 1 reflexivity.
Defined.

(** 1-universal property of wedge. *)
Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
  : f $o wedge_inl $== g $o wedge_inl
  -> f $o wedge_inr $== g $o wedge_inr
  -> f $== g.
X, Y, Z: pType
f, g: X \/ Y $-> Z
f $o wedge_inl $== g $o wedge_inl ->
f $o wedge_inr $== g $o wedge_inr -> f $== g
Proof.
X, Y, Z: pType
f, g: X \/ Y $-> Z
f $o wedge_inl $== g $o wedge_inl ->
f $o wedge_inr $== g $o wedge_inr -> f $== g
  intros p q.
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
f $== g
  snrapply Build_pHomotopy.
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
f == g
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
?p pt = dpoint_eq f @ (dpoint_eq g)^
  -
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
f == g snrapply (Pushout_ind _ p q).
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
forall a : Unit,
transport
  (fun w : Pushout (unit_name pt) (unit_name pt) =>
   f w = g w) (pglue a) (p (unit_name pt a)) =
q (unit_name pt a)
    intros [].
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
transport
  (fun w : Pushout (unit_name pt) (unit_name pt) =>
   f w = g w) (pglue tt) (p pt) = q pt
    nrapply transport_paths_FlFr'.
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
ap f (pglue tt) @ q pt = p pt @ ap g (pglue tt)
    lhs nrapply (whiskerL _ (dpoint_eq q)).
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
ap f (pglue tt) @
dpoint
  (pfam_phomotopy (f $o wedge_inr) (g $o wedge_inr)) =
p pt @ ap g (pglue tt)
    rhs nrapply (whiskerR (dpoint_eq p)).
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
ap f (pglue tt) @
dpoint
  (pfam_phomotopy (f $o wedge_inr) (g $o wedge_inr)) =
dpoint
  (pfam_phomotopy (f $o wedge_inl) (g $o wedge_inl)) @
ap g (pglue tt)
    clear p q.
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt) @
dpoint
  (pfam_phomotopy (f $o wedge_inr) (g $o wedge_inr)) =
dpoint
  (pfam_phomotopy (f $o wedge_inl) (g $o wedge_inl)) @
ap g (pglue tt)
    lhs nrapply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(ap f (pglue tt) @ dpoint_eq (f $o wedge_inr)) @
(dpoint_eq (g $o wedge_inr))^ =
dpoint
  (pfam_phomotopy (f $o wedge_inl) (g $o wedge_inl)) @
ap g (pglue tt)
    simpl.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(ap f (pglue tt) @ (ap f (pglue tt)^ @ point_eq f)) @
(ap g (pglue tt)^ @ point_eq g)^ =
((1 @ point_eq f) @ (1 @ point_eq g)^) @
ap g (pglue tt)
    apply moveR_pV.
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt) @ (ap f (pglue tt)^ @ point_eq f) =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    lhs nrapply whiskerL.
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt)^ @ point_eq f = ?Goal
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt) @ ?Goal =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    {
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt)^ @ point_eq f = ?Goal nrapply whiskerR.
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt)^ = ?Goal0
      apply ap_V. }
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt) @ ((ap f (pglue tt))^ @ point_eq f) =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    lhs nrapply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(ap f (pglue tt) @ (ap f (pglue tt))^) @ point_eq f =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    lhs nrapply whiskerR.
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap f (pglue tt) @ (ap f (pglue tt))^ = ?Goal
X, Y, Z: pType
f, g: X \/ Y $-> Z
?Goal @ point_eq f =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    1: apply concat_pV.
X, Y, Z: pType
f, g: X \/ Y $-> Z
1 @ point_eq f =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt)^ @ point_eq g)
    rhs nrapply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y $-> Z
1 @ point_eq f =
((((1 @ point_eq f) @ (1 @ point_eq g)^) @
  ap g (pglue tt)) @ ap g (pglue tt)^) @ point_eq g
    apply moveL_pM.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ (point_eq g)^ =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ap g (pglue tt)^
    lhs_V nrapply concat_p1.
X, Y, Z: pType
f, g: X \/ Y $-> Z
((1 @ point_eq f) @ (point_eq g)^) @ 1 =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ap g (pglue tt)^
    lhs nrapply concat_pp_p.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ ((point_eq g)^ @ 1) =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ap g (pglue tt)^
    lhs_V nrapply whiskerL.
X, Y, Z: pType
f, g: X \/ Y $-> Z
?Goal = (point_eq g)^ @ 1
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ ?Goal =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ap g (pglue tt)^
    1: apply (inv_pp 1).
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ (1 @ point_eq g)^ =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ap g (pglue tt)^
    rhs nrapply whiskerL.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ (1 @ point_eq g)^ =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ ?Goal
X, Y, Z: pType
f, g: X \/ Y $-> Z
ap g (pglue tt)^ = ?Goal
    2: apply ap_V.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ (1 @ point_eq g)^ =
(((1 @ point_eq f) @ (1 @ point_eq g)^) @
 ap g (pglue tt)) @ (ap g (pglue tt))^
    apply moveL_pV.
X, Y, Z: pType
f, g: X \/ Y $-> Z
((1 @ point_eq f) @ (1 @ point_eq g)^) @
ap g (pglue tt) =
((1 @ point_eq f) @ (1 @ point_eq g)^) @
ap g (pglue tt)
    reflexivity.
  -
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
Pushout_ind
  (fun w : Pushout (unit_name pt) (unit_name pt) =>
   f w = g w) p q
  (fun a : Unit =>
   match
     a as u
     return
       (transport
          (fun
             w : Pushout (unit_name pt) (unit_name pt)
           => f w = g w) (pglue u) (p pt) = q pt)
   with
   | tt =>
       transport_paths_FlFr' (pglue tt) (p pt) (q pt)
         (whiskerL (ap f (pglue tt)) (dpoint_eq q) @
          ((concat_p_pp (ap f (pglue tt))
              (dpoint_eq (f $o wedge_inr))
              (dpoint_eq (g $o wedge_inr))^ @
            (moveR_pV (ap g (pglue tt)^ @ point_eq g)
               (((1 @ point_eq f) @ (1 @ point_eq g)^) @
                ap g (pglue tt))
               (ap f (pglue tt) @
                (ap f (pglue tt)^ @ point_eq f))
               (whiskerL (ap f (pglue tt))
                  (whiskerR (ap_V f (pglue tt))
                     (point_eq f)) @
                (concat_p_pp (ap f (pglue tt))
                   (ap f (pglue tt))^ (point_eq f) @
                 (whiskerR (concat_pV (ap f ...))
                    (point_eq f) @
                  (moveL_pM (point_eq g) (1 @ ...)
                     (... @ ...) (...^ @ ...) @
                   (concat_p_pp (...) (...) (...))^))))
             :
             (ap f (pglue tt) @
              dpoint_eq (f $o wedge_inr)) @
             (dpoint_eq (g $o wedge_inr))^ =
             dpoint
               (pfam_phomotopy (f $o wedge_inl)
                  (g $o wedge_inl)) @ ap g (pglue tt))) @
           (whiskerR (dpoint_eq p) (ap g (pglue tt)))^))
   end) pt = dpoint_eq f @ (dpoint_eq g)^ simpl; pelim p q.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq f) @ (1 @ point_eq g)^ =
dpoint_eq f @ (dpoint_eq g)^
    f_ap.
X, Y, Z: pType
f, g: X \/ Y $-> Z
1 @ point_eq f = dpoint_eq f
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq g)^ = (dpoint_eq g)^
    1: apply concat_1p.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(1 @ point_eq g)^ = (dpoint_eq g)^
    lhs nrapply inv_pp.
X, Y, Z: pType
f, g: X \/ Y $-> Z
(point_eq g)^ @ 1^ = (dpoint_eq g)^
    apply concat_p1.
Defined.

Global Instance hasbinarycoproducts : HasBinaryCoproducts pType.
HasBinaryCoproducts pType
Proof.
HasBinaryCoproducts pType
  intros X Y.
X, Y: pType
BinaryCoproduct X Y
  snrapply Build_BinaryCoproduct.
X, Y: pType
pType
X, Y: pType
X $-> ?cat_coprod
X, Y: pType
Y $-> ?cat_coprod
X, Y: pType
forall z : pType,
(X $-> z) -> (Y $-> z) -> ?cat_coprod $-> z
X, Y: pType
forall (z : pType) (f : X $-> z) (g : Y $-> z),
?cat_coprod_rec z f g $o ?cat_inl $== f
X, Y: pType
forall (z : pType) (f : X $-> z) (g : Y $-> z),
?cat_coprod_rec z f g $o ?cat_inr $== g
X, Y: pType
forall (z : pType) (f g : ?cat_coprod $-> z),
f $o ?cat_inl $== g $o ?cat_inl ->
f $o ?cat_inr $== g $o ?cat_inr -> f $== g
  -
X, Y: pType
pType exact (X \/ Y).
  -
X, Y: pType
X $-> X \/ Y exact wedge_inl.
  -
X, Y: pType
Y $-> X \/ Y exact wedge_inr.
  -
X, Y: pType
forall z : pType,
(X $-> z) -> (Y $-> z) -> X \/ Y $-> z intros Z f g.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
X \/ Y $-> Z
    by apply wedge_rec.
  -
X, Y: pType
forall (z : pType) (f : X $-> z) (g : Y $-> z),
(fun (Z : pType) (f0 : X $-> Z) (g0 : Y $-> Z) =>
 wedge_rec f0 g0) z f g $o wedge_inl $== f intros Z f g.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
 wedge_rec f g) Z f g $o wedge_inl $== f
    snrapply Build_pHomotopy.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
 wedge_rec f g) Z f g $o wedge_inl == f
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
?p pt =
dpoint_eq
  ((fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
    wedge_rec f g) Z f g $o wedge_inl) @
(dpoint_eq f)^
    1: reflexivity.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun x0 : X => 1) pt =
dpoint_eq
  ((fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
    wedge_rec f g) Z f g $o wedge_inl) @
(dpoint_eq f)^
    by simpl; pelim f.
  -
X, Y: pType
forall (z : pType) (f : X $-> z) (g : Y $-> z),
(fun (Z : pType) (f0 : X $-> Z) (g0 : Y $-> Z) =>
 wedge_rec f0 g0) z f g $o wedge_inr $== g intros Z f g.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
 wedge_rec f g) Z f g $o wedge_inr $== g
    snrapply Build_pHomotopy.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
 wedge_rec f g) Z f g $o wedge_inr == g
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
?p pt =
dpoint_eq
  ((fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
    wedge_rec f g) Z f g $o wedge_inr) @
(dpoint_eq g)^
    1: reflexivity.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(fun x0 : Y => 1) pt =
dpoint_eq
  ((fun (Z : pType) (f : X $-> Z) (g : Y $-> Z) =>
    wedge_rec f g) Z f g $o wedge_inr) @
(dpoint_eq g)^
    simpl.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
1 =
(ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
   (pglue tt)^ @ point_eq f) @ (dpoint_eq g)^
    apply moveL_pV.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
1 @ dpoint_eq g =
ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
  (pglue tt)^ @ point_eq f
    apply moveL_pM.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(1 @ dpoint_eq g) @ (point_eq f)^ =
ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
  (pglue tt)^
    refine (_ @ (ap_V _ (pglue tt))^).
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(1 @ dpoint_eq g) @ (point_eq f)^ =
(ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
   (pglue tt))^
    apply moveR_Mp.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(point_eq f)^ =
(1 @ dpoint_eq g)^ @
(ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
   (pglue tt))^
    apply moveL_pV.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
(point_eq f)^ @
ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
  (pglue tt) = (1 @ dpoint_eq g)^
    apply moveR_Vp.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
ap (wedge_rec' f g (point_eq f @ (point_eq g)^))
  (pglue tt) = point_eq f @ (1 @ dpoint_eq g)^
    refine (Pushout_rec_beta_pglue _ f g _ _  @ _).
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
point_eq f @ (point_eq g)^ =
point_eq f @ (1 @ dpoint_eq g)^
    simpl.
X, Y, Z: pType
f: X $-> Z
g: Y $-> Z
point_eq f @ (point_eq g)^ =
point_eq f @ (1 @ dpoint_eq g)^
    by pelim f g.
  -
X, Y: pType
forall (z : pType) (f g : X \/ Y $-> z),
f $o wedge_inl $== g $o wedge_inl ->
f $o wedge_inr $== g $o wedge_inr -> f $== g intros Z f g p q.
X, Y, Z: pType
f, g: X \/ Y $-> Z
p: f $o wedge_inl $== g $o wedge_inl
q: f $o wedge_inr $== g $o wedge_inr
f $== g
    by apply wedge_up.
Defined.

(** *** Lemmas about wedge functions *)

Lemma wedge_pr1_inl {X Y} : wedge_pr1 $o (@wedge_inl X Y) $== pmap_idmap.
X, Y: pType
wedge_pr1 $o wedge_inl $== pmap_idmap
Proof.
X, Y: pType
wedge_pr1 $o wedge_inl $== pmap_idmap
  reflexivity.
Defined.

Lemma wedge_pr1_inr {X Y} : wedge_pr1 $o (@wedge_inr X Y) $== pconst.
X, Y: pType
wedge_pr1 $o wedge_inr $== pconst
Proof.
X, Y: pType
wedge_pr1 $o wedge_inr $== pconst
  snrapply Build_pHomotopy.
X, Y: pType
wedge_pr1 $o wedge_inr == pconst
X, Y: pType
?p pt =
dpoint_eq (wedge_pr1 $o wedge_inr) @
(dpoint_eq pconst)^
  1: reflexivity.
X, Y: pType
(fun x0 : Y => 1) pt =
dpoint_eq (wedge_pr1 $o wedge_inr) @
(dpoint_eq pconst)^
  rhs nrapply concat_p1.
X, Y: pType
1 = dpoint_eq (wedge_pr1 $o wedge_inr)
  rhs nrapply concat_p1.
X, Y: pType
1 = ap wedge_pr1 (point_eq wedge_inr)
  rhs nrapply (ap_V _ wglue).
X, Y: pType
1 = (ap wedge_pr1 wglue)^
  exact (inverse2 (wedge_rec_beta_wglue pmap_idmap pconst)^).
Defined.

Lemma wedge_pr2_inl {X Y} : wedge_pr2 $o (@wedge_inl X Y) $== pconst.
X, Y: pType
wedge_pr2 $o wedge_inl $== pconst
Proof.
X, Y: pType
wedge_pr2 $o wedge_inl $== pconst
  reflexivity.
Defined.

Lemma wedge_pr2_inr {X Y} : wedge_pr2 $o (@wedge_inr X Y) $== pmap_idmap.
X, Y: pType
wedge_pr2 $o wedge_inr $== pmap_idmap
Proof.
X, Y: pType
wedge_pr2 $o wedge_inr $== pmap_idmap
  snrapply Build_pHomotopy.
X, Y: pType
wedge_pr2 $o wedge_inr == pmap_idmap
X, Y: pType
?p pt =
dpoint_eq (wedge_pr2 $o wedge_inr) @
(dpoint_eq pmap_idmap)^
  1: reflexivity.
X, Y: pType
(fun x0 : Y => 1) pt =
dpoint_eq (wedge_pr2 $o wedge_inr) @
(dpoint_eq pmap_idmap)^
  rhs nrapply concat_p1.
X, Y: pType
1 = dpoint_eq (wedge_pr2 $o wedge_inr)
  rhs nrapply concat_p1.
X, Y: pType
1 = ap wedge_pr2 (point_eq wedge_inr)
  rhs nrapply (ap_V _ wglue).
X, Y: pType
1 = (ap wedge_pr2 wglue)^
  exact (inverse2 (wedge_rec_beta_wglue pconst pmap_idmap)^).
Defined.

(** Wedge of an indexed family of pointed types *)

(** Note that the index type is not necessarily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *)
Definition FamilyWedge (I : Type) (X : I -> pType) : pType.
I: Type
X: I -> pType
pType
Proof.
I: Type
X: I -> pType
pType
  snrapply Build_pType.
I: Type
X: I -> pType
Type
I: Type
X: I -> pType
IsPointed ?pointed_type
  -
I: Type
X: I -> pType
Type srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _).
I: Type
X: I -> pType
I -> {x : I & X x}
I: Type
X: I -> pType
I -> pUnit
    +
I: Type
X: I -> pType
I -> {x : I & X x} exact (fun i => (i; pt)).
    +
I: Type
X: I -> pType
I -> pUnit exact (fun _ => pt).
  -
I: Type
X: I -> pType
IsPointed
  (Pushout (fun i : I => (i; pt)) (fun _ : I => pt)) apply pushr.
I: Type
X: I -> pType
pUnit
    exact pt.
Defined.

Definition fwedge_in' (I : Type) (X : I -> pType)
  : forall i, X i $-> FamilyWedge I X
  := fun i => Build_pMap _ _ (fun x => pushl (i; x)) (pglue i).

(** We have an inclusion map [pushl : sig X -> FamilyWedge X].  When [I] is pointed, so is [sig X], and then this inclusion map is pointed. *)
Definition fwedge_in (I : pType) (X : I -> pType)
  : psigma (pointed_fam X) $-> FamilyWedge I X
  := Build_pMap _ _ pushl (pglue pt).

(** Recursion principle for the wedge of an indexed family of pointed types. *)
Definition fwedge_rec (I : Type) (X : I -> pType) (Z : pType)
  (f : forall i, X i $-> Z)
  : FamilyWedge I X $-> Z.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
FamilyWedge I X $-> Z
Proof.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
FamilyWedge I X $-> Z
  snrapply Build_pMap.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
FamilyWedge I X -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
?Goal pt = pt
  -
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
FamilyWedge I X -> Z snrapply Pushout_rec.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
{x : I & X x} -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
pUnit -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
forall a : I,
?pushb ((fun i : I => (i; pt)) a) =
?pushc ((fun _ : I => pt) a)
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
{x : I & X x} -> Z apply (sig_rec _ _ _ f).
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
pUnit -> Z exact pconst.
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
forall a : I,
sig_rec I (fun i : I => X i) Z (fun i : I => f i)
  ((fun i : I => (i; pt)) a) =
pconst ((fun _ : I => pt) a) intros i.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
sig_rec I (fun i : I => X i) Z (fun i : I => f i)
  ((fun i : I => (i; pt)) i) =
pconst ((fun _ : I => pt) i)
      exact (point_eq (f i)).
  -
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
Pushout_rec Z
  (sig_rec I (fun i : I => X i) Z (fun i : I => f i))
  pconst (fun i : I => point_eq (f i)) pt = pt exact idpath.
Defined.

(** We specify a universe variable here to prevent minimization to [Set]. *)
Global Instance hasallcoproducts_ptype : HasAllCoproducts pType@{u}.
HasAllCoproducts pType
Proof.
HasAllCoproducts pType
  intros I X.
I: Type
X: I -> pType
Coproduct I X
  snrapply Build_Coproduct.
I: Type
X: I -> pType
pType
I: Type
X: I -> pType
forall i : I, X i $-> ?cat_coprod
I: Type
X: I -> pType
forall z : pType,
(forall i : I, X i $-> z) -> ?cat_coprod $-> z
I: Type
X: I -> pType
forall (z : pType) (f : forall i : I, X i $-> z)
(i : I), ?cat_coprod_rec z f $o ?cat_in i $== f i
I: Type
X: I -> pType
forall (z : pType) (f g : ?cat_coprod $-> z),
(forall i : I, f $o ?cat_in i $== g $o ?cat_in i) ->
f $== g
  -
I: Type
X: I -> pType
pType exact (FamilyWedge I X).
  -
I: Type
X: I -> pType
forall i : I, X i $-> FamilyWedge I X exact (fwedge_in' I X).
  -
I: Type
X: I -> pType
forall z : pType,
(forall i : I, X i $-> z) -> FamilyWedge I X $-> z exact (fwedge_rec I X).
  -
I: Type
X: I -> pType
forall (z : pType) (f : forall i : I, X i $-> z)
(i : I),
fwedge_rec I X z f $o fwedge_in' I X i $== f i intros Z f i.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
fwedge_rec I X Z f $o fwedge_in' I X i $== f i
    snrapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
fwedge_rec I X Z f $o fwedge_in' I X i == f i
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
?p pt =
dpoint_eq (fwedge_rec I X Z f $o fwedge_in' I X i) @
(dpoint_eq (f i))^
    1: reflexivity.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
(fun x0 : X i => 1) pt =
dpoint_eq (fwedge_rec I X Z f $o fwedge_in' I X i) @
(dpoint_eq (f i))^
    simpl.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
1 =
(ap
   (Pushout_rec Z
      (sig_rec I (fun i : I => X i) Z
         (fun i : I => f i)) (unit_name pt)
      (fun i : I => point_eq (f i))) (pglue i) @ 1) @
(dpoint_eq (f i))^
    apply moveL_pV.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
1 @ dpoint_eq (f i) =
ap
  (Pushout_rec Z
     (sig_rec I (fun i : I => X i) Z
        (fun i : I => f i)) (unit_name pt)
     (fun i : I => point_eq (f i))) (pglue i) @ 1
    apply equiv_1p_q1.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
dpoint_eq (f i) =
ap
  (Pushout_rec Z
     (sig_rec I (fun i : I => X i) Z
        (fun i : I => f i)) (unit_name pt)
     (fun i : I => point_eq (f i))) (pglue i)
    symmetry.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i $-> Z
i: I
ap
  (Pushout_rec Z
     (sig_rec I (fun i : I => X i) Z
        (fun i : I => f i)) (unit_name pt)
     (fun i : I => point_eq (f i))) (pglue i) =
dpoint_eq (f i)
    exact (Pushout_rec_beta_pglue Z _ (unit_name pt) (fun i => point_eq (f i)) _).
  -
I: Type
X: I -> pType
forall (z : pType) (f g : FamilyWedge I X $-> z),
(forall i : I,
 f $o fwedge_in' I X i $== g $o fwedge_in' I X i) ->
f $== g intros Z f g h.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
f $== g
    snrapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
f == g
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
?p pt = dpoint_eq f @ (dpoint_eq g)^
    +
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
f == g snrapply Pushout_ind.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall b : {x : I & X x},
(fun
   w : Pushout (fun i : I => (i; pt))
         (fun _ : I => pt) => f w = g w) (pushl b)
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall c : pUnit,
(fun
   w : Pushout (fun i : I => (i; pt))
         (fun _ : I => pt) => f w = g w) (pushr c)
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall a : I,
transport
  (fun
     w : Pushout (fun i : I => (i; pt))
           (fun _ : I => pt) => f w = g w) (pglue a)
  (?pushb ((fun i : I => (i; pt)) a)) =
?pushc ((fun _ : I => pt) a)
      *
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall b : {x : I & X x},
(fun
   w : Pushout (fun i : I => (i; pt))
         (fun _ : I => pt) => f w = g w) (pushl b) intros [i x].
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
x: X i
f (pushl (i; x)) = g (pushl (i; x))
        nrapply h.
      *
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall c : pUnit,
(fun
   w : Pushout (fun i : I => (i; pt))
         (fun _ : I => pt) => f w = g w) (pushr c) intros [].
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
f (pushr tt) = g (pushr tt)
        exact (point_eq _ @ (point_eq _)^).
      *
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
forall a : I,
transport
  (fun
     w : Pushout (fun i : I => (i; pt))
           (fun _ : I => pt) => f w = g w) (pglue a)
  ((fun b : {x : I & X x} =>
    (fun (i : I) (x : X i) => h i x) b.1 b.2)
     ((fun i : I => (i; pt)) a)) =
(fun c : pUnit =>
 match c as u return (f (pushr u) = g (pushr u)) with
 | tt => point_eq f @ (point_eq g)^
 end) ((fun _ : I => pt) a) intros i; cbn.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
transport
  (fun
     w : Pushout (fun i : I => (i; pt))
           (fun _ : I => pt) => f w = g w) (pglue i)
  (h i pt) = point_eq f @ (point_eq g)^
        nrapply transport_paths_FlFr'.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
ap f (pglue i) @ (point_eq f @ (point_eq g)^) =
h i pt @ ap g (pglue i)
        lhs nrapply concat_p_pp.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
(ap f (pglue i) @ point_eq f) @ (point_eq g)^ =
h i pt @ ap g (pglue i)
        apply moveR_pV.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
ap f (pglue i) @ point_eq f =
(h i pt @ ap g (pglue i)) @ point_eq g
        rhs nrapply concat_pp_p.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
ap f (pglue i) @ point_eq f =
h i pt @ (ap g (pglue i) @ point_eq g)
        apply moveL_pM.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
(ap f (pglue i) @ point_eq f) @
(ap g (pglue i) @ point_eq g)^ = h i pt
        symmetry.
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
i: I
h i pt =
(ap f (pglue i) @ point_eq f) @
(ap g (pglue i) @ point_eq g)^
        exact (dpoint_eq (h i)).
    +
I: Type
X: I -> pType
Z: pType
f, g: FamilyWedge I X $-> Z
h: forall i : I,
f $o fwedge_in' I X i $== g $o fwedge_in' I X i
Pushout_ind
  (fun
     w : Pushout (fun i : I => (i; pt))
           (fun _ : I => pt) => f w = g w)
  (fun b : {x : I & X x} =>
   (fun (i : I) (x : X i) => h i x) b.1 b.2)
  (fun c : pUnit =>
   match
     c as u return (f (pushr u) = g (pushr u))
   with
   | tt => point_eq f @ (point_eq g)^
   end)
  (fun i : I =>
   transport_paths_FlFr' (pglue i) (h i pt)
     (point_eq f @ (point_eq g)^)
     (concat_p_pp (ap f (pglue i)) (point_eq f)
        (point_eq g)^ @
      moveR_pV (point_eq g) (h i pt @ ap g (pglue i))
        (ap f (pglue i) @ point_eq f)
        (moveL_pM (ap g (pglue i) @ point_eq g)
           (ap f (pglue i) @ point_eq f) (h i pt)
           (dpoint_eq (h i))^ @
         (concat_pp_p (h i pt) (ap g (pglue i))
            (point_eq g))^))
   :
   transport
     (fun
        w : Pushout (fun i0 : I => (i0; pt))
              (fun _ : I => pt) => f w = g w)
     (pglue i)
     ((fun b : {x : I & X x} =>
       (fun (i0 : I) (x : X i0) => h i0 x) b.1 b.2)
        ((fun i0 : I => (i0; pt)) i)) =
   (fun c : pUnit =>
    match
      c as u return (f (pushr u) = g (pushr u))
    with
    | tt => point_eq f @ (point_eq g)^
    end) ((fun _ : I => pt) i)) pt =
dpoint_eq f @ (dpoint_eq g)^ reflexivity.
Defined.

(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge summand should land in. *)
Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I -> pType)
  : FamilyWedge I X $-> pproduct X
  := cat_coprod_prod X.

(** ** The pinch map on the suspension *)

(** Given a suspension, there is a natural map from the suspension to the wedge of the suspension with itself. This is known as the pinch map.

This is the image to keep in mind:
<<
                                    *
                                   /|\
                                  / | \
    Susp X                       /  |  \
                                /   |   \
       *                       * merid(x)*
      /|\                       \   |   /
     / | \                       \  |  /
    /  |  \                       \ | /
   /   |   \      Pinch            \|/
  * merid(x)*   ---------->         *
   \   |   /                       /|\
    \  |  /                       / | \
     \ | /                       /  |  \
      \|/                       /   |   \
       *                       * merid(x)*
                                \   |   /
                                 \  |  /
                                  \ | /
                                   \|/
                                    *
>>

Note that this is only a conceptual picture as we aren't working with "reduced suspensions". This means we have to track back along [merid pt] making this map a little trickier to imagine. *)

(** The pinch map for a suspension. *)
Definition psusp_pinch (X : pType) : psusp X $-> psusp X \/ psusp X.
X: pType
psusp X $-> psusp X \/ psusp X
Proof.
X: pType
psusp X $-> psusp X \/ psusp X
  refine (Build_pMap _ _ (Susp_rec pt pt _) idpath).
X: pType
X -> pt = pt
  intros x.
X: pType
x: X
pt = pt
  refine (ap wedge_inl _ @ wglue @ ap wedge_inr _ @ wglue^).
X: pType
x: X
pt = pt
X: pType
x: X
pt = pt
  1,2: exact (loop_susp_unit X x).
Defined.

(** It should compute when [ap]ed on a merid. *)
Definition psusp_pinch_beta_merid {X : pType} (x : X)
  : ap (psusp_pinch X) (merid x)
    = ap wedge_inl (loop_susp_unit X x) @ wglue
    @ ap wedge_inr (loop_susp_unit X x) @ wglue^.
X: pType
x: X
ap (psusp_pinch X) (merid x) =
((ap wedge_inl (loop_susp_unit X x) @ wglue) @
 ap wedge_inr (loop_susp_unit X x)) @ wglue^
Proof.
X: pType
x: X
ap (psusp_pinch X) (merid x) =
((ap wedge_inl (loop_susp_unit X x) @ wglue) @
 ap wedge_inr (loop_susp_unit X x)) @ wglue^
  rapply Susp_rec_beta_merid.
Defined.

(** Doing wedge projections on the pinch map gives the identity. *)
Definition wedge_pr1_psusp_pinch {X}
  : wedge_pr1 $o psusp_pinch X $== Id (psusp X).
X: pType
wedge_pr1 $o psusp_pinch X $== Id (psusp X)
Proof.
X: pType
wedge_pr1 $o psusp_pinch X $== Id (psusp X)
  snrapply Build_pHomotopy.
X: pType
wedge_pr1 $o psusp_pinch X == Id (psusp X)
X: pType
?p pt =
dpoint_eq (wedge_pr1 $o psusp_pinch X) @
(dpoint_eq (Id (psusp X)))^
  -
X: pType
wedge_pr1 $o psusp_pinch X == Id (psusp X) snrapply Susp_ind_FlFr.
X: pType
(wedge_pr1 $o psusp_pinch X) North =
Id (psusp X) North
X: pType
(wedge_pr1 $o psusp_pinch X) South =
Id (psusp X) South
X: pType
forall x : X,
ap (wedge_pr1 $o psusp_pinch X) (merid x) @ ?HS =
?HN @ ap (Id (psusp X)) (merid x)
    +
X: pType
(wedge_pr1 $o psusp_pinch X) North =
Id (psusp X) North reflexivity.
    +
X: pType
(wedge_pr1 $o psusp_pinch X) South =
Id (psusp X) South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr1 $o psusp_pinch X) (merid x) @ merid pt =
1 @ ap (Id (psusp X)) (merid x) intros x.
X: pType
x: X
ap (wedge_pr1 $o psusp_pinch X) (merid x) @ merid pt =
1 @ ap (Id (psusp X)) (merid x)
      rhs nrapply concat_1p.
X: pType
x: X
ap (wedge_pr1 $o psusp_pinch X) (merid x) @ merid pt =
ap (Id (psusp X)) (merid x)
      rhs nrapply ap_idmap.
X: pType
x: X
ap (wedge_pr1 $o psusp_pinch X) (merid x) @ merid pt =
merid x
      apply moveR_pM.
X: pType
x: X
ap (wedge_pr1 $o psusp_pinch X) (merid x) =
merid x @ (merid pt)^
      change (?t = _) with (t = loop_susp_unit X x).
X: pType
x: X
ap (wedge_pr1 $o psusp_pinch X) (merid x) =
loop_susp_unit X x
      lhs nrapply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr1 (ap (psusp_pinch X) (merid x)) =
loop_susp_unit X x
      lhs nrapply (ap _ (psusp_pinch_beta_merid x)).
X: pType
x: X
ap wedge_pr1
  (((ap wedge_inl (loop_susp_unit X x) @ wglue) @
    ap wedge_inr (loop_susp_unit X x)) @ wglue^) =
loop_susp_unit X x
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
ap wedge_pr1 wglue^ = loop_susp_unit X x
      lhs nrapply (ap (fun x => _ @ x) (ap_V _ _)).
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
(ap wedge_pr1 wglue)^ = loop_susp_unit X x
      apply moveR_pV.
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ ap wedge_pr1 wglue
      rhs nrapply (whiskerL _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr1
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      lhs nrapply (ap (fun x => _ @ x)).
X: pType
x: X
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) =
?Goal
X: pType
x: X
ap wedge_pr1
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @ ?Goal =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      {
X: pType
x: X
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) =
?Goal lhs_V nrapply ap_compose.
X: pType
x: X
ap (fun x : psusp X => wedge_pr1 (pushr x))
  (loop_susp_unit X x) = ?Goal
        apply ap_const. }
X: pType
x: X
ap wedge_pr1
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @ 1 =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      lhs nrapply concat_p1.
X: pType
x: X
ap wedge_pr1
  (ap wedge_inl (loop_susp_unit X x) @ wglue) =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) @
ap wedge_pr1 wglue =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      lhs nrapply (ap (fun x => _ @ x) (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) @
(point_eq pmap_idmap @ (point_eq pconst)^) =
loop_susp_unit X x @
(point_eq pmap_idmap @ (point_eq pconst)^)
      f_ap.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) =
loop_susp_unit X x
      lhs_V nrapply (ap_compose wedge_inl).
X: pType
x: X
ap (fun x : psusp X => wedge_pr1 (wedge_inl x))
  (loop_susp_unit X x) = loop_susp_unit X x
      apply ap_idmap.
  -
X: pType
Susp_ind_FlFr (wedge_pr1 $o psusp_pinch X)
  (Id (psusp X)) 1 (merid pt)
  (fun x : X =>
   (moveR_pM (merid pt) (merid x)
      (ap (wedge_pr1 $o psusp_pinch X) (merid x))
      (ap_compose (psusp_pinch X) wedge_pr1 (merid x) @
       (ap (ap wedge_pr1) (psusp_pinch_beta_merid x) @
        (ap_pp wedge_pr1
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x)) wglue^ @
         (ap
            (fun
               x0 : wedge_pr1 (wedge_inr pt) =
                    wedge_pr1 (psusp_pinch X South) =>
             ap wedge_pr1
               ((ap wedge_inl (...) @ wglue) @
                ap wedge_inr (loop_susp_unit X x)) @
             x0) (ap_V wedge_pr1 wglue) @
          moveR_pV (ap wedge_pr1 wglue)
            (loop_susp_unit X x)
            (ap wedge_pr1
               ((ap wedge_inl (loop_susp_unit X x) @
                 wglue) @
                ap wedge_inr (loop_susp_unit X x)))
            ((ap_pp wedge_pr1
                (ap wedge_inl (loop_susp_unit X x) @
                 wglue)
                (ap wedge_inr (loop_susp_unit X x)) @
              (ap (fun ... => ... @ x0)
                 ((...)^ @ ap_const ... ...) @
               (concat_p1 (...) @ (... @ ...)))) @
             (whiskerL (loop_susp_unit X x)
                (wedge_rec_beta_wglue pmap_idmap
                   pconst))^))))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap (Id (psusp X)) (merid x)))^) pt =
dpoint_eq (wedge_pr1 $o psusp_pinch X) @
(dpoint_eq (Id (psusp X)))^ reflexivity.
Defined.

Definition wedge_pr2_psusp_pinch {X}
  : wedge_pr2 $o psusp_pinch X $== Id (psusp X).
X: pType
wedge_pr2 $o psusp_pinch X $== Id (psusp X)
Proof.
X: pType
wedge_pr2 $o psusp_pinch X $== Id (psusp X)
  snrapply Build_pHomotopy.
X: pType
wedge_pr2 $o psusp_pinch X == Id (psusp X)
X: pType
?p pt =
dpoint_eq (wedge_pr2 $o psusp_pinch X) @
(dpoint_eq (Id (psusp X)))^
  -
X: pType
wedge_pr2 $o psusp_pinch X == Id (psusp X) snrapply Susp_ind_FlFr.
X: pType
(wedge_pr2 $o psusp_pinch X) North =
Id (psusp X) North
X: pType
(wedge_pr2 $o psusp_pinch X) South =
Id (psusp X) South
X: pType
forall x : X,
ap (wedge_pr2 $o psusp_pinch X) (merid x) @ ?HS =
?HN @ ap (Id (psusp X)) (merid x)
    +
X: pType
(wedge_pr2 $o psusp_pinch X) North =
Id (psusp X) North reflexivity.
    +
X: pType
(wedge_pr2 $o psusp_pinch X) South =
Id (psusp X) South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr2 $o psusp_pinch X) (merid x) @ merid pt =
1 @ ap (Id (psusp X)) (merid x) intros x.
X: pType
x: X
ap (wedge_pr2 $o psusp_pinch X) (merid x) @ merid pt =
1 @ ap (Id (psusp X)) (merid x)
      rhs nrapply concat_1p.
X: pType
x: X
ap (wedge_pr2 $o psusp_pinch X) (merid x) @ merid pt =
ap (Id (psusp X)) (merid x)
      rhs nrapply ap_idmap.
X: pType
x: X
ap (wedge_pr2 $o psusp_pinch X) (merid x) @ merid pt =
merid x
      apply moveR_pM.
X: pType
x: X
ap (wedge_pr2 $o psusp_pinch X) (merid x) =
merid x @ (merid pt)^
      change (?t = _) with (t = loop_susp_unit X x).
X: pType
x: X
ap (wedge_pr2 $o psusp_pinch X) (merid x) =
loop_susp_unit X x
      lhs nrapply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr2 (ap (psusp_pinch X) (merid x)) =
loop_susp_unit X x
      lhs nrapply (ap _ (psusp_pinch_beta_merid x)).
X: pType
x: X
ap wedge_pr2
  (((ap wedge_inl (loop_susp_unit X x) @ wglue) @
    ap wedge_inr (loop_susp_unit X x)) @ wglue^) =
loop_susp_unit X x
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
ap wedge_pr2 wglue^ = loop_susp_unit X x
      lhs nrapply (ap (fun x => _ @ x) (ap_V _ _)).
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
(ap wedge_pr2 wglue)^ = loop_susp_unit X x
      apply moveR_pV.
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ ap wedge_pr2 wglue
      rhs nrapply (whiskerL _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @
(point_eq pconst @ (point_eq pmap_idmap)^)
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr2
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @
(point_eq pconst @ (point_eq pmap_idmap)^)
      lhs nrapply (ap (fun x => _ @ x) _).
X: pType
x: X
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) =
?Goal
X: pType
x: X
ap wedge_pr2
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @ ?Goal =
loop_susp_unit X x @
(point_eq pconst @ (point_eq pmap_idmap)^)
      {
X: pType
x: X
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) =
?Goal lhs_V nrapply ap_compose.
X: pType
x: X
ap (fun x : psusp X => wedge_pr2 (pushr x))
  (loop_susp_unit X x) = ?Goal
        apply ap_idmap. }
X: pType
x: X
ap wedge_pr2
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @
loop_susp_unit X x =
loop_susp_unit X x @
(point_eq pconst @ (point_eq pmap_idmap)^)
      rhs nrapply concat_p1.
X: pType
x: X
ap wedge_pr2
  (ap wedge_inl (loop_susp_unit X x) @ wglue) @
loop_susp_unit X x = loop_susp_unit X x
      apply moveR_pM.
X: pType
x: X
ap wedge_pr2
  (ap wedge_inl (loop_susp_unit X x) @ wglue) =
loop_susp_unit X x @ (loop_susp_unit X x)^
      lhs nrapply ap_pp.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @
ap wedge_pr2 wglue =
loop_susp_unit X x @ (loop_susp_unit X x)^
      rhs nrapply concat_pV.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @
ap wedge_pr2 wglue = 1
      lhs nrapply (ap _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @
(point_eq pconst @ (point_eq pmap_idmap)^) = 1
      apply moveR_pM.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) =
1 @ (point_eq pconst @ (point_eq pmap_idmap)^)^
      lhs_V nrapply (ap_compose wedge_inl).
X: pType
x: X
ap (fun x : psusp X => wedge_pr2 (wedge_inl x))
  (loop_susp_unit X x) =
1 @ (point_eq pconst @ (point_eq pmap_idmap)^)^
      rapply ap_const.
  -
X: pType
Susp_ind_FlFr (wedge_pr2 $o psusp_pinch X)
  (Id (psusp X)) 1 (merid pt)
  (fun x : X =>
   (moveR_pM (merid pt) (merid x)
      (ap (wedge_pr2 $o psusp_pinch X) (merid x))
      (ap_compose (psusp_pinch X) wedge_pr2 (merid x) @
       (ap (ap wedge_pr2) (psusp_pinch_beta_merid x) @
        (ap_pp wedge_pr2
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x)) wglue^ @
         (ap
            (fun
               x0 : wedge_pr2 (wedge_inr pt) =
                    wedge_pr2 (psusp_pinch X South) =>
             ap wedge_pr2
               ((ap wedge_inl (...) @ wglue) @
                ap wedge_inr (loop_susp_unit X x)) @
             x0) (ap_V wedge_pr2 wglue) @
          moveR_pV (ap wedge_pr2 wglue)
            (loop_susp_unit X x)
            (ap wedge_pr2
               ((ap wedge_inl (loop_susp_unit X x) @
                 wglue) @
                ap wedge_inr (loop_susp_unit X x)))
            ((ap_pp wedge_pr2
                (ap wedge_inl (loop_susp_unit X x) @
                 wglue)
                (ap wedge_inr (loop_susp_unit X x)) @
              (ap (fun ... => ... @ x0)
                 ((...)^ @ ap_idmap ...) @
               (moveR_pM (...) (...) (...) (...) @
                (concat_p1 ...)^))) @
             (whiskerL (loop_susp_unit X x)
                (wedge_rec_beta_wglue pconst
                   pmap_idmap))^))))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap (Id (psusp X)) (merid x)))^) pt =
dpoint_eq (wedge_pr2 $o psusp_pinch X) @
(dpoint_eq (Id (psusp X)))^ reflexivity.
Defined.