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.Coproducts WildCat.Products.
Require Import Homotopy.Suspension.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Extensions Modalities.ReflectiveSubuniverse.

(** * Wedge sums *)

Local Open Scope pointed_scope.

Definition Wedge@{i j k | i <= k, j <= k} (X : pType@{i}) (Y : pType@{j}) : pType@{k}
  := [Pushout@{Set i j k} (fun _ : Unit => point X) (fun _ => point Y), pushl (point X)].

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

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

Definition wedge_inl {X Y : pType} : X ->* X \/ Y
  := Build_pMap pushl 1.

Definition wedge_inr {X Y : pType} : Y ->* X \/ Y
  := Build_pMap pushr wglue^.

(** 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
  := Pushout_rec Z f g (fun _ => w).

Definition wedge_rec {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : X \/ Y ->* Z
  := Build_pMap (wedge_rec' f g (point_eq f @ (point_eq g)^)) (point_eq f).

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_rec_beta_inl {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : wedge_rec f g o* wedge_inl ==* f.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl ==* f
Proof.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl ==* f
  snapply Build_pHomotopy.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl == f
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
?p pt =
dpoint_eq (wedge_rec 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 (wedge_rec f g o* wedge_inl) @
(dpoint_eq f)^
  cbn beta; symmetry.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
dpoint_eq (wedge_rec f g o* wedge_inl) @
(dpoint_eq f)^ = 1
  exact (concat_pp_V 1 (point_eq f)).
Defined.

Definition wedge_rec_beta_inr {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : wedge_rec f g o* wedge_inr ==* g.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr ==* g
Proof.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr ==* g
  snapply Build_pHomotopy.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr == g
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
?p pt =
dpoint_eq (wedge_rec 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 (wedge_rec f g o* wedge_inr) @
(dpoint_eq g)^
  cbn -[wedge_rec].
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 =
(ap (wedge_rec f g) wglue^ @ point_eq (wedge_rec f g)) @
(dpoint_eq g)^
  rhs napply concat_pp_p.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 =
ap (wedge_rec f g) wglue^ @
(point_eq (wedge_rec f g) @ (dpoint_eq g)^)
  rhs napply (ap_V _ _ @@ 1).
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 =
(ap (wedge_rec f g) wglue)^ @
(point_eq (wedge_rec f g) @ (dpoint_eq g)^)
  apply moveL_Vp.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
ap (wedge_rec f g) wglue @ 1 =
point_eq (wedge_rec f g) @ (dpoint_eq g)^
  lhs napply concat_p1.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
ap (wedge_rec f g) wglue =
point_eq (wedge_rec f g) @ (dpoint_eq g)^
  napply wedge_rec_beta_wglue.
Defined.

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 napply 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
  napply (ap011 _ (x':=1) (y':=1)).
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = 1
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = 1
  -
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = 1 lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
X, Y: pType
ap (fun x : X \/ Y => fst (wedge_incl X Y x)) wglue =
1
    napply wedge_rec_beta_wglue.
  -
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = 1 lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
X, Y: pType
ap (fun x : X \/ Y => snd (wedge_incl X Y x)) wglue =
1
    napply wedge_rec_beta_wglue.
Defined.

Definition wedge_ind {X Y : pType} (P : X \/ Y -> Type)
  (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y))
  (w : wglue # f pt = g pt)
  : forall xy, P xy.
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall xy : X \/ Y, P xy
Proof.
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall xy : X \/ Y, P xy
  napply (Pushout_ind P f g).
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall a : Unit, transport P (pglue a) (f pt) = g pt
  intros [].
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
transport P (pglue tt) (f pt) = g pt
  exact w.
Defined.

Definition wedge_ind_beta_wglue {X Y : pType} (P : X \/ Y -> Type)
  (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y))
  (w : wglue # f pt = g pt)
  : apD (wedge_ind P f g w) wglue = w
  := Pushout_ind_beta_pglue P _ _ _ _.

Definition wedge_ind_FlFr {X Y Z : pType} {f g : X \/ Y -> Z}
  (l : f o wedge_inl == g o wedge_inl)
  (r : f o wedge_inr == g o wedge_inr)
  (w : ap f wglue @ r pt = l pt @ ap g wglue)
  : f == g.
X, Y, Z: pType
f, g: X \/ Y -> Z
l: f o wedge_inl == g o wedge_inl
r: f o wedge_inr == g o wedge_inr
w: ap f wglue @ r pt = l pt @ ap g wglue
f == g
Proof.
X, Y, Z: pType
f, g: X \/ Y -> Z
l: f o wedge_inl == g o wedge_inl
r: f o wedge_inr == g o wedge_inr
w: ap f wglue @ r pt = l pt @ ap g wglue
f == g
  napply (wedge_ind _ l r).
X, Y, Z: pType
f, g: X \/ Y -> Z
l: f o wedge_inl == g o wedge_inl
r: f o wedge_inr == g o wedge_inr
w: ap f wglue @ r pt = l pt @ ap g wglue
transport (fun xy : X \/ Y => f xy = g xy) wglue
  (l pt) = r pt
  transport_paths FlFr.
X, Y, Z: pType
f, g: X \/ Y -> Z
l: f o wedge_inl == g o wedge_inl
r: f o wedge_inr == g o wedge_inr
w: ap f wglue @ r pt = l pt @ ap g wglue
ap f wglue @ r pt = l pt @ ap g wglue
  exact w.
Defined.

Definition wedge_ind_FFl {X Y Z W : pType} (f : X \/ Y -> Z) (g : Z -> W)
  {y : W}
  (l : forall x, g (f (wedge_inl x)) = y)
  (r : forall x, g (f (wedge_inr x)) = y)
  (w : l pt = ap g (ap f wglue) @ r pt)
  : forall x, g (f x) = y.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
forall x : X \/ Y, g (f x) = y
Proof.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
forall x : X \/ Y, g (f x) = y
  napply (wedge_ind _ l r); simpl.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
transport
  (fun xy : Pushout (unit_name pt) (unit_name pt) =>
   g (f xy) = y) wglue (l pt) = r pt
  transport_paths FFl.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
l pt = ap g (ap f wglue) @ r pt
  exact w.
Defined.

Definition wedge_ind_FFlr {X Y Z : pType} (f : X \/ Y -> Z) (g : Z -> X \/ Y)
  (l : g o f o wedge_inl == wedge_inl)
  (r : g o f o wedge_inr == wedge_inr)
  (w : ap g (ap f wglue) @ r pt = l pt @ wglue)
  : g o f == idmap.
X, Y, Z: pType
f: X \/ Y -> Z
g: Z -> X \/ Y
l: g o f o wedge_inl == wedge_inl
r: g o f o wedge_inr == wedge_inr
w: ap g (ap f wglue) @ r pt = l pt @ wglue
g o f == idmap
Proof.
X, Y, Z: pType
f: X \/ Y -> Z
g: Z -> X \/ Y
l: g o f o wedge_inl == wedge_inl
r: g o f o wedge_inr == wedge_inr
w: ap g (ap f wglue) @ r pt = l pt @ wglue
g o f == idmap
  napply (wedge_ind _ l r); simpl.
X, Y, Z: pType
f: X \/ Y -> Z
g: Z -> X \/ Y
l: g o f o wedge_inl == wedge_inl
r: g o f o wedge_inr == wedge_inr
w: ap g (ap f wglue) @ r pt = l pt @ wglue
transport
  (fun xy : Pushout (unit_name pt) (unit_name pt) =>
   g (f xy) = xy) wglue (l pt) = r pt
  transport_paths FFlr.
X, Y, Z: pType
f: X \/ Y -> Z
g: Z -> X \/ Y
l: g o f o wedge_inl == wedge_inl
r: g o f o wedge_inr == wedge_inr
w: ap g (ap f wglue) @ r pt = l pt @ wglue
ap g (ap f wglue) @ r pt = l pt @ wglue
  exact w.
Defined.

(** 1-universal property of wedge. *)
Lemma wedge_up X Y Z (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
f ==* g
Proof.
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
  snapply 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 napply (wedge_ind_FlFr 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
ap f wglue @ q pt = p pt @ ap g wglue
    lhs napply (1 @@ 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 wglue @
dpoint
  (pfam_phomotopy (f o* wedge_inr) (g o* wedge_inr)) =
p pt @ ap g wglue
    rhs napply (dpoint_eq p @@ 1).
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 wglue @
dpoint
  (pfam_phomotopy (f o* wedge_inr) (g o* wedge_inr)) =
dpoint
  (pfam_phomotopy (f o* wedge_inl) (g o* wedge_inl)) @
ap g wglue
    clear p q; simpl.
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @
((ap f wglue^ @ point_eq f) @
 (ap g wglue^ @ point_eq g)^) =
((1 @ point_eq f) @ (1 @ point_eq g)^) @ ap g wglue
    rhs napply (((concat_1p _) @@ ap inverse (concat_1p _)) @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @
((ap f wglue^ @ point_eq f) @
 (ap g wglue^ @ point_eq g)^) =
(point_eq f @ (point_eq g)^) @ ap g wglue
    lhs napply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
(ap f wglue @ (ap f wglue^ @ point_eq f)) @
(ap g wglue^ @ point_eq g)^ =
(point_eq f @ (point_eq g)^) @ ap g wglue
    apply moveR_pV.
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ (ap f wglue^ @ point_eq f) =
((point_eq f @ (point_eq g)^) @ ap g wglue) @
(ap g wglue^ @ point_eq g)
    lhs napply (1 @@ (ap_V _ _ @@ 1)).
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ ((ap f wglue)^ @ point_eq f) =
((point_eq f @ (point_eq g)^) @ ap g wglue) @
(ap g wglue^ @ point_eq g)
    lhs napply concat_p_Vp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
((point_eq f @ (point_eq g)^) @ ap g wglue) @
(ap g wglue^ @ point_eq g)
    rhs napply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
(((point_eq f @ (point_eq g)^) @ ap g wglue) @
 ap g wglue^) @ point_eq g
    rhs napply ((1 @@ ap_V _ _) @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
(((point_eq f @ (point_eq g)^) @ ap g wglue) @
 (ap g wglue)^) @ point_eq g
    rhs napply (concat_pp_V _ _ @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f = (point_eq f @ (point_eq g)^) @ point_eq g
    by apply moveL_pM.
  -
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
wedge_ind_FlFr p q
  ((1 @@ dpoint_eq q) @
   (((concat_p_pp (ap f wglue)
        (ap f wglue^ @ point_eq f)
        (ap g wglue^ @ point_eq g)^ @
      moveR_pV (ap g wglue^ @ point_eq g)
        ((point_eq f @ (point_eq g)^) @ ap g wglue)
        (ap f wglue @ (ap f wglue^ @ point_eq f))
        ((1 @@ (ap_V f wglue @@ 1)) @
         (concat_p_Vp (ap f wglue) (point_eq f) @
          (((moveL_pM (point_eq g) (point_eq f)
               (point_eq f @ (point_eq g)^) 1 @
             (concat_pp_V (... @ ...^) (ap g wglue) @@
              1)^) @ ((1 @@ ap_V g wglue) @@ 1)^) @
           (concat_p_pp
              ((point_eq f @ (point_eq g)^) @
               ap g wglue) (ap g wglue^) (point_eq g))^)))) @
     ((concat_1p (point_eq f) @@
       ap inverse (concat_1p (point_eq g))) @@ 1)^
     :
     ap f wglue @
     dpoint
       (pfam_phomotopy (f o* wedge_inr)
          (g o* wedge_inr)) =
     dpoint
       (pfam_phomotopy (f o* wedge_inl)
          (g o* wedge_inl)) @ ap g wglue) @
    (dpoint_eq p @@ 1)^)) pt =
dpoint_eq f @ (dpoint_eq g)^ simpl.
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)^
    lhs exact (dpoint_eq p); simpl.
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
(1 @ point_eq f) @ (1 @ point_eq g)^ =
dpoint_eq f @ (dpoint_eq g)^
    exact (concat_1p _ @@ ap inverse (concat_1p _)).
Defined.

Instance hasbinarycoproducts : HasBinaryCoproducts pType.
HasBinaryCoproducts pType
Proof.
HasBinaryCoproducts pType
  intros X Y.
X, Y: pType
BinaryCoproduct X Y
  snapply Build_BinaryCoproduct.
X, Y: pType
pType
X, Y: pType
Core.Hom X ?cat_coprod
X, Y: pType
Core.Hom Y ?cat_coprod
X, Y: pType
forall z : pType,
Core.Hom X z -> Core.Hom Y z -> Core.Hom ?cat_coprod z
X, Y: pType
forall (z : pType) (f : Core.Hom X z)
(g : Core.Hom Y z),
Core.GpdHom
  (Core.cat_comp (?cat_coprod_rec z f g) ?cat_inl) f
X, Y: pType
forall (z : pType) (f : Core.Hom X z)
(g : Core.Hom Y z),
Core.GpdHom
  (Core.cat_comp (?cat_coprod_rec z f g) ?cat_inr) g
X, Y: pType
forall (z : pType) (f g : Core.Hom ?cat_coprod z),
Core.GpdHom (Core.cat_comp f ?cat_inl)
  (Core.cat_comp g ?cat_inl) ->
Core.GpdHom (Core.cat_comp f ?cat_inr)
  (Core.cat_comp g ?cat_inr) -> Core.GpdHom f g
  -
X, Y: pType
pType exact (X \/ Y).
  -
X, Y: pType
Core.Hom X (X \/ Y) exact wedge_inl.
  -
X, Y: pType
Core.Hom Y (X \/ Y) exact wedge_inr.
  -
X, Y: pType
forall z : pType,
Core.Hom X z -> Core.Hom Y z -> Core.Hom (X \/ Y) z exact (@wedge_rec X Y).
  -
X, Y: pType
forall (z : pType) (f : Core.Hom X z)
(g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (wedge_rec f g) wedge_inl)
  f exact (@wedge_rec_beta_inl X Y).
  -
X, Y: pType
forall (z : pType) (f : Core.Hom X z)
(g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (wedge_rec f g) wedge_inr)
  g exact (@wedge_rec_beta_inr X Y).
  -
X, Y: pType
forall (z : pType) (f g : Core.Hom (X \/ Y) z),
Core.GpdHom (Core.cat_comp f wedge_inl)
  (Core.cat_comp g wedge_inl) ->
Core.GpdHom (Core.cat_comp f wedge_inr)
  (Core.cat_comp g wedge_inr) -> Core.GpdHom f g exact (wedge_up X Y).
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
  snapply 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)^
  symmetry; simpl.
X, Y: pType
(ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue^ @ 1) @
1 = 1
  do 2 lhs napply concat_p1.
X, Y: pType
ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue^ = 1
  lhs napply (ap_V _ wglue).
X, Y: pType
(ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue)^ = 1
  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
  snapply 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)^
  symmetry; simpl.
X, Y: pType
(ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue^ @ 1) @
1 = 1
  do 2 lhs napply concat_p1.
X, Y: pType
ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue^ = 1
  lhs napply (ap_V _ wglue).
X, Y: pType
(ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue)^ = 1
  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
  snapply 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
  snapply 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
?f pt = pt
  -
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
FamilyWedge I X -> Z snapply 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 exact (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 (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 (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 (fun i : I => f i)) pconst
  (fun i : I => point_eq (f i)) pt = pt exact idpath.
Defined.

Instance hasallcoproducts_ptype : HasAllCoproducts pType.
HasAllCoproducts pType
Proof.
HasAllCoproducts pType
  intros I X.
I: Type
X: I -> pType
Coproduct I X
  snapply Build_Coproduct.
I: Type
X: I -> pType
pType
I: Type
X: I -> pType
forall i : I, Core.Hom (X i) ?cat_coprod
I: Type
X: I -> pType
forall z : pType,
(forall i : I, Core.Hom (X i) z) ->
Core.Hom ?cat_coprod z
I: Type
X: I -> pType
forall (z : pType)
(f : forall i : I, Core.Hom (X i) z) (i : I),
Core.GpdHom
  (Core.cat_comp (?cat_coprod_rec z f) (?cat_in i))
  (f i)
I: Type
X: I -> pType
forall (z : pType) (f g : Core.Hom ?cat_coprod z),
(forall i : I,
 Core.GpdHom (Core.cat_comp f (?cat_in i))
   (Core.cat_comp g (?cat_in i))) -> Core.GpdHom f g
  -
I: Type
X: I -> pType
pType exact (FamilyWedge I X).
  -
I: Type
X: I -> pType
forall i : I, Core.Hom (X i) (FamilyWedge I X) exact (fwedge_in' I X).
  -
I: Type
X: I -> pType
forall z : pType,
(forall i : I, Core.Hom (X i) z) ->
Core.Hom (FamilyWedge I X) z exact (fwedge_rec I X).
  -
I: Type
X: I -> pType
forall (z : pType)
(f : forall i : I, Core.Hom (X i) z) (i : I),
Core.GpdHom
  (Core.cat_comp (fwedge_rec I X z f)
     (fwedge_in' I X i)) (f i) intros Z f i.
I: Type
X: I -> pType
Z: pType
f: forall i : I, Core.Hom (X i) Z
i: I
Core.GpdHom
  (Core.cat_comp (fwedge_rec I X Z f)
     (fwedge_in' I X i)) (f i)
    snapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f: forall i : I, Core.Hom (X i) Z
i: I
Core.cat_comp (fwedge_rec I X Z f) (fwedge_in' I X i) ==
f i
I: Type
X: I -> pType
Z: pType
f: forall i : I, Core.Hom (X i) Z
i: I
?p pt =
dpoint_eq
  (Core.cat_comp (fwedge_rec I X Z f)
     (fwedge_in' I X i)) @ (dpoint_eq (f i))^
    1: reflexivity.
I: Type
X: I -> pType
Z: pType
f: forall i : I, Core.Hom (X i) Z
i: I
(fun x0 : X i => 1) pt =
dpoint_eq
  (Core.cat_comp (fwedge_rec I X Z f)
     (fwedge_in' I X i)) @ (dpoint_eq (f i))^
    simpl.
I: Type
X: I -> pType
Z: pType
f: forall i : I, Core.Hom (X i) Z
i: I
1 =
(ap
   (Pushout_rec Z (sig_rec (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, Core.Hom (X i) Z
i: I
1 @ dpoint_eq (f i) =
ap
  (Pushout_rec Z (sig_rec (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, Core.Hom (X i) Z
i: I
dpoint_eq (f i) =
ap
  (Pushout_rec Z (sig_rec (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, Core.Hom (X i) Z
i: I
ap
  (Pushout_rec Z (sig_rec (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 : Core.Hom (FamilyWedge I X) z),
(forall i : I,
 Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
   (Core.cat_comp g (fwedge_in' I X i))) ->
Core.GpdHom f g intros Z f g h.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
Core.GpdHom f g
    snapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
f == g
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
?p pt = dpoint_eq f @ (dpoint_eq g)^
    +
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
f == g snapply Pushout_ind.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
i: I
x: X i
f (pushl (i; x)) = g (pushl (i; x))
        napply h.
      *
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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)^
        transport_paths FlFr.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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 napply concat_p_pp.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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 napply concat_pp_p.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (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) @
   moveR_Vp_p_inv (ap f (pglue i)) (h i pt)
     (ap g (pglue i)) (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 ==* @pmap_idmap (psusp X).
X: pType
wedge_pr1 o* psusp_pinch X ==* pmap_idmap
Proof.
X: pType
wedge_pr1 o* psusp_pinch X ==* pmap_idmap
  snapply Build_pHomotopy.
X: pType
wedge_pr1 o* psusp_pinch X == pmap_idmap
X: pType
?p pt =
dpoint_eq (wedge_pr1 o* psusp_pinch X) @
(dpoint_eq pmap_idmap)^
  -
X: pType
wedge_pr1 o* psusp_pinch X == pmap_idmap snapply Susp_ind_FlFr.
X: pType
(wedge_pr1 o* psusp_pinch X) North = pmap_idmap North
X: pType
(wedge_pr1 o* psusp_pinch X) South = pmap_idmap South
X: pType
forall x : X,
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ ?HS =
?HN @ ap pmap_idmap (merid x)
    +
X: pType
(wedge_pr1 o* psusp_pinch X) North = pmap_idmap North reflexivity.
    +
X: pType
(wedge_pr1 o* psusp_pinch X) South = pmap_idmap South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x) intros x.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x)
      rhs napply concat_1p.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
ap pmap_idmap (merid x)
      rhs napply 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 napply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr1 (ap (psusp_pinch X) (merid x)) =
loop_susp_unit X x
      lhs napply (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 napply ap_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)) @
(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 napply (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 napply 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 napply (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 napply 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 napply 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 napply 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 napply (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 napply (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) pmap_idmap
  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_pV wedge_pr1
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x)) 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 wedge_pr1 (...) @ x0)
                ((ap_compose pushr wedge_pr1 (...))^ @
                 ap_const (loop_susp_unit X x)
                   (wedge_pr1 ...)) @
              (concat_p1 (ap wedge_pr1 (...)) @
               (ap_pp wedge_pr1 (...) wglue @
                (... @ ...))))) @
            (whiskerL (loop_susp_unit X x)
               (wedge_rec_beta_wglue pmap_idmap pconst))^)))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap pmap_idmap (merid x)))^) pt =
dpoint_eq (wedge_pr1 o* psusp_pinch X) @
(dpoint_eq pmap_idmap)^ reflexivity.
Defined.

Definition wedge_pr2_psusp_pinch {X}
  : wedge_pr2 o* psusp_pinch X ==* @pmap_idmap (psusp X).
X: pType
wedge_pr2 o* psusp_pinch X ==* pmap_idmap
Proof.
X: pType
wedge_pr2 o* psusp_pinch X ==* pmap_idmap
  snapply Build_pHomotopy.
X: pType
wedge_pr2 o* psusp_pinch X == pmap_idmap
X: pType
?p pt =
dpoint_eq (wedge_pr2 o* psusp_pinch X) @
(dpoint_eq pmap_idmap)^
  -
X: pType
wedge_pr2 o* psusp_pinch X == pmap_idmap snapply Susp_ind_FlFr.
X: pType
(wedge_pr2 o* psusp_pinch X) North = pmap_idmap North
X: pType
(wedge_pr2 o* psusp_pinch X) South = pmap_idmap South
X: pType
forall x : X,
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ ?HS =
?HN @ ap pmap_idmap (merid x)
    +
X: pType
(wedge_pr2 o* psusp_pinch X) North = pmap_idmap North reflexivity.
    +
X: pType
(wedge_pr2 o* psusp_pinch X) South = pmap_idmap South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x) intros x.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x)
      rhs napply concat_1p.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
ap pmap_idmap (merid x)
      rhs napply 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 napply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr2 (ap (psusp_pinch X) (merid x)) =
loop_susp_unit X x
      lhs napply (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 napply ap_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)) @
(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 napply (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 napply 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 napply (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 napply 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 napply 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 napply 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 napply concat_pV.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @
ap wedge_pr2 wglue = 1
      lhs napply (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 napply (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) pmap_idmap
  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_pV wedge_pr2
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x)) 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 wedge_pr2 (...) @ x0)
                ((ap_compose pushr wedge_pr2 (...))^ @
                 ap_idmap (loop_susp_unit X x)) @
              (moveR_pM (loop_susp_unit X x)
                 (loop_susp_unit X x)
                 (ap wedge_pr2 (...))
                 (ap_pp wedge_pr2 ... wglue @ (...)) @
               (concat_p1 (loop_susp_unit X x))^))) @
            (whiskerL (loop_susp_unit X x)
               (wedge_rec_beta_wglue pconst pmap_idmap))^)))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap pmap_idmap (merid x)))^) pt =
dpoint_eq (wedge_pr2 o* psusp_pinch X) @
(dpoint_eq pmap_idmap)^ reflexivity.
Defined.

(** ** Connectivity of wedge inclusion *)

Definition extension_wedge_incl {X Y : pType} (P : X * Y -> Type)
  (d : forall a : X \/ Y, P (wedge_incl X Y a))
  (f : forall (x : X) (y : Y), P (x, y))
  (p : forall (x : X), f x pt = d (wedge_inl x))
  (q : forall (y : Y), f pt y = d (wedge_inr y))
  (pq : p pt
        = q pt
            @ ((apD d wglue)^
                 @ transport_compose_path_ap P (wedge_incl X Y) (wedge_incl_beta_wglue) _))
  : ExtensionAlong (wedge_incl X Y) P d.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
ExtensionAlong (wedge_incl X Y) P d
Proof.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
ExtensionAlong (wedge_incl X Y) P d
  exists (prod_ind _ f).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
forall x : X \/ Y,
prod_ind P f (wedge_incl X Y x) = d x
  napply (wedge_ind _ p q).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport
  (fun xy : X \/ Y =>
   prod_ind P f (wedge_incl X Y xy) = d xy) wglue
  (p pt) = q pt
  lhs napply (transport_paths_FlFr_D wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
((apD
    (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
    wglue)^ @
 ap
   (transport (fun x : X \/ Y => P (wedge_incl X Y x))
      wglue) (p pt)) @ apD d wglue = q pt
  apply moveR_pM.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
(apD
   (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
   wglue)^ @
ap
  (transport (fun x : X \/ Y => P (wedge_incl X Y x))
     wglue) (p pt) = q pt @ (apD d wglue)^
  apply moveR_Vp.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
ap
  (transport (fun x : X \/ Y => P (wedge_incl X Y x))
     wglue) (p pt) =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @ (q pt @ (apD d wglue)^)
  unshelve lhs napply ap_homotopic_id.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
forall x : P (wedge_incl X Y (pushr pt)),
transport (fun x0 : X \/ Y => P (wedge_incl X Y x0))
  wglue x = x
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
(?Goal (prod_ind P f (wedge_incl X Y (pushl pt))) @
 p pt) @ (?Goal (d (pushl pt)))^ =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @ (q pt @ (apD d wglue)^)
  1: exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
(transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue
   (prod_ind P f (wedge_incl X Y (pushl pt))) @ p pt) @
(transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))^ =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @ (q pt @ (apD d wglue)^)
  change (prod_ind P f (wedge_incl X Y (pushl pt))) with (f pt pt).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
(transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (f pt pt) @ p pt) @
(transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))^ =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @ (q pt @ (apD d wglue)^)
  apply moveR_pV.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt) @ p pt =
(apD
   (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
   wglue @ (q pt @ (apD d wglue)^)) @
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (d (pushl pt))
  rhs napply concat_pp_p.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt) @ p pt =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @
((q pt @ (apD d wglue)^) @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
  rhs napply (1 @@ concat_pp_p _ _ _).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt) @ p pt =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue @
(q pt @
 ((apD d wglue)^ @
  transport_compose_path_ap P (wedge_incl X Y)
    wedge_incl_beta_wglue (d (pushl pt))))
  nrefine (_ @@ pq).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt) =
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue
  symmetry.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
apD
  (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x))
  wglue =
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt)
  lhs napply apD_compose.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose P (wedge_incl X Y) wglue
  (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport_compose_path_ap P (wedge_incl X Y)
  wedge_incl_beta_wglue (f pt pt)
  unfold transport_compose_path_ap.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport_compose P (wedge_incl X Y) wglue
  (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport_compose P (wedge_incl X Y) wglue (f pt pt) @
transport2 P wedge_incl_beta_wglue (f pt pt)
  apply whiskerL.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport2 P wedge_incl_beta_wglue (f pt pt)
  lhs napply (apD02 _ wedge_incl_beta_wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall y : Y, f pt y = d (wedge_inr y)
pq: p pt =
q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y)
   wedge_incl_beta_wglue (d (pushl pt)))
transport2 P wedge_incl_beta_wglue
  (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) 1 =
transport2 P wedge_incl_beta_wglue (f pt pt)
  apply concat_p1.
Defined.

Definition conn_map_wedge_incl `{Univalence} {m n : trunc_index} (X Y : pType)
  `{!IsConnected m.+1 X, !IsConnected n.+1 Y}
  : IsConnMap (m +2+ n) (wedge_incl X Y).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
IsConnMap (Tr (m +2+ n)) (wedge_incl X Y)
Proof.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
IsConnMap (Tr (m +2+ n)) (wedge_incl X Y)
  apply conn_map_from_extension_elim.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
forall P : [X * Y, ispointed_prod] -> Type,
(forall b : [X * Y, ispointed_prod],
 In (Tr (m +2+ n)) (P b)) ->
forall d : forall a : X \/ Y, P (wedge_incl X Y a),
ExtensionAlong (wedge_incl X Y) P d
  intros P h d.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
ExtensionAlong (wedge_incl X Y) P d
  snapply extension_wedge_incl.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall (x : X) (y : Y), P (x, y)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall x : X, ?f x pt = d (wedge_inl x)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall y : Y, ?f pt y = d (wedge_inr y)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
?p pt =
?q pt @
((apD d wglue)^ @
 transport_compose_path_ap P 
   (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt)))
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall (x : X) (y : Y), P (x, y) rapply (wedge_incl_elim _ _ (fun x y => P (x, y)) (d o wedge_inr) (d o wedge_inl)).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
d (wedge_inr (ispointed_type Y)) =
d (wedge_inl (ispointed_type X))
    lhs_V exact (apD d wglue).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
transport (fun a : X \/ Y => P (wedge_incl X Y a))
  wglue (d (pushl pt)) =
d (wedge_inl (ispointed_type X))
    exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue _).
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall x : X,
wedge_incl_elim (ispointed_type X) 
  (ispointed_type Y)
  (fun (x0 : X) (y : Y) => P (x0, y)) 
  (d o wedge_inr) (d o wedge_inl)
  ((apD d wglue)^ @
   transport_compose_path_ap P 
     (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt))) x pt = 
d (wedge_inl x) napply wedge_incl_comp2.
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall y : Y,
wedge_incl_elim (ispointed_type X) 
  (ispointed_type Y)
  (fun (x : X) (y0 : Y) => P (x, y0)) 
  (d o wedge_inr) (d o wedge_inl)
  ((apD d wglue)^ @
   transport_compose_path_ap P 
     (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt))) pt y = 
d (wedge_inr y) napply wedge_incl_comp1.
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod],
In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
wedge_incl_comp2 (ispointed_type X) 
  (ispointed_type Y) 
  (fun (x : X) (y : Y) => P (x, y))
  (fun x : Y => d (wedge_inr x))
  (fun x : X => d (wedge_inl x))
  ((apD d wglue)^ @
   transport_compose_path_ap P 
     (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt))) pt =
wedge_incl_comp1 (ispointed_type X) 
  (ispointed_type Y) 
  (fun (x : X) (y : Y) => P (x, y))
  (fun x : Y => d (wedge_inr x))
  (fun x : X => d (wedge_inl x))
  ((apD d wglue)^ @
   transport_compose_path_ap P 
     (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt))) pt @
((apD d wglue)^ @
 transport_compose_path_ap P 
   (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt))) napply wedge_incl_comp3.
Defined.